Polynomial Approximations for Model Checking

  • Nikolai V. Shilov
  • Natalya O. Garanina
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)


The μ-Calculus of D. Kozen (1983) is a very powerful propositional program logic with fixpoints. It is widely used for specification and verification. Model checking is a very popular automatic approach for verification of specifications of finite state systems. The most efficient algorithms that have been developed so far for model checking of the μ-Calculus in finite state systems have exponential upper bounds. A. Emerson, C. Jutla, and P. Sistla studied (1993) the first fragment of the μ-Calculus that permits arbitrary nesting and alternations of fixpoints, and polynomial model checking in finite state systems. In contrast we study lower and upper approximations for model checking that are computable in polynomial time, and that can give correct semantics in finite models for formulae with arbitrary nesting and alternations. A.Emerson, C.Jutla, and P.Sistla proved also that the model checking problem for the μ-Calculus in finite state systems is in \(\mathcal{NP}\cap\) co- \(\mathcal{NP}\). We develop another proof (that we believe is a new one) as a by-product of our study.


μ-Calculus model checking complexity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arnold, A., Niwinski, D.: Rudiments of μ-calculus. North-Holland, Amsterdam (2001)Google Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  3. 3.
    Cleaveland, R., Klain, M., Steffen, B.: Faster Model-Checking for Mu-Calculus. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 410–422. Springer, Heidelberg (1993)Google Scholar
  4. 4.
    Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of Mu- Calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)Google Scholar
  5. 5.
    Fagin, R.: Generalized First-Order Spectra and Polynomial-Time Recognizable Sets. In: Complexity of Computations, SIAM-AMS Proc., vol. 7, pp. 27–41 (1974)Google Scholar
  6. 6.
    Immerman, N.: Descriptive Complexity: A Logician’s Approach to Computation. Notices of the American Mathematical Society 42(10), 1127–1133 (1995)zbMATHMathSciNetGoogle Scholar
  7. 7.
    Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)zbMATHGoogle Scholar
  8. 8.
    Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27(3), 333–354 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Shilov, N.V., Yi, K.: How to find a coin: propositional program logics made easy. The Bulletin of the European Association for Theoretical Computer Science 75, 127–151 (2001)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Nikolai V. Shilov
    • 1
    • 2
  • Natalya O. Garanina
    • 2
  1. 1.Visiting Erskine FellowUniversity of CanterburyChristchurchNew Zealand
  2. 2.Institute of Informatics SystemsNovosibirskRussia

Personalised recommendations