Abstract
One source of complexity in the μ-calculus is its ability to specify an unbounded number of switches between universal (AX) and existential (EX) branching modes. We therefore study the problems of satisfiability, validity, model checking, and implication for the universal and existential fragments of the μ-calculus, in which only one branching mode is allowed. The universal fragment is rich enough to express most specifications of interest, and therefore improved algorithms are of practical importance. We show that while the satisfiability and validity problems become indeed simpler for the existential and universal fragments, this is, unfortunately, not the case for model checking and implication. We also show the corresponding results for the alternationfree fragment of the μ-calculus, where no alternations between least and greatest fixed points are allowed. Our results imply that efforts to find a polynomial-time model-checking algorithm for the μ-calculus can be replaced by efforts to find such an algorithm for the universal or existential fragment.
This work was supported in part by NSF grant CCR-9988172, the AFOSR MURI grant F49620-00-1-0327, and a Microsoft Research Fellowship.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
B. Banieqbal and H. Barringer. Temporal logic with fixed points. Temporal Logic in Specification, LNCS 398, pages 62–74. Springer-Verlag, 1987.
J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992.
E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, LNCS 131, pages 52–71. Springer-Verlag, 1981.
E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Trans. on Programming Languages and Systems, 8(2):244–263, 1986.
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal μ-calculus. Formal Methods in System Design, 2:121–147, 1993.
M. Dam. CTL. and ECTL. as fragments of the modal μ-calculus. Theoretical Computer Science, 126:77–96, 1994.
E. Emerson and J. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151–178, 1986.
E. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. Foundations of Computer Science, pages 328–337. IEEE Press, 1988.
E. Emerson and C. Jutla. Tree automata, μ-calculus and determinacy. In Proc. Foundations of Computer Science, pages 368–377. IEEE Press, 1991.
E. Emerson, C. Jutla, and A. Sistla. On model-checking for fragments of μ-calculus. In Computer Aided Verification, LNCS 697, pages 385–396. Springer-Verlag, 1993.
E. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional μ-calculus. In Proc. Logic in Computer Science, pages 267–278. 1986.
M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194–211, 1979.
R. Greenlaw, H. Hoover, and W. Ruzzo. Limits of Parallel Computation. Oxford University Press, 1995.
O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843–871, 1994.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137–161, 1985.
N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384–406, 1981.
D. Janin and I. Walukiewicz. On the expressive completeness of the propositional μ-calculus with respect to the monadic second-order logic. In Concurrency Theory, LNCS 1119, pages 263–277. Springer-Verlag, 1996.
M. Jurdzinski. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters, 68(3):119–124, 1998.
M. Jurdzinski. Small progress measures for solving parity games. In Theoretical Aspects of Computer Science, LNCS 1770, pages 290–301. Springer-Verlag, 2000.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
D. Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):333–354, 1988.
O. Kupferman and M. Vardi. An automata-theoretic approach to modular model checking. ACM Trans. on Programming Languages and Systems, 22:87–128, 2000.
O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312–360, 2000.
R. Kurshan. FormalCheck User’s Manual. Cadence Design Inc., 1998.
D. Long, A. Brown, E. Clarke, S. Jha, and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Computer Aided Verification, LNCS 818, pages 338–350. Springer-Verlag, 1994.
K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123–144. Springer-Verlag, 1985.
A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. Principles of Programming Languages, pages 179–190. ACM Press, 1989.
P. Ramadge and W. Wonham. The control of discrete-event systems. IEEE Trans. on Control Theory, 77:81–98, 1989.
H. Seidl. Fast and simple nested fixpoints. Information Processing Letters, 59(6):303–308, 1996.
M. Vardi. A temporal fixpoint calculus. In Proc. Principles of Programming Languages, pages 250–259. ACM Press, 1988.
M. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc. Theory of Computing, pages 240–251. ACM Press, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henzinger, T.A., Kupferman, O., Majumdar, R. (2003). On the Universal and Existential Fragments of the μ-Calculus. In: Garavel, H., Hatcliff, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2003. Lecture Notes in Computer Science, vol 2619. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36577-X_5
Download citation
DOI: https://doi.org/10.1007/3-540-36577-X_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00898-9
Online ISBN: 978-3-540-36577-8
eBook Packages: Springer Book Archive