×

zbMATH — the first resource for mathematics

The modal mu-calculus alternation hierarchy is strict. (English) Zbl 0915.03017
Summary: One of the open questions about the modal mu-calculus is whether the alternation hierarchy collapses; that is, whether all modal fixpoint properties can be expressed with only a few alternations of least and greatest fixpoints. In this paper, we resolve this question by showing that the hierarchy does not collapse.

MSC:
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andersen, H.R., Verification of temporal properties of concurrent systems, ()
[2] Arnold, A.; Niwinski, D., Fixed point characterization of Büchi automata on infinite trees, J. inform. process. cybernet. EIK, 26, 451-459, (1990) · Zbl 0721.68040
[3] Barwise, J., Admissible sets and structures, (1975), Springer Berlin · Zbl 0316.02047
[4] Bekič, H., Definable operations in general algebras, and the theory of automata and flow charts, () · Zbl 0548.68004
[5] Bradfield, J.C., Verifying temporal properties of systems, (1991), Birkhäuser Boston
[6] Bradfield, J.C., On the expressivity of the modal mu-calculus, (), 479-490 · Zbl 1379.68155
[7] Bradfield, J.C., The modal mu-calculus alternation hierarchy is strict, (), 233-246 · Zbl 0915.03017
[8] Emerson, E.A.; Jutla, C.; Sistla, A.P., On model-checking for fragments of μ-calculus, (), 385-396 · Zbl 0973.68120
[9] Emerson, E.A.; Lei, C.-L., Efficient model checking in fragments of the propositional mu-calculus, (), 267-278
[10] Kaivola, R., On modal mu-calculus and Büchi tree automata, Inform. process. lett., 54, 17-22, (1995) · Zbl 1004.68530
[11] Kozen, D., Results on the propositional mu-calculus, Theoret. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007
[12] Kozen, D., A finite model theorem for the propositional μ-calculus, Studia logica, 47, 233-241, (1988) · Zbl 0667.03019
[13] Lenzi, G., A hierarchy theorem for the mu-calculus, (), 87-109 · Zbl 1045.03516
[14] Long, D.; Browne, A.; Clarke, E.; Jha, S.; Marrero, W., An improved algorithm for the evaluation of fixpoint expressions, (), 338-350 · Zbl 0901.68118
[15] Lubarsky, R.S., Μ-definable sets of integers, J. symbolic logic, 58, 291-313, (1993) · Zbl 0776.03022
[16] R.S. Lubarsky, personal communication, 1997.
[17] Mader, A., Verification of modal properties using Boolean equation systems, ()
[18] Moschovakis, Y.N., Elementary induction on abstract structures, (1974), North-Holland Amsterdam · Zbl 0307.02003
[19] Niwiński, D., On fixed point clones, (), 464-473
[20] Rabin, M.O., Weakly definable relations and special automata, (), 1-23 · Zbl 0214.02208
[21] Richter, W.; Aczel, P., Inductive definitions and reflecting properties of admissible ordinals, (), 301-381
[22] Stirling, C., Local model checking games, (), 1-11
[23] Stirling, C.P., Modal and temporal logics, (), 477-563
[24] Streett, R.S.; Emerson, E.A., An automata theoretic decision procedure for the propositional mu-calculus, Inform. and comput., 81, 249-264, (1989) · Zbl 0671.03023
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.