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 C1 and C2 of P, is it possible to reach C2 from C1 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 C2 and then check whether C1 is in the language of A; recall that membership checking for finite automata is solvable in linear time. First, observe that C2 is a single word and is obviously regular. We start with an automaton for C2 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.