Il modello che controlla pspace-hard *nella dimensione della formula *?

Question

Sistla/Clarke ha dimostrato [SC82] che il problema di controllo del modello LTL sia complesso PSPACE. A volte le persone scrivono che questo problema è "PSPACE-HARD in $ | phi | $" (per esempio [LP85]). Cosa significa formalmente questo?

Come dimostrare che un problema decisionale che ha diversi parametri (qui, $ phi $ e sistema) PSPACE-Hard è in uno dei parametri? Immagino che avremmo bisogno di ridurre il problema con il problema con il problema con il parametro ininterisibile che viene risolto, mentre il parametro interessante può variare.

Ma la prova originale di Sistla/Clarke [Lemma 4.4, SC82] non fa la cosa sopra! Nella loro prova, entrambi i parametri dell'istanza del problema del modello di controllo del modello LTL risultante $ n $, dove $ n $ è il nastro TM legato. Esiste una prova che fissa uno dei parametri?