Introduction
Model checking ([
Temporal logic specifications, whether given in LTL or in CTL, are roughly divided
into two basic categories [
Symbolic model checking is performed using two main approaches. The first is
based on BDDs (e.g. SMV [
We consider a different approach for fair cycle detection, that makes use of
Description Logic (DL) technology. We cast a model M and the negation of the given liveness
specification ϕ as a satisfiability query in DL, such that if an interpretation is found, it
indicates an error in M . While a model and a liveness formula can be easily encoded as
a terminology in ALC, this is not the case with fairness constraints. In order to express
fairness, more expressive dialects are needed (see, for example [
We have implemented our method in the Description Logic reasoner FaCT++ [
The rest of the paper is organized as follows. In the next section we give the necessary definitions, and in Section 3 we present the translation of a liveness model checking problem into a DL satisfiability query. Section 4 is the main section of the paper, where we present our algorithm for fair cycle detection. Section 5 presents experimental results, and Section 6 concludes the paper.
Description Logic Definition 1 (Description Logic ALC) Let NC and NR be disjoint sets of atomic concepts {A1, A2, . . .} and atomic roles {R1, R2, . . .} respectively. The set of concepts C is the smallest set including NC such that if C, D ∈ C and R ∈ NR, then so are ¬C, C u D and ∃R.C.
Additional concepts are defined as syntactic sugaring of those above: • C t D = ¬(¬C u ¬D) • ∀R.C = ¬∃R.¬C and • > = A t ¬A for some atomic concept A.
A general concept inclusion (GCI) is an expression of the form C v D, where C and D are arbitrary concepts. A terminology (or TBox) T consists of a finite set of concept inclusions.
The semantics of expressions is defined with respect to a structure I = (ΔI , ·I ), called an interpretation, where ΔI is a non-empty set of individuals, and (·)I is an interpretation function that maps atomic concepts A to a subset of ΔI and atomic roles R to a subset of ΔI × ΔI . The interpretation function is extended to arbitrary concepts in a way that satisfies each of the following: – (C u D)I = CI ∩ DI , – (∃R.C)I = {e ∈ ΔI : ∃(e, e0) ∈ RI s.t. e0 ∈ CI }, and – (¬C)I = ΔI \ CI .
An interpretation I satisfies a GCI (C v D) if CI ⊆ DI , and a TBox T if it satisfies each concept inclusion in T .
The concept satisfiability problem is to determine, for a given TBox T and concept C, if there exists an interpretation I that satisfies T and for which CI is non-empty, written T |=dl C.
Tableaux Algorithms for Concept Satisfiability in ALC. The tableaux algorithm works on a labeled tree, called a completion tree, that has a close correspondence to an interpretation. For a concept C, we write nnf(C) to denote the Negation Normal Form (NNF) of C, write ¬˙C to denote the NNF of ¬C, and write sub(C) to denote the set of all subconcepts of C (including C) and their negation. For a TBox T we define sub(T ) = S(CvD)∈T sub(C) ∪ sub(D).
Definition 2 Let T be an ALC TBox and C is a concept in NNF. A completion tree for C with respect to T is a directed graph G = (V, E, L) where each node x ∈ V is labelled with a set L(x) ⊆ sub(T ) ∪ sub(C) and each edge hx, yi ∈ E is labelled with a role name L(hx, yi) ∈ RN .
If hx, yi ∈ E, then y is called a successor of x and x is called a predecessor of y. If, in addition, R = L(hx, yi), then y (x) is called an R-successor (R-predecessor) of x (y). Ancestor is the transitive closure of predecessor, and descendant is the transitive closure of successor.
G is said to contain a clash if for some A ∈ NC and node x of G, {A, ¬A} ⊆ L(x).
The tableaux algorithm for checking concept satisfiability of C w.r.t. T starts with the completion tree G = ({r0}, ∅, L) where L(r0) = {nnf(C)}. G is then expanded by repeatedly applying the expansion rules given in Figure 1, stopping if a clash occurs. In order to ensure termination we need to restrict the creation of new nodes in the v-rule: if 1. C1 v C2 ∈ T , and
2. {¬˙ C1, nnf(C2)} ∩ L(x) = ∅ then set L(x) = L(x) ∪ {C} for some C ∈ {¬˙ C1, nnf(C2)} u-rule: if 1. C1 u C2 ∈ L(x), and
2. {C1, C2} 6⊆ L(x) then set L(x) = L(x) ∪ {C1, C2} t-rule: if 1. C1 t C2 ∈ L(x), and
2. {C1, C2} ∩ L(x) = ∅ then set L(x) = L(x) ∪ {C} for some C ∈ {C1, C2} ∃-rule: if 1. ∃R.C ∈ L(x), x is not blocked, and
2. x has no R-successor y with C ∈ L(y), then create a new node y with L(hx, yi) = R
and L(y) = {C} ∀-rule: if 1. ∀R.C ∈ L(x), and
2. there is an R-successor y of x such that C ∈/ L(y) then set L(y) = L(y) ∪ {C}
Definition 3 (Blocking) A node x is label blocked if it has an ancestor y such that L(x) ⊆ L(y). In this case, we say that y blocks x. A node is blocked if either it is label blocked or its predecessor is blocked.
When nodes in a branch of the completion tree resemble ancestor nodes, a block is established to ensure that further applications of ∃-rule are not applied to the blocked nodes (and therefore ensure termination). Definition 4 A completion tree G is called complete if no expansion rule can be applied. G is clash-free if no node contains a clash.
A tableaux algorithm for checking concept satisfiability of an ALC concept C w.r.t. a TBox T builds a completion tree for C. If a complete and clash-free tree can be obtained, the algorithm returns “satisfiable”; otherwise, if it was unable to build such a tree, it returns “unsatisfiable”.
Theorem 5. (decision procedure, [
Model Checking Definition 6 (Kripke Structure) Let V be a set of Boolean variables. A Kripke structure M over V is a quadruple M = (S, I , R, L) where 1. S is a finite set of states. 2. I ⊆ S is the set of initial states. 3. R ⊆ S × S is a transition relation that must be total, that is, for every state s ∈ S there is a state s0 ∈ S such that R(s, s0). 4. L : S → 2V is a function that labels each state with the set of variables true in that state.
We view each state s as a truth assignment to the variables in V . We view a set of states as a Boolean function over V , characterizing the set. For example, the set of initial states, I , is considered as a Boolean function over V . Thus, if a state s belongs to I , we write s |= I . Similarly, if vi ∈ L(s) we write s |= vi, and if vi 6∈ L(s) we write s |= ¬vi.
In practice, the full Kripke structure of a system is not explicitly given. Rather, a
model is described by a set of Boolean variables V = {v1, ..., vn}, their initial values
and their next-state assignments. The definition we give below is an abstraction of the
input language of SMV [
Definition 7 (Model Description) Let V = {v1, ..., vn} be a set of Boolean variables. A tuple MD = (IMD , [hc1, c01i, ..., hcn, c0ni]) is a Model Description over V where IM D, ci, c0i are Boolean expressions over V .
The semantics of a model description defines a Kripke structure MMD = (S, IM , R, L), where S = 2V , L(s) = s, IM = {s|s |= IMD }, and R = {(s, s0) : ∀1 ≤ i ≤ n, s |= ci implies s0 |= ¬vi and s |= c0i ∧ ¬ci implies s0 |= vi}.
Intuitively, a pair hci, c0ii defines the next-state assignment of variable vi in terms of the
current values of {v1, ..., vn}. That is,
next(vi) =
0
1
{0, 1}
if ci
if c0i ∧ ¬ci
otherwise
where the assignment {0, 1} indicates that for every possible next-state value of
variables v1, ...vi−1, vi+1, ..., vn there must exist a next-state with vi = 1, and a next-state
with vi = 0.
Computation Tree Logic (CTL) [
The formal semantics of a CTL formula are defined with respect to a Kripke structure M = (S, I, R, L) over a set of variables V = {v1, ..., vk}. A path in M is an infinite sequence of states (s0, s1, ...) such that each successive pair of states (si, si+1) is an element of R. The notation M, s |= ϕ, means that the formula ϕ is true in state s of the model M .
– M, s |= p iff s |= p – M, s |= ¬ϕ iff M, s 6|= ϕ – M, s |= ϕ ∧ ψ iff M, s |= ϕ and M, s |= ψ – M, s0 |= AXp iff for all paths (s0, s1, ...), M, s1 |= p – M, s0 |= EXp iff there exists a path (s0, s1, ...), M, s1 |= p – M, s0 |= A[ϕUψ] iff for all paths (s0, s1, ...), there exists i such that M, si |= ψ and for all 0 ≤ j < i,M, sj |= ϕ – M, s0 |= E[ϕUψ] iff there exists a path (s0, s1, ...), and there exists i such that
M, si |= ψ and for all 0 ≤ j < i,M, sj |= ϕ We say that a Kripke structure M = (S, I, R, L) satisfies a CTL formula ϕ (M |= ϕ) if there exists a state si such that si |= I and M, si |= ϕ.
Linear Temporal Logic (LTL) [
Model checking of an LTL formula ϕ is commonly done by first building a Bu¨chi
automaton A¬ϕ that accepts ¬ϕ [
Note that the LTL formula Fp and the CTL formula AFp are equivalent. We sometimes use the CTL notation, since the description of an erroneous path, (EG¬p) is not possible in LTL.
Model description as a DL terminology
We show how a model description can be encoded as a TBox over the Description
Logic dialect ALC. This translation is taken from [
Let M D = (I, [hc1, c01i, ..., hcn, c0ni]) be a model description for the model MMD = (S, I, R, L), over V = {v1, ..., vn}. We generate a TBox TMD , linear in the size of MD . For each variable vi ∈ V we introduce one primitive concept Vi, where Vi denotes vi = 1 and ¬Vi denotes vi = 0. We introduce one primitive role R corresponding to the transition relation of the model. Given a Boolean expression p over the state variables v1, ..., vn, we denote D(p) the concept P derived from p by replacing each vi in p with Vi, and ∨, ∧, ¬ with u, t, ¬ respectively. For example, if p = (¬v1 ∧ v2), then D(p) = (¬V1 u V2).
We define the concept S0 to represent the set of initial states: S0 = D(I). We define Ci = D(ci), C0i = D(c0i), for all 1 ≤ i ≤ n. We then introduce concept inclusions describing the model: for each pair hci, c0ii we introduce the inclusions
Ci v ∀R.¬Vi (¬Ci u C0i) v ∀R.Vi The first inclusion ensures that in any interpretation, an individual that belongs to Ci can be related by R only to individuals that do not belong to Vi. As we show in the sequel, individuals correspond to states in the model MMD . This means that when ci holds in a state s, all neighbor states of s must have vi = 0. The above inclusions thus restrict the role R to agree with the definition of R in the model description.
The TBox built above describes the model only, and does not consider the specification to be verified. Legal interpretations include for example the empty interpretation, and are not necessarily useful for verification. In order to use DL reasoning for model checking we need to add axioms to the terminology, to stand for the specification. The method we describe below adds concept inclusions that describe an error in the model. Interpretations will therefore be legal sub-models that demonstrate an erroneous behavior. 3
Model Checking Liveness Formulas using DL We first consider a liveness formula of the type AF(p), with p being a Boolean expression. For our method to work, we need to define a buggy path, that is, a path on which p never happens. We thus look for a representation of EG(¬p).
The following is a known equation [
Note that the expression ∃R.C can be seen as taking one step through R, and thus corresponds, in a sense, to the CTL expression EX(C).
Let TMD be the terminology we get by adding Equation (2) to TMD . We define the 0 concept Cϕ by Cϕ v S0 u EGnotP. In order to verify ϕ, we now check whether Cϕ is satisfiable with respect to our terminology: TM0 D |=dl Cϕ ? A positive answer from the DL reasoning tool will be accompanied by an interpretation for TMD in which Cϕ is not 0 empty. This interpretation can serve as a witness to EG(¬p), or as a counterexample to AF(p). The following proposition states our result formally.
Proposition 8. MMD 6|= ϕ if and only if TM0 D |=dl Cϕ.
The proof can be found in [
Example. Consider a model of a buggy three-bit counter, for which the least and most significant bits behave as expected, but the middle bit has a bug: when its current value is 0, it may assume any value in the next state, and when its current value is 1 it keeps its value in the next state. This behavior can be described as a model description (using (2) S0 v (¬V1 u ¬V2 u ¬V3)
V1 v ∀R.¬V1 ¬V1 v ∀R.V1
V2 v ∀R.V2 (V1 u V2 u V3) v ∀R.¬V3 (¬V3 u (¬V1 t ¬V2)) v ∀R.¬V3
(V1 u V2 u ¬V3) v ∀R.V3 (V3 u (¬V1 t ¬V2)) v ∀R.V3 > for v1 ∨ ¬v1 and ⊥ for v1 ∧ ¬v1) in the following way.
Counter = (I, [hv1, >i, h⊥, v2i, h(v1 ∧ v2 ∧ v3) ∨ (¬v3 ∧ (¬v1 ∨ ¬v2)), >i]) with I = ¬v1 ∧ ¬v2 ∧ ¬v3. Figure 2 describes the Kripke structure for Counter. Note that in the figure, v1 is the right-most bit.
The description of the model as a TBox TCounter over ALC has three concepts V3, V2, V1 and one role R. The concept inclusions for TCounter are given in Figure 2. For convenience we broke the concept inclusions describing the behavior of V3 into two parts. Note that there is only one concept inclusion describing the behavior of V2, since it is free to change when its value is 0.
Let the formula to be verified be ϕ = AF(v1 ∧ ¬v2 ∧ v3), asserting that the state (101) should be reachable on every path. Translated into DL, we add the following inclusion to TCounter (presented in Fig. 2):
and define Cϕ v S0 u EGnotP. Note that since the formula does not hold in the model, running the DL query TCounter |=dl Cϕ is expected to be satisfiable. A possible model (or counterexample to the formula) could be the loop (000),(001),(000)...
As discussed in Section 2.2, liveness formulas are usually accompanied by one or more fairness constraints, and need to be verified on fair paths only. In our example, let the fairness constraint be Fairness (v1 ∧ v2 ∧ v3), asserting that only paths on which the state (111) occurs infinitely often should be considered. The loop (000),(001),(000) is not a fair counterexample, and a different path should be sought . A fair counterexample will then be (000),(011),(110),(111),(010),(011). In the section below we discuss how fairness can be implemented in DL. 4
Realizing Fairness in Tableaux Reasoning While a model and a liveness formula can be encoded as a terminology over ALC, this is not the case for a fairness proposition. If, as in our case, the proposition is mapped to a primitive concept FC and we are using tableaux reasoning, then no bound is known a-priori on the depth in which the concept FC may appear in a completion tree. Thus expressing the existence of a fairness condition can be seen as reachability, which can not be expressed in first order logic.
We propose a modification to the tableaux procedure to support fairness. Our procedure is both terminating and sound: if a fair cycle is found, it is a correct one. However, the procedure is not complete, that is, there are cases where a fair cycle exits, but our procedure fails to find it. We show that by an iterative application of the algorithm, completeness can also be achieved. In the remainder of this section we discuss the theoretical and implementation considerations for realizing fairness in DL reasoning.
Recall from Section 2.2 that fairness constraints in model checking are variables that should be satisfied over all cycles in the model. In tableaux reasoning, a model is represented by a completion tree, and cycles in the model are represented by blocked nodes. If node x is blocked by the node x0 then there exists a path of nodes x0, . . . , xn such that L(hx0, x1i) = R0, . . . , L(hxn, xi) = Rn and Ri are the roles occurring in a terminology. This represents the blocking loop (x0, . . . , xn)∗.
In order to implement reasoning with fairness, we need to reject those completion trees that corresponds to unfair computations. Let FC be a fairness constraint. Completion tree G is unfair w.r.t. FC if there is loop (x0, . . . , xn)∗ such that FC ∈/ L(xi) for all 0 ≤ i ≤ n. G is called fair model of a concept C w.r.t. fairness constraint FC if G is a model of C which is not unfair w.r.t. FC.
Modifying Tableaux to Support Fairness Our approach to implementing fairness is to build a complete and clash-free completion tree and, if it is unfair, to attempt to make it fair by adding the fairness constraint to the label of some node involved in a cycle. To accomplish this, the tableaux algorithm is extended with the new rule illustrated in Figure 3. (Note that this new rule must also have a lower priority than all existing rules.) established.
v ∃R.C u ¬B} without any fairness constraint but not satisfiable w.r.t. fairness constraint FC = B. Indeed, every node of the completion tree for C will be labeled with ¬B, and it is not possible to add B to a cycle without a Theorem 9. The tableaux algorithm with f airness-rule terminates and is sound (if a complete clash-free fair completion tree for C is found then C is satisfiable). Proof Outline. Soundness is straightforward. To prove termination, assume WLOG that the completion tree is a single path. There are three cases to consider after a first application of f airness-rule to a given blocking loop: (1) it is subsequently possible to compute a complete clash-free fair completion tree before a second application of f airness-rule, (2) a clash occurs before a second application of the f airness-rule, or (3) a subsequent application of f airness-rule is required. Both cases (1) and (2) lead to termination. Case (3) implies that the addition of an FC to a label inside the cycle breaks the blocking condition and leads to a new cycle. The algorithm therefore proceeds by adding an FC inside the next loop. Again, there are three possible outcomes, with two resulting in termination. Ultimately, there is a sequence of case (3) that transpire for which adding an FC forces unblocking the last node and moving the blocking loop forward. However, after a finite number of occurrences of case (3), there must eventually be two nodes labeled by the same FC for which the labels are the same (since the TBox is finite). One of these nodes will then block the other, and the fair loop must then be f airness-rule: if 1. x is a node blocked by x0, (x0, . . . , xn)∗ is a cycle corresponding to x, then set L(xi) = L(xi) ∪ {FC} for some i : 0 ≤ i ≤ n
2. FC is a fairness constraint such that for every i, 0 ≤ i ≤ n, FC ∈/ L(xi)
Note that there is no guarantee of completeness, that is, if a concept is satisfiable w.r.t. FC, that the tableaux procedure builds a complete clash-free fair completion tree. This is a consequence of the way blocking is defined. To illustrate, consider a TBox consisting of two GCIs: T2 = {C v ¬B, > v ∃R.>}. Concept C is satisfiable w.r.t. T2 since there exists a complete and clash-free completion tree G = (V, E, L) such that V = {x, y}, E = {hx, yi}, L(x) = {C, ¬B, ∃R.>}, L(y) = {∃R.>}, L(hx, yi) = R. Here, node y is blocked by x. However, the fair algorithm with FC = B will return “unsatisfiable” since the clash appears immediately following the addition of FC to the only possible node x. However, there is complete and clash-free fair completion tree for this case: G0 = (V 0, E0, L0) with V 0 = {x, y, z}, E0 = {hx, yi, hy, zi}, L0(x) = {C, ¬B, ∃R.>}, L0(y) = {B, ∃R.>}, L0(z) = {∃R.>}, L0(hx, yi) = L0(hy, zi) = R. Here, node z can be label blocked by either x or y. To address this problem, we introduce the notion of n-blocking.
Definition 10 (n-Blocking) Let n be a non-negative integer. Node x is n-blocked by node x0 with blocking loop x0, . . . , xm if x is blocked by x0 by the same blocking loop and n ≤ m, that is, there are at least n nodes in the blocking loop.
Observe that normal blocking can be viewed as a 0-blocking. Also note that replacing normal blocking with n-blocking in the (fair) tableaux algorithm will clearly preserve termination, soundness and (in the unfair case) completeness.
In the example above the algorithm with 1-blocking will find that C is satisfiable w.r.t. T2, producing the completion tree G0, with node z being blocked by x. not exceeding n.
Theorem 11. Let C denote a concept, T a TBox, FC a fairness condition and n a non-negative integer. Then there is a tableaux-based decision procedure that returns “satisfiable” iff C is satisfiable w.r.t. T and FC with a fair blocking loop with length Proof Outline. Check the unfair satisfiability of C using tableaux. If it is unsatisfiable, return “unsatisfiable”. Then, for each 0 ≤ k ≤ n, run the fair algorithm with k-blocking. Return “satisfiable” if the algorithm returns “satisfiable” for some such k; otherwise return “unsatisfiable”. Termination and soundness are a simple consequence of Theorem 9. Completeness follows from the fact that no fair blocking loops for any possible length not exceeding n were found.
This approach can be used for detecting fair cycles in model checking. The length of a cycle cannot exceed the number of states in the model. Since models are finite, for every model M and specification ϕ there must exist n such that if M | contains a fair cycle with length not exceeding n. Thus, it is possible to build the TBox = ϕ then M outline for Theorem 11 to get a decision procedure for fair model checking. T using the technique from Section 3 and run the procedure suggested in our proof tu 5
Experimental Evaluation
We implemented the modified tableaux reasoning procedure described in Section 4 on
top of FaCT++ [
The models we acquired were originally written in the VIS [
It is evident from Figure 4 that our approach is efficacious in certain scenarios. For the “amba” benchmark, our system could not finish in the given time, while VIS was easily able to handle it in a fraction of a second. However, the “vsaR” benchmarks Benchmark vsaR - 6 vsaR - 8 vending amba2 - G3 amba3 - G3
Result Fail Fail Pass Pass Pass
Fig. 4. RUN TIMES FOR THE FAIRNESS VERIFICATION TASKS. proved simple for our reasoner while VIS was unable to finish in the given time. It seems that our method works better when a fair cycle does exist in the model. This can be explained by the fact that when a clash is found applying the fairness-rule, the n-blocking algorithm should be applied again with increased n. 6
Conclusion We have proposed a novel approach to fair cycle detection in model checking, using tableaux-based DL technology. While encoding of fairness constraints can not be expressed as a terminology over ALC, we showed how the tableaux reasoning procedure can be modified to support it.
Experiments, comparing our method to the model checker VIS [
We thank Armin Biere and Barbara Jobstmann for providing us the AIGER examples. Our work was partially supported by the SEALIFE project (IST-2006-027269), by NSERC of Canada and by the Cheriton Scholarship Fund of the Cheriton School of Computer Science.