Pushdown Processes: Games and Model Checking | Zendy

Igor Walukiewicz | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Pushdown Processes: Games and Model Checking

Author(s) -

Igor Walukiewicz

Publication year - 1996

Publication title -

brics report series

Language(s) - English

Resource type - Journals

eISSN - 1601-5355

pISSN - 0909-0878

DOI - 10.7146/brics.v3i54.20057

Subject(s) - embedded pushdown automaton , pushdown automaton , model checking , deterministic context free grammar , deterministic pushdown automaton , computer science , automaton , discrete mathematics , mathematics , theoretical computer science , programming language , automata theory , parsing , context free grammar , tree adjoining grammar , nondeterministic finite automaton

Games given by transition graphs of pushdown processes are considered. It is shown that if there is a winning strategy in such a game then there is a winning strategy that is realized by a pushdown process. This fact turns out to be connected with the model checking problem for the pushdown automata and the propositional mu-calculus. It is shown that this model checking problem is DEXPTIME-complete.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research