Abstract
We investigate the expressive power of Parikh's Game Logic interpreted in Kripke structures, and show that the syntactical alternation hierarchy of this logic is strict. This is done by encoding the winning condition for parity games of rank n. It follows that Game Logic is not captured by any finite level of the modal μ-calculus alternation hierarchy. Moreover, we can conclude that model checking for the μ-calculus is efficiently solvable iff this is possible for Game Logic
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Arnold, A. and D. NiwiŃski, Rudiments of μ-calculus, Studies in Logic 146. North Holland, 2001.
Bradfield, J. C., ‘The modal mu-calculus alternation hierarchy is strict'. Theoretical Computer Science 195(2):133-153, 1998.
Emerson, E. A., and C. S. Jutla. ‘Tree automata, mu-calculus and determinacy’, in 32nd Annual Symposium on Foundations of Computer Science, 368-377. IEEE, 1991.
Emerson, E. A., C. S. Jutla, and A. P. Sistla, ‘Model checking in fragments of mu-calculus’, in International Conference on Computer Aided Verification, LNCS 697:385-396. Springer-Verlag, 1993.
Emerson, E. A., ‘Model checking and the mu-calculus’, in N. Immerman and P. Kolaitis, (eds.), Descriptive Complexity and Finite Models, DIMACS: Series in Discrete Mathematics and Theoretical Computer Science 31. American Mathematical Society, 1997.
Janin, D., and I. Walukiewicz, ‘On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic’, in U. Montanari and V. Sassone, (eds.), Proceedings of the 7th International Conference on Concurrency Theory, CONCUR'96, LNCS 1119:263-277. Springer-Verlag, 1996.
Lenzi G., ‘A hierarchy theorem for the mu-calculus’, in F. Meyer auf der Heide and B. Monien, (eds.), Proceedings of the 23rd International Colloquium on Automata, Languages and Programming, ICALP '96, LNCS 1099:87-97. Springer-Verlag, 1996.
NiwiŃski D., and H. Seidl, ‘On distributive fixed-point expressions'. RAIRO Informatique Theorique, 33(4/5):427-446, 1999.
Parikh, R., ‘The logic of games and its applications'. Annals of discrete mathematics, 24:111-140, 1985.
Pauly, M., ‘Game constructions that are safe for bisimulation’, in J. Gerbrandy, M. Marx, M. de Rijke, and Y. Venema, (eds.), JFAK. Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday, CD-ROM http://turing.wins.uva.nl/~j50/cdrom/. Amsterdam University Press, 1999.
Pauly, M., ‘From Programs to Games: Invariance and Safety for Bisimulation’ in Proceedings of 14th Annual Conference of the European Association for Computer Science Logic CSL 2000, LNCS 1862:586-496. Springer-Verlag, 2000.
Pauly, M., Logic for Social Software. PhD thesis, University of Amsterdam, 2001.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Berwanger, D. Game Logic is Strong Enough for Parity Games. Studia Logica 75, 205–219 (2003). https://doi.org/10.1023/A:1027358927272
Issue Date:
DOI: https://doi.org/10.1023/A:1027358927272