patternMinor
Is model checking PSpace-hard *in formula size*?
Viewed 0 times
sizecheckinghardpspaceformulamodel
Problem
Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete.
Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally?
How to prove that a decision problem that has several parameters (here, $\phi$ and system) is PSpace-hard in one of the parameters? I guess we would need to poly-time reduce some PSpace-complete problem to our problem with the unintereseting parameter being fixed, while the interesting parameter can vary.
But the original proof of Sistla/Clarke [Lemma 4.4, SC82] does not do the thing above! In their proof, both parameters of the resulting LTL model-checking problem instance depend on $n$, where $n$ is the TM tape bound. Is there a proof that fixes one of the parameters?
Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally?
How to prove that a decision problem that has several parameters (here, $\phi$ and system) is PSpace-hard in one of the parameters? I guess we would need to poly-time reduce some PSpace-complete problem to our problem with the unintereseting parameter being fixed, while the interesting parameter can vary.
But the original proof of Sistla/Clarke [Lemma 4.4, SC82] does not do the thing above! In their proof, both parameters of the resulting LTL model-checking problem instance depend on $n$, where $n$ is the TM tape bound. Is there a proof that fixes one of the parameters?
Solution
You are certainly right that the level of rigor found in old papers making such claims can be a bit low at times when viewed from today's perspective.
The claim is correct anyway, even if it does not follow from Sistla/Clarke's proof. The reason is that LTL satisfiability checking is also PSPACE-complete. You can see satisfiability checking as a special case of model checking.
More formally, you want to prove the following: There exists a fixed model such that given an LTL formula, checking if the formula holds on the model is PSPACE-hard. Now the satisfiability checking problem does not restrict the number of atomic propositions, so a fixed model does not do the trick. However, S. Demri and P. Schnoebelen show in the paper "The complexity of propositional linear temporal logics in simple cases" (Inf. Comput., 174(1):84–103, 2002) that the satisfiability problem is hard even if we only have a single atomic proposition.
The claim is correct anyway, even if it does not follow from Sistla/Clarke's proof. The reason is that LTL satisfiability checking is also PSPACE-complete. You can see satisfiability checking as a special case of model checking.
More formally, you want to prove the following: There exists a fixed model such that given an LTL formula, checking if the formula holds on the model is PSPACE-hard. Now the satisfiability checking problem does not restrict the number of atomic propositions, so a fixed model does not do the trick. However, S. Demri and P. Schnoebelen show in the paper "The complexity of propositional linear temporal logics in simple cases" (Inf. Comput., 174(1):84–103, 2002) that the satisfiability problem is hard even if we only have a single atomic proposition.
Context
StackExchange Computer Science Q#106726, answer score: 5
Revisions (0)
No revisions yet.