2
$\begingroup$

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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Cilenco
    Commented Jan 31, 2019 at 22:32
  • $\begingroup$ @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. $\endgroup$
    – DCTLib
    Commented Feb 1, 2019 at 7:54
1
$\begingroup$

Check Lichtenstein and Pnueli's 1985 POPL paper.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – DCTLib
    Commented Jan 31, 2019 at 16:45
  • $\begingroup$ Lichtenstein & Pnueli give an algorithm that provides the upper bound matching the lower bound proved in Sistla and Clarke's 1982 STOC paper. $\endgroup$
    – Kai
    Commented Feb 2, 2019 at 8:29
  • $\begingroup$ 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? $\endgroup$
    – DCTLib
    Commented Feb 2, 2019 at 9:30
  • $\begingroup$ That's in the paragraph beginning on page 97 and ending on page 98. $\endgroup$
    – Kai
    Commented Feb 2, 2019 at 9:34
  • $\begingroup$ 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. $\endgroup$
    – DCTLib
    Commented Feb 2, 2019 at 17:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.