Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

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
Authors: 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}
  }
   

Last modified: 2016-01-1416:21
Andrzej Murawski