An improved algorithm for the automatic verification of finite state systems using temporal logic

One method of verifying finite state systems is to represent the system as a statetransition 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 [3], who developed a model checking algorithm for a propositional branchingtime 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 most finite state machines depend on the values 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 original model checker, we show that for certain classes of CTL formulas, the new algorithm is a significant improvement. 1 . Introduction There are two distinct methods of applying temporal logic to system verification. In the first approach, temporal logic is used as a deductive system in which proofs are constructed to show that the system meets its specifications [5,6]. Although this technique is very powerful, the construction of such proofs can be very difficult for a human and almost impossible for a machine. Furthermore, it is unlikely that any significant degree of automation is possible, since the complexity of most temporal logics is so high that the construction of an automatic theorem prover is probably not feasible. The other method is model theoretic in nature and is only applicable to finite state systems, such as network protocols and hardware controllers. In this approach, the system is represented as a finite state-transition graph, or Kripke structure. Then, instead of constructing a tedious proof, an efficient algorithm, called a model checker, is used to determine whether or not this structure is a model of the temporal logic specification. Clarke, Emerson and Sistla have presented an example of this approach [3] by developing a model checking algorithm for a propositional branching-time temporal logic called CTL (Computation Tree Logic). The usefulness of this algorithm, which is linear in both the number of states and the size of the specification, has been demonstrated in several other papers [1,2]. This research was supported by NSF Grant Number MCS-82-16706. One drawback of this algorithm is that it assumes that the state transitions are unconditional in that all of the transitions from a state are always enabled. However, most of the systems encountered in practice (particularly hardware controllers) have state transitions that are enabled or disabled by a set of external input signals. In order to remove these conditional transitions so that this algorithm can be used, it is necessary to replace each state of the original system by a set of states, one for each possible combination of input signals, and to determine which transitions are possible from each new state by evaluating the conditions. If there are n inputs, there are 2? input combinations, so this preprocessing results in an exponential blowup in the number of states. Since the model checker is linear in the number of states, this algorithm is exponential in the number of input signals. In this paper, we present a new algorithm that can verify systems with conditional transitions without the additional preprocessing that the old algorithm requires. In the worst case, the new algorithm is also exponential in the number of input signals. However, if the formula being verified is in a special class, the new algorithm is linear in the number of input signals and quadratic in the size of the input formula. Since this class of formulas includes all of the formulas that we have ever attempted to verify in practice, we believe that the new algorithm is a significant improvement on the original model checking algorithm. We have implemented both the original model checker and the new algorithm in C on a VAX/780 in order to compare their performance. We attempted to use both algorithms to verify two hardware controllers (a simple traffic light controller and a UART). In the first test, the old algorithm took 17.8 seconds of CPU time and the new algorithm took 3.3 seconds. In the second test, the new algorithm took 54.5 seconds of CPU time, but the preprocessing for the old algorithm added too many states for our implementation of the old algorithm to handle. The test of the old algorithm was aborted after 2 hours (!). The paper is organized as follows: In section 2, we describe the syntax and semantics of the logic, called Computation Tree Logic (CTL). In section 3, we describe the structure of the finite state systems that we will verify. In section 4, we give an outline of our algorithm. In section 5, we give a detailed proof of part of the algorithm. In section 6, we discuss the efficiency of the algorithm. The paper concludes with a brief discussion about the usefulness of this algorithm and future enhancements. 2. The Specification Language The formal syntax for CTL is given below. AP is the underlying set of atomic propositions. 1. Every atomic proposition p € AP is a CTL formula. 2. If ^ and f2 are CTL formulas, then so are ~<fr ^ Af 2 , AX fv EX f r Af^U f 2 ] , and E ^ U y. The symbols A and have their usual meanings. X is the next time operator; the formula AX ^ (EX intuitively means that ^ holds in every (in some) immediate successor of the current state. U is the until operator; the formula Af^U f 2 ] ( E ^ U f 2]) intuitively means that for every computation path (for some computation path), there exists an initial prefix of the path such that f2 holds at the last state of the prefix and f 1 holds at all other states along the prefix. We define the semantics of CTL formulas with respect to a labeled state-transition graph. Formally, a Kripke structure is a triple M = (S, ft, P) where • S is a finite set of states. • R is a binary relation o n S ( R C S x S ) which gives the possible transitions between states and must be total, i.e. Vx €S 3y €S [{x,y) €/?]. • P is an assignment of atomic propositions to states i.e. P: S * 2AP. A path is an infinite sequence of states (sQ, s v s2,...) such that V/ [(s., s / + f ) €/?]. We use the standard notation to indicate truth in a structure: M,sQ N f means that formula f holds at state sQ in structure M. When the structure M is understood, we simply write s Q l= f. The relation N is defined inductively as follows: