=Paper=
{{Paper
|id=Vol-477/paper-18
|storemode=property
|title=Fair Cycle Detection using Description Logic Reasoning
|pdfUrl=https://ceur-ws.org/Vol-477/paper_56.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/Ben-DavidPTTW09
}}
==Fair Cycle Detection using Description Logic Reasoning==
https://ceur-ws.org/Vol-477/paper_56.pdf
Fair Cycle Detection using Description Logic Reasoning
Shoham Ben-David1 , Jeffrey Pound1 , Richard Trefler1 , Dmitry Tsarkov2 , Grant
Weddell1
1. David R. Cheriton School of Computer Science, University of Waterloo
2. School of Computer Science, University of Manchester
1 Introduction
Model checking ([12, 20], c.f.[11]) is a technique for verifying finite-state systems, that
has been proven to be very effective in the verification of hardware and software pro-
grams. In model checking, a model M , given as a set of state variables V and their
next-state relations, is verified against a temporal logic formula ϕ. When ϕ holds on all
computation paths of M we write M |= ϕ. The most commonly used temporal logics
are Linear Temporal Logic (LTL) [19] and Computation Tree Logic (CTL) [12].
Temporal logic specifications, whether given in LTL or in CTL, are roughly divided
into two basic categories [16, 1]: formulas that specify safety properties and formulas
that specify liveness properties. Informally, a safety formula states that “something bad
never happens”, and a violation of it can be shown by a finite prefix of a computation
path, reaching a bad state. A liveness formula asserts that “something good will even-
tually happen”, and a counterexample for it must contain an infinite path where a good
state never appears (a cycle, in case of a finite model). A simple example of a liveness
property is the CTL formula AFp asserting that the proposition p must appear even-
tually on every computation path of the model. In many cases, a liveness formula ϕ
is accompanied by a set of fairness constraints: Boolean events that must appear infi-
nitely often on a path to make it fair. When fairness constraints are present, ϕ should
only be verified on fair paths, and a counterexample should demonstrate a fair cycle: an
infinite computation path on which ϕ fails to hold, but each fairness constraint appears
infinitely often.
Symbolic model checking is performed using two main approaches. The first is
based on BDDs (e.g. SMV [17]), and the second is based on satisfiability solving (SAT)
technology [6]. For both methods, liveness formulas are considered more difficult to
verify than safety ones. Special attention has been devoted to detecting fair cycles in
recent years, both using BDDs methods [7, 8], and using SAT-based techniques [2, 14].
We consider a different approach for fair cycle detection, that makes use of Descrip-
tion 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 [15, 10]). We propose
a modification to the ALC reasoning technique based on tableau construction, that al-
lows us to detect a fair cycle. When constructing a tableaux, cycles are represented by
blocking. A node x is said to be blocked by a node y if there exists a path of nodes from
y to x, and the label of x is a subset of the label of y. Given a cycle in the tableau, and
2
a fairness constraint FC, we attempt to make the cycle fair by adding FC to the label of
a node in the cycle. To accomplish this, we extend the tableaux algorithm with a new
rule that we call a fairness rule. We show that our method is sound and terminating, and
discuss how completeness can be achieved.
We have implemented our method in the Description Logic reasoner FaCT++ [22],
and we present experimental results comparing our method with runs using the model
checker VIS [9]. Although running on a few examples only, the results demonstrate the
potential of our method, as they significantly outperform VIS on some of the examples.
The rest of the paper is organized as follows. In the next section we give the neces-
sary 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 re-
sults, and Section 6 concludes the paper.
2 Background and Definitions
2.1 Description Logic
Definition 1 (Description Logic ALC) Let NC and NR be disjoint sets of atomic con-
cepts {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 = C I ∩ DI ,
– (∃R.C)I = {e ∈ ∆I : ∃(e, e0 ) ∈ RI s.t. e0 ∈ C I }, and
– (¬C)I = ∆I \ C I .
An interpretation I satisfies a GCI (C v D) if C I ⊆ 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 C I 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
3
Form (NNF) of C, write ¬C ˙ to denote the NNF of ¬C, and write sub(C) to denote the
set of all subconcepts
S of C (including C) and their negation. For a TBox T we define
sub(T ) = (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
˙ 1 , nnf(C2 )} ∩ L(x) = ∅
2. {¬C
then set L(x) = L(x) ∪ {C} for some C ∈ {¬C
˙ 1 , 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
/ L(y)
2. there is an R-successor y of x such that C ∈
then set L(y) = L(y) ∪ {C}
Fig. 1. Tableaux expansion rules for ALC
completion tree. The notion of blocking is used for this purpose.
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).
4
Definition 4 A completion tree G is called complete if no expansion rule can be ap-
plied. 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, [21]) The tableaux algorithm always terminates for
a given ALC concept C and TBox T , and returns “satisfiable” iff C is satisfiable w.r.t.
a TBox T .
2.2 Model Checking
Definition 6 (Kripke Structure) Let V be a set of Boolean variables. A Kripke struc-
ture 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 [17].
Definition 7 (Model Description) Let V = {v1 , ..., vn } be a set of Boolean variables.
A tuple MD = (IMD , [hc1 , c01 i, ..., hcn , c0n i]) 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 , c0i i defines the next-state assignment of variable vi in terms of the
current values of {v1 , ..., vn }. That is,
0 if ci
next(vi ) = 1 if c0i ∧ ¬ci
{0, 1} otherwise
where the assignment {0, 1} indicates that for every possible next-state value of vari-
ables v1 , ...vi−1 , vi+1 , ..., vn there must exist a next-state with vi = 1, and a next-state
with vi = 0.
5
Computation Tree Logic (CTL) [12]. Given a finite set AP of atomic propositions,
formulas of CTL are recursively defined as follows:
– Every atomic proposition is a CTL formula.
• ¬ϕ •ϕ∧ψ • AXϕ
– If ϕ and ψ are CTL formulas then so are:
• EXϕ • A[ϕUψ] • E[ϕUψ]
Additional operators are defined as syntactic sugaring of those above:
• AFϕ = A[true Uϕ] • EFϕ = E[true Uϕ]
• AGϕ = ¬E[true U¬ϕ] • EGϕ = ¬A[true U¬ϕ]
The formal semantics of a CTL formula are defined with respect to a Kripke struc-
ture 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) [19]. Linear temporal logic uses the same temporal
operators as CTL, but has no path quantifiers. An LTL formula is thus evaluated with
respect to a given path rather than a Kripke structure. A formula ϕ is said to hold in a
Kripke structure M if it holds along all paths that start from an initial state of M .
Fairness constraints and LTL model checking. Different definitions of fairness con-
straints exist in the literature [13]. The fairness definition used for model checking can
be presented as the LTL formula GFp, describing a fair path as one on which the propo-
sition p occurs infinitely often (or at least once in a loop).
Model checking of an LTL formula ϕ is commonly done by first building a Büchi
automaton A¬ϕ that accepts ¬ϕ [23]. The composition of A¬ϕ (presented as a state-
machine) with the model M (denoted A¬ϕ ||M ) should then be empty: a path, if found,
satisfies ¬ϕ, and therefore demonstrate a counterexample for ϕ. Note that the accep-
tance condition of a Büchi automaton requires that an accepting state is visited infi-
nitely often. Translated into model checking notation, the formula F(false) is verified
on A¬ϕ ||M , with fairness constraints that are the Büchi acceptance conditions. Thus
model checking of any LTL formula is reduced to model checking of a simple Fp for-
mula on fair paths.
Note that the LTL formula Fp and the CTL formula AFp are equivalent. We some-
times use the CTL notation, since the description of an erroneous path, (EG¬p) is not
possible in LTL.
6
2.3 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 [3], where it was used for bounded
model checking of safety formulas. In Section 3 we demonstrate how unbounded model
checking of liveness formulas can be achieved.
Let M D = (I, [hc1 , c01 i, ..., hcn , c0n i]) 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 , c0i i 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 specifi-
cation 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 behav-
ior.
3 Model Checking Liveness Formulas using DL
We first consider a liveness formula of the type AF(p), with p being a Boolean expres-
sion. 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 [12], that we use for our translation into DL:
EG(¬p) = ¬p ∧ EX(EG(¬p)) (1)
Let M D = (I, [hc1 , c01 i, ..., hcn , c0n i]) be a model description for the model MMD =
(S, I, R, L) over V = {v1 , ..., vn }, and let TMD be the terminology built for it as
described in Section 2.3. Let ϕ = AF(p) be the formula to be verified, with p being
a Boolean expression over the variables v1 , ..., vn . Let P= D(p) the corresponding
7
concept. We introduce a new concept called EGnotP, and add the following concept
inclusion to TMD :
EGnotP v ¬P u ∃R.EGnotP (2)
Note that the expression ∃R.C can be seen as taking one step through R, and thus corre-
sponds, in a sense, to the CTL expression EX(C).
0
Let TMD be the terminology we get by adding Equation (2) to TMD . We define the
concept Cϕ by Cϕ v S0 u EGnotP. In order to verify ϕ, we now check whether Cϕ is
0
satisfiable with respect to our terminology: TMD |=dl Cϕ ? A positive answer from the
0
DL reasoning tool will be accompanied by an interpretation for TMD in which Cϕ is not
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.
0
Proposition 8. MMD 6|= ϕ if and only if TMD |=dl Cϕ .
The proof can be found in [4].
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
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
Fig. 2. Terminology and Kirpke Structure for “Counter”
> for v1 ∨ ¬v1 and ⊥ for v1 ∧ ¬v1 ) in the following way.
Counter = (I, [hv1 , >i, h⊥, v2 i, 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
8
inclusion to TCounter (presented in Fig. 2):
EGnotP v (¬V1 t V2 t ¬V3 ) u ∃R.EGnotP
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 counterex-
ample 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 proce-
dure 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 the-
oretical 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 , x1 i) = 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. Comple-
/ L(xi ) for
tion tree G is unfair w.r.t. FC if there is loop (x0 , . . . , xn )∗ such that FC ∈
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.)
9
f airness-rule: if 1. x is a node blocked by x0 , (x0 , . . . , xn )∗ is a cycle corresponding to x,
2. FC is a fairness constraint such that for every i, 0 ≤ i ≤ n, FC ∈ / L(xi )
then set L(xi ) = L(xi ) ∪ {FC} for some i : 0 ≤ i ≤ n
Fig. 3. Expansion rule for fairness
It might be the case that there is no fair model. For example, the concept C is
satisfiable w.r.t. TBox T1 = {C 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
resulting clash.
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 ap-
plication 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 for-
ward. 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
established. t
u
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 , E 0 , L0 ) with V 0 = {x, y, z}, E 0 = {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.
10
Observe that normal blocking can be viewed as a 0-blocking. Also note that re-
placing 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.
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
not exceeding n.
Proof Outline. Check the unfair satisfiability of C using tableaux. If it is unsatisfi-
able, 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. t
u
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 |= ϕ then M
contains a fair cycle with length not exceeding n. Thus, it is possible to build the TBox
T using the technique from Section 3 and run the procedure suggested in our proof
outline for Theorem 11 to get a decision procedure for fair model checking.
5 Experimental Evaluation
We implemented the modified tableaux reasoning procedure described in Section 4 on
top of FaCT++ [22], a state-of-the-art description logic reasoner. In order to run real
examples, we wrote a translator from the AIGER [5] format, that builds a terminology
as described in Section 3. Liveness formulas were translated in the AIGER models into
Büchi automata (see section 2.2), and the fairness constraints were passed to FaCT++
using a new construct in the interface language.
The models we acquired were originally written in the VIS [9] input language, and
were translated into AIGER using different tools. We present results running three sets
of benchmarks with fairness constraints. The “amba” benchmark encodes an Advanced
High Performance Bus. The “vsa” benchmarks encode a simple architecture for a mi-
croprocessor. In each of the vsa benchmarks, the number indicates the datawidth of the
microprocessor. The “Vending” example is part of the VIS distribution.
Experimental Results. Figure 4 summarizes our proof-of-concept results. The exam-
ples were run on Intel CoreDuo computer, 3.4 HGz, 2Gb RAM, Linux SuSE 11.0.
Times reported are in seconds and a time of DNF indicates that the run did not finish in
the alloted time of 1 hour.
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
11
Benchmark Result Size (vars) FaCT++ VIS
vsaR - 6 Fail 170 9.9s DNF
vsaR - 8 Fail 204 12.3s DNF
vending Pass 64 DNF 1.1s
amba2 - G3 Pass 63 DNF 0.7s
amba3 - G3 Pass 77 DNF 17.7s
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 ex-
pressed 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 [9], show mixed
results. On some models our method significantly outperform VIS, while other models
demonstrate the opposite. This is not too surprising. In the model checking community
it has been recognized that no single method can outperform others on all models [18].
State of the art model checkers invoke multiple algorithms for each model checking
problem, to speed up verification. Our method can fit nicely in such a platform, speeding
up verification time for part of the models.
Acknowledgements
We thank Armin Biere and Barbara Jobstmann for providing us the AIGER exam-
ples. 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.
References
1. M. W. Alford, J. P. Ansart, G. Hommel, L. Lamport, B. Liskov, G. P. Mullery, and F. B.
Schneider. Distributed systems: methods and tools for specification. An advanced course.
Springer-Verlag New York, Inc., New York, NY, USA, 1985.
2. Mohammad Awedh and Fabio Somenzi. Proving more properties with bounded model
checking. In CAV, pages 96–108, 2004.
3. S. Ben-David, R. Trefler, and G. Weddell. Bounded model checking with description logic
reasoning. In Automated Reasoning with Analytic Tableaux and Related Methods, LNAI
4548-0060, pages 60–72, July 2007.
12
4. Shoham Ben-David, Richard Trefler, Dmitry Tsarkov, and Grant Weddell. Checking in-
evitability and invariance using description logic technology, 2008. Technical report CS-
2008-28, University of Waterloo.
5. A. Biere. The AIGER And-Inverter Graph (AIG) Format, 2007. http://fmv.jku.at/aiger/.
6. A. Biere, A. Cimatti, E. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs.
In TACAS, 1999.
7. Roderick Bloem, Harold N. Gabow, and Fabio Somenzi. An algorithm for strongly con-
nected component analysis in n log n symbolic steps. In Formal Methods in Computer Aided
Design, pages 37–54. Springer-Verlag, 2000.
8. Roderick Bloem, Harold N. Gabow, and Fabio Somenzi. An algorithm for strongly con-
nected component analysis in log symbolic steps. Formal Methods in System Design,
28(1):37–56, 2006.
9. R. K. Brayton, G. D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng,
S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. K. Ranjan, S. Sarwary, T. R.
Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In CAV, 1996.
10. D. Calvanese, G. De Giacomo, and M. Lenzerini. Reasoning in expressive description logics
with fixpoints based on automata on infinite trees. In IJCAI, pages 84–89, 1999.
11. E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, 2000.
12. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using
branching time temporal logic. In Proc. Workshop on Logics of Programs, LNCS 131, pages
52–71. Springer-Verlag, 1981.
13. Nissim Francez. Fairness. Springer-Verlag New York, Inc., New York, NY, USA, 1986.
14. Malay K. Ganai, Aarti Gupta, and Pranav Ashar. Beyond safety: customized sat-based model
checking. In DAC, pages 738–743, 2005.
15. Giuseppe De Giacomo and Fabio Massacci. Combining deduction and model checking into
tableaux and algorithms for converse-PDL. Information and Computation, 162(1-2):117–
137, 2000.
16. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on
Software Engineering, SE–3(2):125–143, 1977.
17. K. McMillan. Symbolic model checking, 1993.
18. Ziv Nevo. User-friendly model checking: Automatically configuring algorithms with rule-
base/pe. In 4th Haifa Verification Conference, October 2008.
19. Amir Pnueli. The temporal logic of programs. In 18th IEEE Symposium on Foundation of
Computer Science, pages 46–57, 1977.
20. J. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In 5th
International Symposium on Programming, 1982.
21. Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with comple-
ments. Artificial Intelligence, 48(1):1–26, 1991.
22. Dmitry Tsarkov and Ian Horrocks. FaCT++ description logic reasoner: System description.
In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume 4130 of
Lecture Notes in Artificial Intelligence, pages 292–297. Springer, 2006.
23. M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In F. Moller and
G. Birtwistle, editors, Logics for Concurrency: Structure versus Automata, volume 1043 of
Lecture Notes in Computer Science, pages 238–266. Springer-Verlag, Berlin, 1996.