Abstract
We define Ehrenfeucht-FraÏssé games which exactly capture the expressive power of the extremal fixed point operators of modal mu-calculus. The resulting games have significance, we believe, within and outside of concurrency theory. On the one hand they naturally extend the iterative bisimulation games associated with Hennessy-Milner logic, and on the other hand they offer deeper insight into the logical role of fixed points. For this purpose we also define second-order propositional modal logic to contrast fixed points and second-order quantifiers.
Chapter PDF
references
Abramsky, S., and Jagadeesan, R. (1994). Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59, 543–574.
Arnold, A., and Niwinski, D. (1990). Fixed point characterization of Büchi automata on infinite trees. J. Inf. Process. Cybern., EIK 26, 451–459.
Baeten, J. and Weijland, W. (1990). Process Algebra. Cambridge Tracts in Theoretical Computer Science, 18.
Bosse, U. (1992). An “Ehrenfeucht-FraÏssé game” for fixpoint and stratified fixpoint logic. Lecture Notes in Computer Science, 702, 100–114.
Bradfield, J. (1995). The modal mu-calculus alternation hierarchy is strict. Submitted for publication.
Condon, A. (1992). The complexity of stochastic games. Information and Computation, 96, 203–224.
Emerson, E., and Jutla, C. (1988). The complexity of tree automata and logics of programs. Extended version from FOCS '88.
Fagin, R., Stockmeyer, L., and Vardi, M. (1995). On monadic NP vs monadic co-NP. Information and Computation, 120, 78–92.
Hodges, W. (1993). Model Theory. Cambridge University Press.
Immermann, N. (1986). Relational queries computable in polynomial time. Information and Control, 68, 86–104.
Kaivola, R. (1995). On modal mu-calculus and Büchi tree automata. Information Processing Letters, 54, 17–22.
Kozen, D. (1983). Results on the propositional mu-calculus. Theoretical Computer Science, 27, 333–354.
Milner, R. (1989). Communication and Concurrency. Prentice Hall.
Moschovakis, Y. (1989). A game theoretic modelling of concurrency. Procs. 4th IEEE Symposium on Logic in Computer Science.
Nielsen, M. and Clausen, C. (1994). Bisimulations, games and logic. Lecture Notes in Computer Science, 812, 289–306.
Stirling, C. (1993). Modal and temporal logics for processes. Notes for Summer School in Logical Methods in Concurrency. Department of Computer Science, Aarhus University.
Stirling, C. (1995). Local model checking games. Lecture Notes in Computer Science, 962, 1–11.
Thomas, W. (1993). On the Ehrenfeucht-FraÏssé game in theoretical computer science. Lecture Notes in Computer Science, 668.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stirling, C. (1996). Games and modal mu-calculus. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_51
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive