A synthesis of two approaches for verifying finite state concurrent systems.
01 January 1989
Finite state concurrent systems arise in many applications. Both sequential circuits and communication protocols can be viewed as implementing such systems at some level of abstraction. When the number of system states is large, correctness may become a major problem. Two techniques have shown promise for automatically verifying this type of program. The first approach is based on temporal logic model checking and is used in the CTL verifier developed at CMU. The second approach is based on showing containment between automata and is used by the COSPAN system developed at Bell Laboratories. We describe a branching time temporal logic, called ECTL, which permits operators of the form E[M](f sub 1,...,f sub n) and A[M](f sub 1,...,f sub n) where M is an automation on infinite tapes and f sub 1,...,f sub n are other ECTL formulas, and A and E are the universal and existential branching time operators, respectively.