Abstract
We analyse the complexity of the sets of states, in certain classes of infinite systems, that satisfy formulae of the modal mu-calculus. Improving on some of our earlier results, we establish a strong upper bound (namely Δ 12 ). We also establish various lower bounds and restricted upper bounds, incidentally providing another proof that the mu-calculus alternation hierarchy does not collapse at level 2.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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. C. Bradfield, Verifying Temporal Properties of Systems. Birkhäuser, Boston, Mass. ISBN 0-8176-3625-0 (1991).
J. C. Bradfield, A proof assistant for symbolic model-checking. Proc. CAV '92. LNCS 663 316–329 (1993).
J. C. Bradfield, On the expressivity of the modal mu-calculus, Technical Report ECS-LFCS-95-338, LFCS, University of Edinburgh (1995). On-line via http://www.dcs.ed.ac.uk/home/jcb/.
J. C. Bradfield and C. Stirling, Local model checking for infinite state spaces. Theoret. Comput. Sci. 96 157–174 (1992).
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).
J. Esparza, On the decidability of model-checking for several μ-calculi and Petri nets, Proc. CAAP '94, LNCS 787 115–129 (1994).
J. Esparza and M. Nielsen, Decidability issues for Petri nets — a survey, J. Inform. Process. Cybernet. 30 143–160 (1994).
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).
K. Larsen, Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theoret. Comput. Sci. 72 265–288 (1990).
Y. N. Moschovakis, Descriptive set theory. North-Holland, Amsterdam & New York (1980).
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.
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). On the expressivity of the modal mu-calculus. In: Puech, C., Reischuk, R. (eds) STACS 96. STACS 1996. Lecture Notes in Computer Science, vol 1046. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60922-9_39
Download citation
DOI: https://doi.org/10.1007/3-540-60922-9_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60922-3
Online ISBN: 978-3-540-49723-3
eBook Packages: Springer Book Archive