Symbolic CTL Model Checking





Symbolic CTL Model Checking

Earlier we studied checking CTL formulas using graph traversal algorithms. Building on the knowledge of traversing graphs symbolicallytraversing graphs through Boolean function computationswe are in a position to derive symbolic algorithms to check CTL formulas. Keep in mind that the Boolean functions in symbolic algorithms are represented using BDDs. Therefore, all Boolean operations are BDD operations. We will first look at fix-point computation and relate it to CTL formulas. Once expressed using fix-point notation, the representation lends itself to symbolic computation.

Fix-point Computation

A function y = f(x) has a fix-point if there exists p such that p = f(p), and p is called a fix-point of the function. On one hand, not all functions have fix-points. Function f(x) = x + 1 in a real domain and range does not have a fix-point. On the other hand, some functions have multiple fix-points. For example, f(x) = x2 - 2 in a real domain and range has two fix-points: -1 and 2. One way of finding a fix-point is to select an initial value of x, say x0, and compute iteratively the sequence x1 = f(x0), x2 = f(x1), ..., xi + 1 = f(xi), until x = f(x). This sequence of computations can be regarded as applying mapping f to x0 multiple times until it reaches a fix-point. The choice of x0 plays an important role in determining whether a fix-point will be found and which fix-point will be found.

Let's consider functions with a domain and range that are subsets of states. In other words, functions that take as input a subset of states and produce another subset of states. Let t(S) denote a such function and ti(S) be i applications of t to S. In other words, ti(S) = t(t(...t(S))) i times. Furthermore, let's say that t(S) is monotonic if A B implies t(A) t(B). Let U be the set of all states. Theorem 9.1 provides conditions on t so that it has fix-points.

Theorem 9.1.

If t is monotonic and U is finite, then ti(Ø) ti + 1 (Ø) and ti(U) ti + 1 (U). Furthermore, there exist integers a and b such that ta(Ø) = ta + 1 (Ø) and tb (U) = tb + 1 (U).

We can call ta (Ø) and tb (U) the least and greatest fix-point of t, and denote them by lfp(t) and gfp(t) respectively. Now we can express the six CTL operators using fix-point notation. In Theorem 9.2, for brevity a CTL formula stands for the set of states at which the formula holds. That is, formula f stands for the characteristic function l(s, f) = {s/f holds at state s}. It is for notational brevity that we use this shorthand.

Theorem 9.2.

The six CTL operators can be expressed as fix-point computations:

  1. AF(f) = lfp(t(S)), where t(S) = f + AX(S).

  2. EF(f) = lfp(t(S)), where t(S) = f + EX(S).

  3. AG(f) = gfp(t(S)), where t(S) = f · AX(S).

  4. EG(f) = gfp(t(S)), where t(S) = f · EX (S).

  5. A(fUg) = lfp(t(S)), where t(S) = g + f · AX(S).

  6. E(fUg) = lfp(t(S)), where t(S) = g + f · EX(S).

