Paper: An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic (at LICS 1986)

Authors: Michael C. Browne

Abstract

One method of verifying finite state systems is to represent the system as a state-transistion graph and use an efficient algorithm, called a model checker, to determine if this structure is a model of a temporal logic specification. An example of this approach was given by Clarke, Emerson and Sistla, who developed a model checking algorithm for a propositional branching-time temporal logic called CTL (Computation Tree Logic). Unfortunately, their algorithm assumes that all of the state transitions are unconditional, when in practice the transitions of the most finite state machines depend on the value of a set of inputs. In this paper, we present an improved CTL model checking algorithm that allows conditional transitions. Although the worst case complexity of our new algorithm is the same as the orginal model checker, we show that for certain classes of CTL formulas, the new algorithm is a significant improvement.

BibTeX

  @InProceedings{Browne-AnImprovedAlgorithm,
    author = 	 {Michael C. Browne},
    title = 	 {An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {260--266},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }