Abstract
In this survey I would like to present some connections between the μ-calculus and games, more specifically games of possibly infinite duration played on labeled graphs. A fundamental connection was established by Emerson and Jutla [12] and subsequently developed by several authors [13, 36, 42, 1]. Essentially, the result is that any formula of the μ-calculus expresses the existence of a strategy in a certain game. The idea of such a correspondence can be traced back to Büchi and McNaughton who observed a similar property of monadic second order arithmetic (see [10]).
Supported by Polish KBN grant No. 7 T11C 027 20
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
A. Arnold. A selection property of the boolean μ-calculus and some of its applications. RAIRO-Theoretical Informatics and Applications, 31:371–384, 1997.
A. Arnold. The μ-calculus alternation-depth hierarchy is strict on binary trees. RAIRO-Theoretical Informatics and Applications, 33:329–339, 1999.
A. Arnold and D. Niwiński. Fixed point characterization of weak monadic logic definable sets of trees. In M. Nivat and A. Podelski, editors, Tree automata and Languages, pages 159–188. Elsevier, 1992.
A. Arnold and D. Niwiński. Rudiments of μ-Calculus. Elsevier Science, Studies in Logic and the Foundations of Mathematics, 146, North-Holland, Amsterdam, 2001.
J. Bernet, D. Janin and I. Walukiewicz. Permissive strategies: from parity games to safety games. Theoretical Informatics and Applications (RAIRO), to appear.
J. C. Bradfield. The modal mu-calculus alternation hierarchy is strict. Theoretical Computer Science, 195:133–153, 1997.
J. C. Bradfield. Simplifying the modal mu-calculus alternation hierarchy. In M. Morvan, C. Meinel, and D. Krob, editors, Proc. STACS’ 98, pages 39–49. Lect. Notes Comput. Sci. 1373, 1998.
J. Bradfield and C. Stirling. Modal logics and mu-calculi: an introduction. In J. Bergstra, A. Ponse and S. Smolka, editors, Handbook of Process Algebra, pages 293–332. Elsevier, North-Holland, 2001.
A. Browne, E.M. Clarke, S. Jha, D.E. Long, and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. Theoretical Computer Science, 178:237–255, 1997.
J. R. Büchi. Using determinacy to eliminate quantifiers. In M. Karpinski, editor, Fundamentals of Computation Theory, volume 56, pages 367–378. Lect. Notes Comput. Sci., 1977.
R. Cleaveland, M. Klein and B. Steffen. Faster model checking for the modal mu-calculus. In G.v. Bochmann and D. Probst, editors, Computer-Aided Verification (CAV’ 92), volume 663, pages 410–422, Lect. Notes Comput. Sci., 1992.
E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. In Proceedings 32th Annual IEEE Symp. on Foundations of Comput. Sci., pages 368–377. IEEE Computer Society Press, 1991.
E. A. Emerson, C.S. Jutla, and A. P. Sistla. On model-checking for fragments of the μ-calculus. In C. Courcoubetis, editor, Computer Aided Verification, pages 385–396. Lect. Notes Comput. Sci. 697, 1993.
D. Gale and F. M. Stewart. Infinite games with perfect information. Ann. of Math. Studies 28 (Contribution to the Theory of Games II), pages 245–266, Princeton, 1953.
Y. Gurevich. The logic in computer science column. Bull. EATCS, 38, pages 93–100, 1989.
Y. Gurevich and L. Harrington. Trees, automata and games. In Proc. 14th ACM Symp. on the Theory of Computing, pages 60–65, 1982.
P. G. Hinman. Recursion-Theoretic Hierarchies. Perspective in Mathematical Logic, Springer-Verlag, 1978.
M. Jurdziński. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters, 68:119–124, 1998.
M. Jurdziński. Small progress measures for solving parity games. In Proc. 17th Symp. Theoretical Aspects of Computer Science, volume 1770, pages 290–301. Lect. Notes Comput. Sci., 2000.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
G. Lenzi. A hierarchy theorem for the mu-calculus. In F. Meyer auf der Heide and B. Monien, editors, Proc. ICALP’ 96, pages 87–109. Lect. Notes Comput. Sci. 1099, 1996.
R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.
D.A. Martin. Borel determinacy. Annals of Math. 102, pages 363–371, 1975.
R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65:149–184, 1993.
A.W. Mostowski. Games with forbidden positions. Technical Report Technical Report 78, Instytut Matematyki, University of Gdansk, 1991.
A.A. Muchnik. Games on infinite trees and automata with dead-ends: a new proof of the decidability of the monadic theory of two successors (in Russian). Semiotics and Information, 24:17–40, 1984.
D. E. Muller and P. E. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267–276, 1987.
J. Mycielski. Games with perfect information. In R. J. Aumann and S. Hart, editors, Handbook of Game Theory with Economic Applications, volume 1, pages 41–70. North-Holland, 1992.
D. Niwiński. On fixed point clones. In L. Kott, editor, Proc. 13th ICALP, pages 464–473. Lect. Notes Comput. Sci. 226, 1986.
D. Niwiński. Fixed points vs. infinite generation. In Proc. 3rd IEEE Symp. on Logic in Comput. Sci., pages 402–409, 1988.
D. Niwiński. Fixed points characterization of infinite behaviour of finite state systems. Theoretical Computer Science, 189:1–69, 1997.
V. Petersson and S. Vorobyov. A randomized subexponential algorithm for parity games. Nordic Journal of Computing, 8:324–345, 2001.
A. Puri. Theory of Hybrid Systems and Discrete Event Systems. PhD thesis, College of Engineering, University of California, Berkeley, 1995.
M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Soc, 141:1–35, 1969.
H. Seidl. Fast and simple nested fixpoints. Information Processing Letters, 59:303–308, 1996.
C. Stirling. Local model checking games. In Proc. Concur’95, volume 962, pages 1–11, Lect. Notes Comput. Sci., 1995.
R. S. Streett and E. A. Emerson. An automaton theoretic decision procedure for the propositional μ-calculus. Information and Computation, 81:249–264, 1989.
W. Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, pages 389–455. Springer-Verlag, 1997.
J. Vöge and M. Jurdziński. A discrete strategy improvement algorithm for solving parity games. In Proc. CAV 2000, volume 1855, pages 202–215, Lect. Notes Comput. Sci., 2000.
K. Wagner. Eine topologische Charakterisierung einiger Klassen regulärer Folgenmengen. J. Inf. Process. Cybern. EIK, 13:473–487, 1977.
I. Walukiewicz. Monadic second-order logic on tree-like structures. In C. Puech and R. Reischuk, editors, Proc. STACS’ 96, pages 401–414. Lect. Notes Comput. Sci. 1046, 1996.
I. Walukiewicz. Pushdown processes: Games and model checking. Information and Computation, 164(2):234–263, 2001.
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
Niwiński, D. (2002). μ-Calculus via Games (Extended Abstract). In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-45793-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44240-0
Online ISBN: 978-3-540-45793-0
eBook Packages: Springer Book Archive