May 27, 2011, 2:08 p.m.
posted by nfrank
Symbolic CTL Model CheckingEarlier 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 ComputationA 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) = x^{2} - 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 x_{0}, and compute iteratively the sequence x_{1} = f(x_{0}), x_{2} = f(x_{1}), ..., x_{i} + 1 = f(x_{i}), until x = f(x). This sequence of computations can be regarded as applying mapping f to x_{0} multiple times until it reaches a fix-point. The choice of x_{0} 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 t^{i}(S) be i applications of t to S. In other words, t^{i}(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 t^{i}(Ø) t^{i} + 1 (Ø) and t^{i}(U) t^{i + 1} (U). Furthermore, there exist integers a and b such that t^{a}(Ø) = t^{a + 1} (Ø) and t^{b} (U) = t^{b + 1} (U). We can call t^{a} (Ø) and t^{b} (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:
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, t^{1} = f + AX(Ø). The states included in t^{1} 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 t^{1} are the set of states at which f holdsl(s, f). Thus, states in t^{1} satisfy AX(f). In iteration 2, t^{2} = f + AX(f). The states included are those that satisfy f and all the next states that satisfy f. Thus, t^{2} satisfies AX(f). In the ith iteration,
Thus, a state is in t^{i} if it satisfies f or all paths from it reach states that satisfy f in i or fewer transitions. Therefore, states in t^{i} 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 t^{n}, 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), AX^{2}(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 bitsq_{2}, q_{1}, and q_{0}to encode the eight states. For simplicity, the code of a state is the binary of the state number. For example, s_{6} 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 s_{2}, s_{3}, s_{6}, and s_{7}. So, the characteristic function l(q_{0}, q_{1}, q_{2}, a) is
Similarly, and
From these atomic propositions, we can compute the following:
Now, we have l(q_{0}, q_{1} q_{2}, f) = q_{1} and l(q_{0}, q_{1}, q_{2}, g) = . As a check, we label the states with f and g, as in FigureA. It can be seen that both l(q_{0}, q_{1}, q_{2}, f) and l(q_{0}, q_{1}, q_{2}, 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 t^{1} (S) = g + f · EX(Ø) = l(q_{0}, q_{1}, q_{2}, g) = q_{2}q_{1}q_{0} + . The states included in this iterations are 000, 100, and 111 (or, s_{0}, s_{4}, and s_{7}). 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 t^{2}(S) is not equal to t^{1}(S), we continue. In iteration 3,
Substituting the expressions, we get , which is not equal to t^{2}(S). The states are 000, 010, 111, 100, 110, and 111 (or, s_{0}, s_{2}, s_{3}, s_{4}, s_{6}, and s_{7}). They are shaded in Figure. The newly added state s_{2} is two cycles from a state labeled g. In iteration 4,
Substituting the expressions, we get , which is equal to t^{2}(S). Therefore, we have reached a fix-point. The characteristic function for the states satisfying is . The states are s_{0}, s_{2}, s_{3}, s_{4}, s_{6}, and s_{7}. 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 ConstraintsA fairness constraint f = {f_{1}, ..., f_{n}} mandates that all its formulas, f_{1}, ..., f_{n}, 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 EX_{f}(f), E_{f}(fUg), and EG_{f}(f). We first compute EG_{f}, then EX_{f} and EU_{f}, which makes use of the algorithm of EG_{f}. EG_{f}(f) means that there exists a path along which f holds at every state, and every formula of f holds infinitely often. In Figure, EG_{f}(f) with f = {f_{1}, f_{2}} holds at state Figure. A Kripke structure having states satisfying EG_{f}(f)
s_{1}, because path P satisfies f at every state, and it satisfies both f_{1} and f_{2}. Similarly, EG_{f}(f) holds at s_{2}, s_{3}, and s_{4}. But EG_{f}(f) fails at s_{0}, s_{5}, and s_{6}, because path L, the only path, does not satisfy both fairness constraints. EG_{f}(f) can be expressed using fix-point notation and ordinary CTL operators
where
When we compare EG_{f}(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, t^{1} = f · EX(E(fU(f))), which holds at state s if f holds at s and its next state satisfies fUf. Such a state, s_{0}, is illustrated in FigureA. Figure. Unrolling the fix-point computation of EG_{f}(f). (A) A sequence of states after one iteration expansion of EG_{f}(f). (B) A sequence of states after two iterations of expanding EG_{f}(f).In iteration 2, t^{2} = f · EX(E(fU(t^{1} · f))), which is the same description as t^{1} except for how the path endsit must end at a state in t^{1}, which contains s_{0}. Concatenating the path described by t^{2} with the path for s_{0} from t^{1}, 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 EG_{f}(f). To compute EX_{f}(f), we use the same technique we introduced in explicit checking of EX_{f}(f)namely, creating variable fair, which evaluates true at a state if there is a fair path emanating from the state. Then EX_{f}(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) = EG_{f}(1). Therefore, the set of states satisfying EX_{f}(f) is the set of states with next states that are in both l(s, f) and l(s, fair). In other words, EX_{f}(f) = EX(f) · EG_{f}(1). Similarly, E_{f}(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 (s_{1}s_{0}) to encode the states, and the encoding of a state matches the state's subscript. With fairness constraint f = {s_{1}}, which indicates that states q_{2} and q_{3} are fair states, we can compute EG_{f}(f). Figure. Checking fair CTL formula EG_{f}(x) with fairness constraint f = {s_{1}}
First we calculate the set of states at which f holds. It consists of states q_{0}, q_{1}, and q_{3}, giving . The state set satisfying the fairness constraint is s_{1}. In EG_{f}(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, t^{1}, 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 t^{2} = f · EX(E(fU(s_{1}s_{0}))). The inner fix-point computation is E(fU(s_{1}s_{0})) = lfp(s_{1}s_{0} + fEX(S)).
So, a fix-point for the outer fix-point computation. Therefore, the entire computation terminates, giving
Based on this result, only states q_{0} and q_{3} satisfy EG_{f}(f). Examining Figure, we can confirm that these two states traverse the self-loop at state q_{3} satisfy f infinitely often and every state along the path also satisfies f. State q_{1} is excluded because it does not satisfy f. State q_{2} is omitted because it does not satisfy f. |
- Comment