Polynomial Approximations for Model Checking

Abstract

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.