I'm thinking of restructuring my blogs. I've recently found that things have changed a lot since I started my break a year or so ago: Lance has retired from blogging, Andy D has started his new cool blog, and Luca Aceto has his blog. Ah ... also I'm having a lot of difficulty deciphering blogger's word verification mechanism.
Unfortunately, I've become really rusty with HTML and will have to start getting used to it again. Shocked with what a long break can do to one's dexterity ;) Anyway, I'll put all the new links some time soon.
Monday, June 30, 2008
Thursday, June 26, 2008
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 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:
It seems that similar ideas were already proposed earlier for ground tree rewrite systems, a more general class of systems, in:
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.
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.
Subscribe to:
Posts (Atom)