Abstract
We consider two-player parity games played on transition graphs of higher order pushdown automata. They are “game-equivalent” to a kind of model-checking game played on graphs of the infinite hierarchy introduced recently by Caucal. Then in this hierarchy we show how to reduce a game to a graph of lower level. This leads to an effective solution and a construction of the winning strategies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
T. Cachat, Symbolic strategy synthesis for games on pushdown graphs, ICALP’02, LNCS 2380, pp. 704–715, 2002.
T. Cachat, Uniform solution of parity games on prefix-recognizable graphs, INFINITY 2002, ENTCS 68(6), 2002.
T. Cachat, Two-way tree automata solving pushdown games, ch. 17 in W. THOMASAND T. WILKE eds., Automata, Logics, and Infinite Games, A Guide to Current Research, LNCS 2500, 2002 [11].
D. Caucal, On infinite transition graphs having a decidable monadic theory, ICALP’96, LNCS 1099, pp. 194–205, 1996.
D. Caucal, On infinite terms having a decidable monadic theory, MFCS’02, LNCS 2420, pp. 165–176, 2002.
D. Caucal, O. Burkart, F. Moller and B. Steffen, Verification on infinite structures, Handbook of process algebra, Ch. 9, pp. 545–623, Elsevier, 2001.
B. Courcelle and I. Walukiewicz, Monadic second-order logic, graph converings and unfoldings of transition systems, Annals of Pure and Applied Logic 92-1, pp. 35–62, 1998.
E. A. Emerson and C. S. Jutla, Tree automata, mu-calculus and determinacy, FoCS’91, IEEE Computer Society Press, pp. 368–377, 1991.
J. Engelfriet, Iterated push-down automata, 15th STOC, pp. 365–373, 1983.
J. Esparza, D. Hansel, P. Rossmanith and S. Schwoon, Efficient algorithm for model checking pushdown systems, Technische Universität München, 2000.
E. Grädel, W. Thomas and T. Wilke eds., Automata, Logics, and Infinite Games, A Guide to Current Research, LNCS 2500, 2002.
E. Grädel and I. Walukiewicz, Guarded fixed point logic, LICS’ 99, IEEE Computer Society Press, pp. 45–54, 1999.
T. Knapik, D. Niwinski and P. UrzyczynHigher-order pushdown trees are easy, FoSSaCS’02, LNCS 2303, pp. 205–222, 2002.
O. Kupferman, M. Y. Vardi and N. Piterman, Model checking linear properties of prefix-recognizable systems, CAV’02, LNCS 2404, pp. 371–385.
O. Kupferman and M. Y. Vardi, An automata-theoretic approach to reasoning about infinite-state systems, CAV’00, LNCS 1855, 2000.
W. Thomas, Languages, Automata, and Logic, Handbook of formal language theory, vol. III, pp. 389–455, Springer-Verlag, 1997.
M. Y. Vardi, Reasoning about the past with two-way automata., ICALP’98, LNCS 1443, pp. 628–641, 1998.
I. Walukiewicz, Pushdown processes: games and model checking, CAV’96, LNCS 1102, pp. 62–74, 1996. Full version in Information and Computation 164, pp. 234–263, 2001.
I. Walukiewicz, Monadic second order logic on tree-like structures, STACS’96, LNCS 1046, pp. 401–414. Full version in TCS 275 (2002), no. 1–2, pp. 311–346.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cachat, T. (2003). Higher Order Pushdown Automata, the Caucal Hierarchy of Graphs and Parity Games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds) Automata, Languages and Programming. ICALP 2003. Lecture Notes in Computer Science, vol 2719. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45061-0_45
Download citation
DOI: https://doi.org/10.1007/3-540-45061-0_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40493-4
Online ISBN: 978-3-540-45061-0
eBook Packages: Springer Book Archive