To understand the notation in Theorem 9.2, consider AF(f) = lfp(t(S)), where t(S) = f + AX(S). This says that the set of states AF(f) holds is the least fix-point of t(S). t(S) takes in a set of states S and computes the set of states with next states that satisfy S. In other words, in S, this result is then ORed with the set of states at which formula f holds. Using characteristic function notation, it is l(s, AF(f)) = lfp(t(S)) and t(S) = l(s, f) + l(s, AX(S). Operators AX and EX can be computed without using a fix-point operator, as


and


where T(s, n) is the transition relation of the underlying Kripke structure. The universal and existential quantifiers are computed as conjunction and disjunction as follows:


and


Function t(S) transforms predicates f and g into a function and is called a predicate transformer.

To have an intuitive understanding of these identities, we need to examine AF(f). AF(f) holds at a state if all paths from the state will eventually lead to states, including the state itself, at which f holds. The least fix-point computation AF(f) = lfp(f + AX(S) consists of a sequence of operations, as shown here.

In iteration 1, t1 = f + AX(Ø). The states included in t1 are the states at which f holds and the states at which AX(Ø) holds. AX(Ø) contains the states with next states that satisfy Ø, which is not satisfiable. Thus, AX(Ø) gives Ø. Therefore, the states returned by t1 are the set of states at which f holdsl(s, f). Thus, states in t1 satisfy AX(f).

In iteration 2, t2 = f + AX(f). The states included are those that satisfy f and all the next states that satisfy f. Thus, t2 satisfies AX(f).

In the ith iteration,


Thus, a state is in ti if it satisfies f or all paths from it reach states that satisfy f in i or fewer transitions. Therefore, states in ti satisfy AX(f). Hence, the states in the least fix-point of t(S) = f + AX(S) satisfy AX(f). Figure shows a Kripke structure and illustrates the progressive inclusion of states through iterations in fix-point computation. The solid circles represent included states, and states labeled f satisfy f.

Figure. Successive inclusion of states satisfying AF(f) in fix-point computation


Conversely, consider state v that all its paths eventually lead to states satisfying f. Let n be the earliest time when all paths from v have reached states satisfying f. Then v must be included in tn, which is a subset of the least fix-point of t(S). Therefore, v must be in lfp(t(S)).

Similarly, AG(f) = gfp(t(S)), where t(S) = f · AX(S) expands to


which implies that a state v satisfies AG(f) if it satisfies f, AX(f), AX2(f), and so on, which is equivalent to saying that v satisfies f, and all its next states satisfy f, and all its next next states satisfy f, and so on. This is just what AG(f) is. Other identities can be interpreted similarly.

To complete our treatment of symbolic checking of CTL formulas, we need to examine the case when the formula f is a Boolean formula without CTL operators. We can compute l(s, f) from the bottom up using the following identities:


and


Note that characteristic functions are represented using BDDs. Therefore, fix-point computation, complementation, and ORing of characteristic functions are executed as efficiently as BDD operations.

14.

Let's take a look at in the Kripke structure in Figure. We use 3 bitsq2, q1, and q0to encode the eight states. For simplicity, the code of a state is the binary of the state number. For example, s6 has code 110. The transition relation is


Plugging in the state bits, we obtain


Notice the complexity of the transition function. It is a major source of computational cost. This transition function is used in computing EX(f), as in


To compute , we first compute f = a and , and then E(fUg). The set of the states satisfying atomic formulas, a, consists of s2, s3, s6, and s7. So, the characteristic function l(q0, q1, q2, a) is


Similarly, and


From these atomic propositions, we can compute the following:


Now, we have l(q0, q1 q2, f) = q1 and l(q0, q1, q2, g) = . As a check, we label the states with f and g, as in FigureA. It can be seen that both l(q0, q1, q2, f) and l(q0, q1, q2, g) give the correct sets of states.

Next, we use the fix-point formulation to compute E(fUg). That is, E(fUg) = lfp(t(S)), where t(S) = g + f · EX(S).

In iteration 1, we have t1 (S) = g + f · EX(Ø) = l(q0, q1, q2, g) = q2q1q0 + . The states included in this iterations are 000, 100, and 111 (or, s0, s4, and s7). They are shaded in FigureA. This iteration finds the states only satisfy g.

In iteration 2,


where


After simplification, . The states are 000, 011, 100, 110, and 111. They are shaded in FigureB. This iteration includes states that are labeled g or f, and those with a next state labeled g. The former is a result of iteration 1, and the latter is a result of the current iteration. Because t2(S) is not equal to t1(S), we continue.

In iteration 3,


Substituting the expressions, we get , which is not equal to t2(S). The states are 000, 010, 111, 100, 110, and 111 (or, s0, s2, s3, s4, s6, and s7). They are shaded in Figure. The newly added state s2 is two cycles from a state labeled g.

In iteration 4,



Substituting the expressions, we get , which is equal to t2(S).

Therefore, we have reached a fix-point. The characteristic function for the states satisfying is . The states are s0, s2, s3, s4, s6, and s7.

25. A Kripke structure for symbolically checking


Figure. Progressive inclusion of states satisfying . (A) Kripke structure after f and g are verified. (B) Kripke structure after two iteration of t(s) = g + f · EX(S).


27. States attained in iteration 3 in computing


CTL Checking with Fairness Constraints

A fairness constraint f = {f1, ..., fn} mandates that all its formulas, f1, ..., fn, be satisfied infinitely often along a path. A path satisfying f is called a fair path. Checking a CTL formula f with a fairness constraint f means that only fair paths are considered and we find all states satisfying f along the fair paths. Because all CTL operators can be expressed in three base operators (EX, EU, and EG), we will study checking of these three operators with fairness constraints. To distinguish CTL checking from CTL checking with fairness constraints, we denote checking with fairness with a subscript f, as in EXf(f), Ef(fUg), and EGf(f). We first compute EGf, then EXf and EUf, which makes use of the algorithm of EGf.

EGf(f) means that there exists a path along which f holds at every state, and every formula of f holds infinitely often. In Figure, EGf(f) with f = {f1, f2} holds at state

Figure. A Kripke structure having states satisfying EGf(f)


s1, because path P satisfies f at every state, and it satisfies both f1 and f2. Similarly, EGf(f) holds at s2, s3, and s4. But EGf(f) fails at s0, s5, and s6, because path L, the only path, does not satisfy both fairness constraints. EGf(f) can be expressed using fix-point notation and ordinary CTL operators


where


When we compare EGf(f) with EG(f) = gfp(f · EX(S)), we see that an EU operator is nested inside the EX operator. To get an intuitive understanding of the identity, we must assume there is only one fairness formulaf = {f}and unroll it a couple times.

In iteration 1, t1 = f · EX(E(fU(f))), which holds at state s if f holds at s and its next state satisfies fUf. Such a state, s0, is illustrated in FigureA.

Figure. Unrolling the fix-point computation of EGf(f). (A) A sequence of states after one iteration expansion of EGf(f). (B) A sequence of states after two iterations of expanding EGf(f).


In iteration 2, t2 = f · EX(E(fU(t1 · f))), which is the same description as t1 except for how the path endsit must end at a state in t1, which contains s0. Concatenating the path described by t2 with the path for s0 from t1, we have the path shown in FigureB. This path satisfies f at every state and the fairness constraint is satisfied twice. Further iterations simply append paths from the previous iterations. Each iteration only adds states that satisfy f and a state that satisfies f. At the nth iteration, the resulting path satisfies f n times. Therefore, the result is a path, or a set of paths, that satisfies f at every state and satisfies f infinitely often, which is simply EGf(f).

To compute EXf(f), we use the same technique we introduced in explicit checking of EXf(f)namely, creating variable fair, which evaluates true at a state if there is a fair path emanating from the state. Then EXf(f) = EX(f · fair). To obtain the characteristic function for a set of states satisfying fair, l(s, fair), we use the identity l(s, fair) = EGf(1). Therefore, the set of states satisfying EXf(f) is the set of states with next states that are in both l(s, f) and l(s, fair). In other words, EXf(f) = EX(f) · EGf(1). Similarly, Ef(fUg) = E(fUg · fair), which mandates the ending states also be in l(s, fair).

15.

If we take a look at Figure, we use 2 bits (s1s0) to encode the states, and the encoding of a state matches the state's subscript. With fairness constraint f = {s1}, which indicates that states q2 and q3 are fair states, we can compute EGf(f).

Figure. Checking fair CTL formula EGf(x) with fairness constraint f = {s1}


First we calculate the set of states at which f holds. It consists of states q0, q1, and q3, giving . The state set satisfying the fairness constraint is s1.

In EGf(f) = gfp(f · EX(E(fU(S · f)))), there are two fix-point computations here. The inner fix-point computation comes from E(fU(S · f)).

In iteration 1 of the outer fix-point computation, t1, we need to compute f · EX(E(fUf)). The inner fix-point computation is E(fUf) = lfp(f + fEX(S)). This fix-point computation unfolds as follows:



(a fix-point)

Thus, , giving


In iteration 2 of the outer fix-point computation, we compute . So t2 = f · EX(E(fU(s1s0))).

The inner fix-point computation is E(fU(s1s0)) = lfp(s1s0 + fEX(S)).




So,

a fix-point for the outer fix-point computation. Therefore, the entire computation terminates, giving


Based on this result, only states q0 and q3 satisfy EGf(f). Examining Figure, we can confirm that these two states traverse the self-loop at state q3 satisfy f infinitely often and every state along the path also satisfies f. State q1 is excluded because it does not satisfy f. State q2 is omitted because it does not satisfy f.


     Python   SQL   Java   php   Perl 
     game development   web development   internet   *nix   graphics   hardware 
     telecommunications   C++ 
     Flash   Active Directory   Windows