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:

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.

25 comments:

Anonymous said...

Who knows where to download XRumer 5.0 Palladium?
Help, please. All recommend this program to effectively advertise on the Internet, this is the best program!

cara beli rumah tanpa modal said...

thanks to article master

halaman rumah said...

i like your article sir :)

perumahan baru di tangerang said...

Very beautiful, this blog write very meaningful,your article is really Great

harga rumah saat ini said...

i like your article, thanks to sharing master :)

rumah bebas banjir said...

thanks to posting master

model rumah minimalis said...

thank you for sharing this information very useful

rumah hak milik said...

thank you for sharing this information very useful :)

perumahan di sawangan depok said...

I strongly agree with your article :)

green orchid residence bsd said...

so many that I can take from this blog very helpful. :)

rumah dijual di serpong said...

have much to learn from this article

Rumah Minimalis 1 Lantai Dijual said...

thank you for the information :)

Perumahan di pamulang said...

thanks to posting master

Perkembangan kota Cibinong said...

Very beautiful, this blog write very meaningful,your article is really Great :)

Perumahan di pamulang said...

thanks to posting master

Perumahan Trevista Ciputat said...

i like your article, thanks to sharing master :)

perumahan griya cibinong asri said...

so many that I can take from this blog very helpful. :)

pengaruh nilai tukar rupiah said...

Good! Wish everybody wrote so :)

properti saya said...

site Its really informative :)

Tips Beli Rumah said...

thanks for the info master :)

surat kuasa kepada penjual said...

your posting thats i like :)

Tips Memilih Pengisi Ruangan said...

have much to learn from this article

Kemenpera Tidak Memberikan Sub said...

I like this article. :)

Cara Jitu menata Taman yang In said...

site Its really informative :)

MENYIGAPI GANGGUAN DI TEMPAT H said...

your articles that I like :)