Paper: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract) (at LICS 1986)
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} }