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?