120 MODEL CHECKING OF FINITE-STATE SYSTEMS

Symbolic Model Checking Algorithm:

Input: model M represented by BDDs and CTL formula f . Output: whether f is satisfied.

Let f s denote the value of formula f in state s. If formula f is:

atomic proposition P: return the BDD for P.

¬ f1 or f1 f2: execute Bryant’s algorithms [Bryant, 1986] for Boolean connectives. EX f : return f s = true iff there is a successor state s such that f s = true,

that is, s [ f s N (s, s )].

E[ f1 U f2]: construct the BDD (representing the states in which f holds) by iterating

E[ f1 U f2] = f2 ( f1 EX E[ f1 U f2]).

EG f : construct the BDD by finding the greatest fixed point EG f and iterating EG f = f EX EG f .

All other CTL operators can be stated using the above operators.

Figure 4.5 Symbolic model checking algorithm.

4.6.2 Symbolic Model Checker

Instead of explicitly enumerating all states in the model, which is a labeled state transition system or Kripke structure, we symbolically represent it as BDDs, hence the name symbolic model checker (SMC) [Burch et al., 1990a]. We have to find a way to translate the model into BDDs. Suppose that the current state of the system is represented by a vector of Boolean variables S = {s0, . . . , sn−1} and the next state of the system is represented by a vector of Boolean variables S = {s 0, . . . , s n−1}. Using S and S , the transition relation between the values of the variables in the current and the next states can be stated as a Boolean formula N (s0, . . . , sn−1, s 0, . . . , s n−1). Note that a finite-domain non-Boolean variable can be easily converted into a vector of Boolean variables. We give an example of this conversion in chapter 12 (section 12.3.1).

Each transition in this transition graph models the time passage of one time unit. Without further extensions, non-unit as well as nondeterministic transition time can be modeled by a sequence of unit transitions. Later, we will see that it is easy to extend this transition graph into a more powerful model called the timed transition graph [Campos et al., 1994].

The symbolic model checker, shown in Figure 4.5, takes as input the model M represented by BDDs and the formula f to be verified (in the initial states of M). For every atomic proposition in S, it outputs a BDD with one Boolean variable such that the BDD is true in a state iff the formula f is true in that state.

4.7 REAL-TIME CTL

CTL can specify the relative ordering of events or actions in a finite state system, but it cannot directly express when these events or actions occur. An awkward way of specifying that some event will occur in the future in at most a fixed number of time units is by nesting EX or AX operators. Real-time systems impose bounds on

the response time of events and actions. To handle properties with these quantitative constraints, CTL has been extended in a number of ways. Here we describe one extension [Emerson et al., 1990] that adds time intervals to CTL temporal operators and introduces the bounded until operator U[x, y].

The formula E[ f1 U[x, y] f2] at a given state means that a path exists beginning at this state and leading to a future state where f2 holds, f1 holds at every state between the beginning state and this future state, and the distance between the beginning state and this future state is within the interval [x, y]. This definition is now formalized.

Existentially Bounded Until Operator: The formula E[ f1 U[x, y] f2] at state s0 means that a path exists beginning at s0 and some i such that x ≤ i ≤ y and f2 holds at state si and j < i, f1 holds at state s j .

Example. Let f1 denote that the wireless telephone’s battery power is in the “low” position. Let f2 denote that the wireless telephone is “off.” Then E[ f1 U [5, 18] f2] states that there is an execution path in which the telephone will turn “off” within a time interval between 5 and 18 time units of the telephone’s battery power indicating the “low” position, and before this “off” state the telephone’s battery power is in the “low” position.

The formula EG[x, y] f at state s0 means that there exists a path beginning at s0 and i, x ≤ i ≤ y, f holds at state si .

4.7.1 Minimum and Maximum Delays

Now we describe algorithms [Campos et al., 1994] for finding the minimum and maximum delays between two events. These are known as quantitative algorithms since they compute numerical timing information about events rather than just relative ordering of events in a system. Given a real-time system, they are used to verify that given timing constraints are satisfied and also to predict the system’s performance, telling how well the system performs relative to the given timing constraints. These algorithms start from states satisfying the first event, explore all possible execution paths, and terminate when a state satisfying the second event is reached.

The minimum delay algorithm (Figure 4.6) takes as input the start set and the final set of states satisfying the first event and the second event, respectively. If a state in final set is reachable from a state in start set, it returns the length in terms of the number of edges in a shortest path from a state in start set to a state in final set. If none of the states in final set is reachable, then the algorithm returns infinity. For example, the first event can be a request to use a non-sharable resource by a real-time process and the second event can be the allocation of this resource to this process, so the minimum delay algorithm finds the minimum waiting time for this process to obtain the resource.

The function successors set(S) returns the set of successor states of state S and is defined as successors set(S) = {s |N (s, s ) is true for some s S}. This func-

122 MODEL CHECKING OF FINITE-STATE SYSTEMS

procedure min delay(start set, final set) i := 0;

R := start set;

R := successors set(R) R;

while R = R R ∩ final set = do i := i + 1;

R := R ;

R := successors set(R ) R ; if R ∩ final set =

then return i; else return ∞;

