Is model checking PSpace-hard *in formula size*?

Question

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?

Answer 1

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.