×

zbMATH — the first resource for mathematics

Pushdown processes: Games and model-checking. (English) Zbl 1003.68072
Summary: A pushdown game is a two player perfect information infinite game on a transition graph of a pushdown automaton. A winning condition in such a game is defined in terms of states appearing infinitely often in the play. It is shown that if there is a winning strategy in a pushdown game then there is a winning strategy realized by a pushdown automaton. An EXPTIME procedure for finding a winner in a pushdown game is presented. The procedure is then used to solve the model-checking problem for the pushdown processes and the propositional \(\mu\)-calculus. The problem is shown to be DEXPTIME-complete.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q45 Formal languages and automata
91A05 2-person games
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bergstra, J.; Klop, J., Process theory based on bisimulation semantics, () · Zbl 0683.68066
[2] Burkart, O.; Steffen, B., Model checking for context-free processes, Concur ’92, Lecture notes in computer science, 630, (1992), p. 123-137
[3] Burkart, O.; Steffen, B., Pushdown processes: parallel composition and model checking, Concur ’94, Lecture notes in computer science, 836, (1994)
[4] Caucal, D.; Monfort, R., On the transition graphs of automata and grammars, Graph-theoretic concepts in computer science, Lecture notes in computer science, 484, (1991)
[5] Chandra, A.K.; Kozen, D.C.; Stockmeyer, L.J., Alternation, J. ACM, 28, 114-133, (1981) · Zbl 0473.68043
[6] Christiensen, S.; Huttel, H., Deciding issues for infinite-state processes—a survey, Bulletin of EATCS, 51, 156-166, (October 1993)
[7] Courcelle, B, and, Walukiewicz, I, Monadic Second-Order Logic, Graphs and Unfoldings of Transition Systems, University of Aarhus, BRICS report, RS-95-44. Presented at CSL ’95, to appear in, Journal of Pure and Applied Logic.
[8] Emerson, E.A., Automata, tableaux and temporal logic, College conference on logic of programs, Lecture notes in computer science, 193, (1985), Springer-Verlag · Zbl 0603.03005
[9] Emerson, E.A.; Jutla, C.; Sistla, A., On model-checking for fragments of μ-calculus, Cav ’93, Lecture notes in computer science, 697, (1993), p. 385-396
[10] Emerson, E.A.; Jutla, C.S., Tree automata, mu-calculus and determinacy, Proc. FOCS 91, (1991), p. 368-377
[11] Emerson, E.A.; Lei, C., Efficient model checking in fragments of propositional mu-calculus, First IEEE symposium on logic in computer science, (1986), p. 267-278
[12] Esparza, J.; Kiehn, A., On the model checking problem for branching time logics and basic parallel processes, Cav ’95, Lecture notes in computer science, 939, (1995), p. 353-366
[13] Gurevich, Y.; Harrington, L., Trees, automata and games, 14th symp. on theory of computations, ACM, (1982), p. 60-65
[14] Klarlund, N., Progress measures, immediate determinacy and a subset construction for tree automata, Lics ’92, (1992), p. 382-393
[15] Long, D.E.; Browne, A.; Clarke, E.M.; Jha, S.; Marrero, W.R., An improved algorithms for the evaluation of fixpoint expressions, Cav ’94, Lecture notes in computer science, 818, (1994), p. 338-350
[16] Mostowski, A.W., Regular expressions for infinite trees and a standard form of automata, (), 157-168 · Zbl 0612.68046
[17] Mostowski, A.W., Technical report, (1991)
[18] Muller, D.; Schupp, P., The theory of ends, pushdown automata and second-order logic, Theor. comp. sci., 37, 51-75, (1985) · Zbl 0605.03005
[19] Nerode, A.; Yakhnis, A.; Yakhnis, S., Concurrent programs as strategies in games, () · Zbl 0746.68046
[20] Niwiński, D., Fixed point characterization of infinite behaviour of finite state systems, Theor. comp. sci., 189, 1-69, (1997) · Zbl 0893.68102
[21] Niwiński, D.; Walukiewicz, I., Games for μ-calculus, Theor. comp. sci., 163, 99-116, (1996) · Zbl 0872.03017
[22] Seibert, S., Effektive strategiekonstruktion für gale – stewart – spiele auf trasitions graphen, (1996), Kiel University
[23] Seidl, H., Fast and simple nested fixpoints, Inform. proc. lett., 59, 303-308, (1996) · Zbl 0900.68458
[24] Streett, R.S.; Emerson, E.A., An automata theoretic procedure for the propositional mu-calculus, Inform. and comput., 81, 249-264, (1989) · Zbl 0671.03023
[25] Thomas, W., On the synthesis of strategies in infinite games, Stacs ’95, Lecture notes in computer science, 900, (1995), p. 1-13 · Zbl 1379.68233
[26] Thomas, W., Languages, automata, and logic, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.