Abstract
One of the open questions about the modal mu-calculus is whether the alternation hierarchy collapses; that is, whether all modal fix-point properties can be expressed with only a few alternations of least and greatest fix-points. In this paper, we resolve this question by showing that the hierarchy does not collapse.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
H. R. Andersen, Verification of Temporal Properties of Concurrent Systems, DAIMI PB — 445, Computer Science Dept, Aarhus University (1993).
A. Arnold and D. Niwinski, Fixed point characterization of Büchi automata on infinite trees. J. Inf. Process. Cybern., EIK 26, 451–459 (1990).
J. Barwise, Admissible sets and structures, Springer-Verlag, Berlin/New York (1975).
J. C. Bradfield, Verifying Temporal Properties of Systems. Birkhäuser, Boston, Mass. 0-817-63625-0 (1991).
J. C. Bradfield, On the expressivity of the modal mu-calculus. Proc. STACS '96, LNCS 1046, 479–490 (1996).
J. C. Bradfield, The modal mu-calculus alternation hierarchy is strict. Online via the Web page http://www.dcs.ed.ac.uk/home/jcb/ or by ftp at ftp://ftp.dcs.ed.ac.uk/export/jcb/Research/ althi.ps.gz.
E. A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. Extended version from FOCS '88. (1988).
E. A. Emerson and C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus. Proc. First IEEE Symp. on Logic in Computer Science 267–278 (1986).
R. Kaivola, On modal mu-calculus and Büchi tree automata. Inf. Proc. Letters 54 17–22 (1995).
D. Kozen, Results on the propositional mu-calculus. Theoret. Comput. Sci. 27 333–354 (1983).
G. Lenzi, A hierarchy theorem for the mu-calculus. To appear in Proc. ICALP '96.
D. Long, A. Browne, E. Clarke, S. Jha and W. Marrero, An improved algorithm for the evaluation of fixpoint expressions. Proc. CAV '94, LNCS 818 338–350 (1994).
R. S. Lubarsky, Μ-definable sets of integers, J. Symbolic Logic 58 291–313 (1993).
Y. N. Moschovakis, Elementary induction on abstract structures, North-Holland, Amsterdam (1974).
D. Niwiński, On fixed point clones. Proc. 13th ICALP, LNCS 226 464–473 (1986).
M. O. Rabin, Weakly definable relations and special automata, in Y. Bar-Hillel (ed.) Mathematical Logic and Foundations of Set Theory, North-Holland, Amsterdam (1970), 1–23.
W. Richter and P. Aczel, Inductive definitions and reflecting properties of admissible ordinals, in Fenstad and Hinman (ed.), Generalized recursion theory, North-Holland, Amsterdam 301–381 (1974).
R. S. Streett and E. A. Emerson, An automata theoretic decision procedure for the propositional mu-calculus. Information and Computation 81 249–264 (1989).
C. Stirling, Local model checking games. Proc. Concur '95, LNCS 962, 1–11 (1995).
M. Takashashi, The greatest fixed-points and rational omega-tree languages. Theor. Comput. Sci. 44 259–274 (1986).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bradfield, J.C. (1996). The modal mu-calculus alternation hierarchy is strict. In: Montanari, U., Sassone, V. (eds) CONCUR '96: Concurrency Theory. CONCUR 1996. Lecture Notes in Computer Science, vol 1119. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61604-7_58
Download citation
DOI: https://doi.org/10.1007/3-540-61604-7_58
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61604-7
Online ISBN: 978-3-540-70625-0
eBook Packages: Springer Book Archive