Figure 4.6 Minimum delay algorithm.

tion, the sets R and R of states, and the intersection and union operations are all implemented using BDDs.

Next we describe the maximum delay algorithm (Figure 4.7), which also takes as input the start set and the final set of states satisfying the first event and the second event, respectively. If a state in final set is reachable from a state in start set, it returns the length in terms of the number of edges in a longest path from a state in start set to a state in final set. If an infinite path exists from a state in start set that never reaches a state in final set, then the algorithm returns infinity. Again, for example, the first event can be a request to use a non-sharable resource by a real-time process and the second event can be the allocation of this resource to this process, so the maximum delay algorithm finds the maximum waiting time for this process to obtain the resource. If we impose a deadline (relative to the resource request time by this process) for the allocation of this resource to this process, then the maximum delay algorithm tells us whether this deadline can be satisfied or not.

The set not final set represents the set of states which are not in the set final set. The function predecessors set(S ) returns the set of predecessor states of state S and is defined as predecessors set(S ) = {s|N (s, s ) is true for some s S }. As in the minimum delay algorithm, this predecessor function, the sets R and R of states,

procedure max delay(start set, final set)

i := 0;

R := true;

R := not final set;

while R = R R ∩ start set = do i := i + 1;

R := R ;

R := predecessors set(R ) not final set; if R = R

then return ∞; else return i;

Figure 4.7 Maximum delay algorithm.

and the intersection operations are all implemented using BDDs. Here, a backward search is needed to identify a longest path.

Two reasons exist for the efficiency of these quantitative algorithms. First, Boolean formulas are used to represent the sets of states satisfying certain events, and these formulas are represented by BDDs in the implementation. Since sets are represented by BDDs, the operations on these sets are implemented as efficient operations on the BDDs described earlier. Second, these operations are applied to sets of many states instead of individual states, thus significantly reducing computation time for exhaustive state space exploration.

4.7.2 Minimum and Maximum Number of Condition Occurrences

Often we are interested in knowing the number of states satisfying a given condition along a path, for example, how many times a train arrives and passes a railroad crossing. Here, we describe two condition counting algorithms [Campos et al., 1994] that compute the minimum and maximum number of states satisfying a given condition over all finite paths from a state in the start set to a state in the final set, thus telling the minimum and maximum number of occurrences of this condition over all finite paths between these states.

Similar to the minimum and maximum delay algorithms, these quantitative algorithms start from states satisfying the first event, explore all possible execution paths and count the number of states satisfying a given condition, and terminate when a state satisfying the second event is reached. Before running either condition counting algorithm, we have to first check that a finite path is present in the transition graph from a state in the start set to a state in the final set using the maximum delay algorithm described above.

We need to introduce a counter variable in each state to remember the number of states satisfying the given condition along the path traversed so far. To do this systematically, a new state transition system is introduced in which each state is a pair of the original state and the positive integer counter [Campos et al., 1994]. Let N be the set of natural numbers. The state set is Sa = S × N.

Augmented Transition Relation: Given an original state-transition graph with transition relation N S × S, the corresponding augmented transition relation Na Sa × Sa is defined as

Na ( s, k , s , k ) = N (s, s ) (s condition k = k + 1 s / condition k = k).

This means that in the augmented transition relation Na , there is a transition froms, k to s , k iff there is a transition from state s to state s in the original transition relation N and either s belongs to the condition and the counter k is k + 1 or s does not belong to the condition and k is the same as k. Therefore, the condition counter k for state s is incremented only if state s satisfies this condition.

124 MODEL CHECKING OF FINITE-STATE SYSTEMS

Let T Sa . Again, the function successors set(T ) returns the set of predecessor states of state S and is defined as successors set(T ) = {t |N (t, t ) is true for some t T }. We now outline the minimum counting algorithm.

Procedure min count ( start set, condition, final set ) current min := ∞;

R = { s, 1 |s start set ∩ condition} { s, 0 |s start set ∩ condition}; loop

reached final set := R ∩ final set; if reached final set = then begin

m := max{k| s, k reached final set}; if m < current min then current min := m

end;

R := R ∩ not final set;

if R = then return current min;

R := successors set(R ) endloop;

Figure 4.8 Minimum condition-counting algorithm.

In the algorithm (Figure 4.8), variable current min gives the minimum count for all previous iterations. The set R is the set of states in Sa reached in the current iteration of the loop. The algorithm checks the endpoints of paths with i states during the ith iteration. If the states are in final set (meaning they are the terminal states of paths), the counter values are used to compute the minimum count for these paths and the current minimum is updated. If the states are not in final set (meaning they are not terminal states of paths), the loop continues after deriving the successors of these non-terminal states. The algorithm returns the current minimum as the minimum count when all reached states are in final set.

Procedure max count ( start set, condition, final set ) current max := −∞;

R = { s, 1 |s start set ∩ condition} { s, 0 |s start set ∩ condition}; loop

reached final set := R ∩ final set; if reached final set = then begin

m := max{k| s, k reached final set};

if m > current max then current max := m

end;

R := R ∩ not final set;

if R = then return current max;

R := successors set(R ) endloop;

Figure 4.9 Maximum condition-counting algorithm.