Abstract
The purpose of this tutorial is to survey the essentials of the algorithmic theory of infinite games, its role in automatic program synthesis and verification, and some challenges of current research.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
E. Asarin, O. Maler, A. Pnueli, J. Sifakis, Controller Synthesis for Timed Automata, Proc. IFAC Symposium on System Structure and Control, 469–474, Elsevier, Amsterdam 1998.
E. Asarin, O. Maler, As Soon as Possible: Time Optimal Control for Timed Automata, Hybrid Systems (F. Vaandrager et al. Eds.): Computation and Control, Lecture Notes in Computer Science 1569 (1999), 19–30.
E. A. Emerson, C. S. Jutla, A. P. Sistla, On model checking for fragments of μ-calculus, in: CAV’93 (C. Coucoubetis, Ed), Lecture Notes in Computer Science 697 (1993), 385–396.
S. Dziembowski, M. Jurdzinski, I. Walukiewicz, How much memory is needed to win infinite games?, Proc. 12th IEEE Symp. on Logic in Computer Science, 1997, 99–110.
M. Jurdzinski, Deciding the winner in parity games is in UP∩co-UP, Inform. Processing Letters 68 (1998), 119–124.
O. Kupferman, M. Y. Vardi, Church’s problem revisited, Bull. Symb. Logic 5 (1999), 245–263.
Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Programs, Springer-Verlag, Berlin-Heidelberg-New York 1992.
P. Madhusudan, P. S. Thiagarajan: Distributed Controller Synthesis for Local Specifications. Proc. ICALP 2001, Lecture Notes in Computer Science 2076 (2001), 396–407.
A. Pnueli, R. Rosner, Distributed reactive systems are hard to synthesize, Proc. 31st IEEE Symp. on Foundation of Computer Science, 1990, 746–757.
C. Stirling, Modal and Temporal Properties of Processes, Springer-Verlag, New York 2001.
W. Thomas, On the synthesis of strategies in infinite games, in: STACS’95 (E. W. Mayr, C. Puech, Eds.), Lecture Notes in Computer Science 900 (1995), 1–13.
W. Thomas, Languages, automata, and logic, in: Handbook of Formal Languages (G. Rozenberg, A. Salomaa, Eds.), Vol. 3, Springer-Verlag, Berlin Heidelberg 1997.
J. Vöge, M. Jurdzinski, A strategy improvement algorithm for solving parity games, CAV 2000, Lect. Notes in Computer Science 1855 (2000), 202–215.
I. Walukiewicz, Pushdown processes: games and model-checking, Information and Computation 157 (2000), 234–263.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thomas, W. (2002). Infinite Games and Verification. In: Brinksma, E., Larsen, K.G. (eds) Computer Aided Verification. CAV 2002. Lecture Notes in Computer Science, vol 2404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45657-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-45657-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43997-4
Online ISBN: 978-3-540-45657-5
eBook Packages: Springer Book Archive