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

**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} }