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) |
Keywords:
temporal logic; expressivity; modal mu-calculus; alternation hierarchy; fixpoint propertiesReferences:
| [1] | Andersen, H. R., Verification of Temporal Properties of Concurrent Systems, (DAIMI PB-445 (1993), Computer Science Dept, Aarhus University) |
| [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: Springer Berlin · Zbl 0316.02047 |
| [4] | Bekič, H., Definable operations in general algebras, and the theory of automata and flow charts, (Jones, C. B., Programming Languages and their Definition. Programming Languages and their Definition, Lecture Notes in Computer Science, vol. 177 (1984), Springer: Springer Berlin) · Zbl 0548.68004 |
| [5] | Bradfield, J. C., Verifying Temporal Properties of Systems (1991), Birkhäuser: Birkhäuser Boston |
| [6] | Bradfield, J. C., On the expressivity of the modal mu-calculus, (Puech, C.; Reischuk, R., Proc. STACS ’96. Proc. STACS ’96, Lecture Notes in Computer Science, vol. 1046 (1996), Springer: Springer Berlin), 479-490 · Zbl 1379.68155 |
| [7] | Bradfield, J. C., The modal mu-calculus alternation hierarchy is strict, (Montanari, U.; Sassone, V., Proc. CONCUR ’96. Proc. CONCUR ’96, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: Springer Berlin), 233-246 · Zbl 0915.03017 |
| [8] | Emerson, E. A.; Jutla, C.; Sistla, A. P., On model-checking for fragments of μ-calculus, (Courcoubetis, C., Proc. CAV ’93. Proc. CAV ’93, Lecture Notes in Computer Science, vol. 697 (1993), Springer: Springer Berlin), 385-396 · Zbl 0973.68120 |
| [9] | Emerson, E. A.; Lei, C.-L., Efficient model checking in fragments of the propositional mu-calculus, (Proc. 1st LICS, IEEE. Proc. 1st LICS, IEEE, Los Alamitos, CA (1986)), 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, (auf der Heide, F. Meyer; Monien, B., Proc. ICALP ’96. Proc. ICALP ’96, Lecture Notes in Computer Science, vol. 1099 (1996), Springer: Springer Berlin), 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, (Dill, D. L., Proc. CAV ’94. Proc. CAV ’94, Lecture Notes in Computer Science, vol. 818 (1994), Springer: Springer Berlin), 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.; R.S. Lubarsky, personal communication, 1997. |
| [17] | Mader, A., Verification of modal properties using boolean equation systems, (Doctoral Dissertation (1996), Institut für Informatik, Technische Universität München) |
| [18] | Moschovakis, Y. N., Elementary Induction on Abstract Structures (1974), North-Holland: North-Holland Amsterdam · Zbl 0307.02003 |
| [19] | Niwiński, D., On fixed point clones, (Kott, L., Proc. 13th ICALP. Proc. 13th ICALP, Lecture Notes in Computer Science, vol. 226 (1986), Springer: Springer Berlin), 464-473 · Zbl 0596.68036 |
| [20] | Rabin, M. O., Weakly definable relations and special automata, (Bar-Hillel, Y., Mathematical Logic and Foundations of Set Theory (1970), North-Holland: North-Holland Amsterdam), 1-23 · Zbl 0214.02208 |
| [21] | Richter, W.; Aczel, P., Inductive definitions and reflecting properties of admissible ordinals, (Fenstad, J. E.; Hinman, P. G., Generalized Recursion Theory (1974), North-Holland: North-Holland Amsterdam), 301-381 · Zbl 0318.02042 |
| [22] | Stirling, C., Local model checking games, (Lee, I.; Smolka, S. A., Proc. Concur ’95. Proc. Concur ’95, Lecture Notes in Computer Science, vol. 962 (1995), Springer: Springer Berlin), 1-11 |
| [23] | Stirling, C. P., Modal and temporal logics, (Abramsky, S.; Gabbay, D.; Maibaum, T., Handbook of Logic in Computer Science, vol. 2 (1991), Oxford University Press: Oxford University Press Oxford), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
