Open AccessPushdown 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.