Abstract
We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice.
This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the “right” model checking games for IFP by a) giving a translation of formulae φ and structures \(\cal A\) into simple games such that \(\cal A \models \phi\) if, and only if, Player 0 wins the corresponding game and b) showing that the winner of simple backtracking games can again be defined in IFP.
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
Dawar, A., Grädel, E., Kreutzer, S.: Inflationary fixed points in modal logic. ACM Transactions on Computational Logic, TOCL (2003) (accepted for publication)
Garey, M.R., Johnson, D.S.: Computers and Intractability. A Guide to the Theory of NP-Completeness. W. H. Freeman and company, New York (1979) ISBN 0-7167-1044-7
Grädel, E.: Finite model theory and descriptive complexity. In: Finite Model Theory and Its Applications, Springer, Heidelberg (2003) (to appear), See http://wwwmgi.informatik.rwth-aachen.de/Publications/pub/graedel/Gr-FMTbook.ps
Grädel, E., Kreutzer, S.: Will deflation lead to depletion? On non-monotone fixed-point inductions. In: IEEE Symp. of Logic in Computer Science, LICS (2003)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Kreutzer, S.: Expressive equivalence of least and inflationary fixed-point logic. In: 17th Symp. on Logic in Computer Science (LICS), pp. 403 – 413 (2002)
Martin, D.: Borel determinacy. Annals of Mathematics 102, 336–371 (1975)
Stirling, C.: Bisimulation, model checking and other games. Notes for the Mathfit instructional meeting on games and computation, Edinburgh (1997)
Walukiewicz, I.: Monadic second order logic on tree-like structures. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 401–414. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dawar, A., Grädel, E., Kreutzer, S. (2004). Backtracking Games and Inflationary Fixed Points. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds) Automata, Languages and Programming. ICALP 2004. Lecture Notes in Computer Science, vol 3142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27836-8_37
Download citation
DOI: https://doi.org/10.1007/978-3-540-27836-8_37
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22849-3
Online ISBN: 978-3-540-27836-8
eBook Packages: Springer Book Archive