## Paper: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract) (at LICS 1986)

*Winner of the Test-of-Time Award in 2006***E. Allen Emerson Chin-Laung Lei**

### Abstract

In this paper we adress the problem of automatically verifying
that a given finite state concurrent program meets a correctness assertion
specified in the propositional Mu-Calculus Lμ defined by Kozen in
[Ko83]. The propositional Mu-Calculus provides a framework for handling
fairness, past-tense temporal modalities, and extended temporal modalities such
as those of [Wo81] in a uniform way. We give an efficient model checking
algorithm for specifications given in a fragment, Lμ_{2}, of the
propositional Mu-Calculus, where the alternation depth of least and greatest
fixpoint operators is restricted to be at most 2. We show that
Lμ_{2} can succinctly encode (and is, in fact, stricly more
expressive than) many of the commonly used logics of programs such as PDL
([FL79]), PDL-Δ ([St82]), CTL ([EC82], [CES83]), FCTL and GFCTL
([EL85]). In practice, we therefore have a small polynomial time model checker
for a most useful portion of the propositional Mu-Calculus.

### BibTeX

@InProceedings{EmersonLei-EfficientModelCheck, author = {E. Allen Emerson and Chin-Laung Lei}, title = {Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)}, booktitle = {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)}, year = {1986}, month = {June}, pages = {267--278}, location = {Cambridge, MA, USA}, publisher = {IEEE Computer Society Press} }