Why is LTL Model Checking in PSPACE

Given a LTL formula $$\phi$$ and a transition system $$T$$ we have to do following steps:

1. Build a (non deterministic) Büchi automaton for $$T$$
2. Build a (non deterministic) Büchi automaton for $$\phi$$
3. Compute the intersection of these automatons and check for emptyness

Step 1 can be done in $$\mathcal{O}(|T|)$$ time and space. I also know and understand that step 3 requires $$\mathcal{O}(log^2n)$$ space. But what about step 2? The size of the resulting Büchi Automaton from a LTL formula can be exponential in $$|\phi|$$. Writing that down requires more then polynomial space. So what am I missing here?

Do you may have any papers or books I could read on this topic?

It is correct that writing the Buchi automaton to memory takes exponential space.....which is why you don't do that.

The construction for the Buchi automaton is however very regular and can be done in a forward manner. This allows you to construct it on-the-fly while you search for an accepting lasso in the product between the Buchi automaton and $$T$$.

In this way, you can find an accepting lasso in NPSPACE (it is exists): you build a Turing machine that builds the product on-the-fly, searches for a lasso by non-deterministically guessing which transition in the product to take, and non-determinstically guesses the lasso knot to store (which, w.l.o.g., could also be the required accepting state). If it finds a path to such a knot and then a path from the knot back to the knot, you know that there is a word in the product.

To make this algorithm always terminate, you also have a counter to keep track of the number of transitions observed so far. If it exceeds two times the size of the product, then the algorithm aborts with a "no" answer. Such a counter also only needs space polynomial in the size of the LTL formula.

Since PSPACE=NPSPACE, it follows that you only need polynomial space for such a Turing machine.

• Great answer thank you for this. Do you have any papers for on-the-fly construction? And is it needed for this to use a generalized BA or is a normal one okay for that too? – Cilenco Jan 31 '19 at 22:32
• @Cilenco You can degeneralize the GBA on-the-fly as well and hence the construction works with an ordinary Buchi automaton as well. Alternatively, you can use the LTL->Alternating automaton->Buchi automaton construction for getting from LTL to a Buchi automaton, which avoids generalized Buchi automata altogether and can be done on-the-fly, too. I don't know any papers containing the full construction, I'm afraid. My best guess is the Baier/Katoen "Model Checking" book, but that's only a guess. – DCTLib Feb 1 '19 at 7:54
• Does this paper actually explain the space complexity? From a quick reading, the section "Complcxity of the Checking Algorithm" only mentions an exponential time complexity of their algorithm. – DCTLib Jan 31 '19 at 16:45
• Lichtenstein & Pnueli give an algorithm that provides the upper bound matching the lower bound proved in Sistla and Clarke's 1982 STOC paper. – Kai Feb 2 '19 at 8:29
• Well, the Liechtenstein and Pnueli paper contains an exponential time upper bound and no PSPACE lower bound as I can see. Could you state where exactly in the paper the PSCAPE lower bound is mentioned? – DCTLib Feb 2 '19 at 9:30
• That's in the paragraph beginning on page 97 and ending on page 98. – Kai Feb 2 '19 at 9:34
• Ah, I see. The claim is indeed in the introduction. That paragraph does not say why the problem is in PSPACE, though (which is what the OP asked). And the rest of the paper does not do this either, as far as I can see. – DCTLib Feb 2 '19 at 17:42