Pushdown systems: reachability via saturations

Finally, I have some time to resume blogging again after finishing several papers (and now with something with more content). Before I continue, I'd like to apologize for not replying some comments because by mistake I had them forwarded to an expired email address. How careless I was!

Anyway, I'm intending to cover a simple basic topic in the verification of infinite-state systems. Reachability is probably the most basic question when you do verification and we would like to see how to solve this problem efficiently for pushdown systems, which are the simplest well-behaved class of infinite-state systems. For those practically-minded, pushdown systems can naturally be used to model sequential programs and algorithms for pushdown systems have been implemented and used for doing program analysis for real. By the way, the saturation technique also extends to other (more powerful) classes of infinite-state systems and so it's really worth knowing. Anyway, please review the definition of pushdown systems here before you continue.

Roughly speaking, the reachability problem for pushdown systems asks the following question: given a pushdown system P and two configurations C₁ and C₂ of P, is it possible to reach C₂ from C₁ in P? There are other variants of the problem that take sets of configurations instead of just single configurations, and they can be solved using exactly the same saturation technique.

In here I have mentioned that the MSO theory of pushdown systems is decidable and this implies that reachability is also decidable. However, the algorithm that you obtain in this way runs in exponential time.

The idea of saturation construction is to construct a finite automaton A that recognizes the set of configurations that can reach C₂ and then check whether C₁ is in the language of A; recall that membership checking for finite automata is solvable in linear time. First, observe that C₂ is a single word and is obviously regular. We start with an automaton for C₂ and introduce several extra states, each corresponding to a state of the pushdown system P. Call this automaton A. We shall iteratively add transitions to A by the following rules: if there is a transition (p,a,c,v,p') in P, and in the automaton A the state p' can reach a state q via the word v, then we shall add a transition (p,c,q) in A. The intuitive idea is that if a configuration p'vw is accepted by A, then the configuration paw must also be accepted by A because you can apply the transition (p,a,c,v,p'). By the way, notice that we don't add any states in the iteration and so the algorithm can only add polynomially many transitions to A. Hence, the algorithm terminates in polynomial time.

As far as I remember, the idea was first proposed in the paper by Bouajjani, Esparza, and Maler for pushdown systems:

Reachability analysis of pushdown automata: Application to model-checking. CONCUR 1997.

It seems that similar ideas were already proposed earlier for ground tree rewrite systems, a more general class of systems, in:

Coquide, Dauchet, and Gilleron. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science 127, 1994.

By the way, it is worth noticing that simple fixpoint computations might not terminate for pushdown systems, as the state space is infinite. So, the saturation construction is necessary after all.