# Counterexample-Preserving Reduction for Symbolic Model Checking

Authors: Wanwei Liu; Rui Wang; Xianjin Fu; Ji Wang; Wei Dong; Xiaoguang Mao
Journal: Journal of Applied Mathematics
 (2014)

---

## Abstract

The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique “counterexample-preserving reduction” (CePRe, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.


---

## Body

## 1. Introduction

LTL [1] is one of the most frequently used specification languages in model checking (cf. [2]). It designates properties over a linear structure, which can be viewed as an execution of the program. The task of LTL model checking is to search the state space (explicitly or implicitly), with the goal of detecting the existence of feasible traces violating the specification. If such traces exist, the model checker will report one of them as a “counterexample”; otherwise, the model checker will give an affirmative report.It can be shown that the complexity of LTL model checking forM⊨φ is in O(|M|×2|φ|); meanwhile, the nesting depth of temporal operators might be the major factor affecting the cost in compiling LTL formulae. Hence, it is reasonable to simplify the specification before conducting model checking. For example, in [3], Somenzi and Bloem provided a set of rewriting schemas for simplifying LTL specifications, and these rewriting schemas preserve logical equivalence.One may argue that “a majority of LTL formulae used in real applications are simple, succinct rather than complicated” Nevertheless, we might need to observe the following facts.(i)
Some LTL formula, for exampleF(pUq), is usually considered to be a “simple” one. Nevertheless, it can be further simplified to Fq, and this fact tends to be ignored (on one hand, pUq implies Fq, and hence F(pUq) implies FFq (i.e., Fq); on the other hand, q implies pUq, and hence Fq implies F(pUq)).(ii)
Indeed, people do use complicated specifications in the real industrial field, as well as in some standard benchmark (cf. [4]).(iii)
Last but not least, not all specifications are designated manually. Actually, some formulae are generated by specification-generaton-tools (e.g., ProSpec). Indeed, one may find that lots of these machine-generated specifications can be simplified.Symbolic model checking [5] is one of the most significant breakthroughs in model checking, and two major fashions of symbolic model checking are widely used: one is the BDD-based manner [6] and the other is SAT-based manner, such as BMC [7] or PDR [8–11] algorithms.Instead of using an explicit representation, the symbolic approach represents state space with a series of Boolean formulae. This enables implicit manipulation of the verification process and it usually leads to an efficient implementation [12]. Meanwhile, the symbolic encoding of transitions and invariants of the model provides heuristic information to simplify the specification. For example,(i)
the formulaepUq and (rUp)Uq can be, respectively, reduced as q and (rUp)∨q, if we know that p→q holds everywhere in the model;(ii)
each occurrence ofGθ in the specification can be replaced with ⊤ (i.e., logically true), if we can inductively infer that the Boolean formula θ holds at each reachable state in the model. Actually, we can make sure of these conditions with the following efforts.(i)
To ensure that “p→q holds everywhere in the model',' one possible way is to make sure that p→q is aninvariant in the model—that is, just to examine if ρ∧¬(p→q) is unsatisfiable (we in the latter denote it as ρ⊢p→q), where ρ is the Boolean encoding of the model's transition relation.(ii)
Likely, to justify thatθ holds at each reachable state (note that a “dead-end” has no infinite path starting from it, and hence we may safely omit dead-ends in the model when doing this), it suffices to ensure that θ0⊢θ and ρ⊢θ→θ′, where θ0 is the initial condition of the model. We could do this because the component ρ should be satisfied at each transition step. Hence, it encloses both “local invariants” and “transitional invariants”. For example, if ρ=p∧(q→q′), then we may consider p as a local invariant, whereas q→q′ is a transitional invariant.Hence, this provides an opportunity to replace the specification with a simpler one, accompanied with some lightweight extra task of condition detection. Even if such detection fails, the overhead is usually negligible. More importantly, such reductions can be performed before starting model checking. At the same time, such kind of simplification is not always feasible to conduct manually; the reason is that the scale of boolean facilities is too large to be effectively handled by humans. Therefore, it is reasonable of leveraging the SAT-solvers to accomplish this task.In this paper, we systematically investigate the above idea and tentatively name this techniquecounter example-preserving reduction (CePRe, for short). To justify it, we have extended NuSMV and implemented CePRe as an upfront option for LTL model checking. Subsequently, we conduct experiments over both industrial benchmarks and randomly generated cases. Experimental results show that CePRe can improve the efficiency significantly.This paper is organized as follows. Section2 revisits some basic notions. Section 3 introduces the details of the CePRe technique and Section 4 gives a formal treatment of performance analysis. In Section 5, the experimental results over industrial benchmarks and over random generated cases are given. We summarize the whole paper with Section 6.


## 2. Preliminaries

We presuppose a countable setP ofatomic propositions, ranging over p, q, and so forth, and for each proposition p∈P, we create aprimed versionp′ (not belonging to P) for it. For each set V⊆P, we define V'≜{p′∣p∈V}. We use B(V) to denote the set of Boolean formulae over V. Similarly, we denote by B(V∪V') the set of Boolean formulae built up from V∪V'. The scope of theprime operator can be naturally lifted to Boolean formulae over B(V), by defining
(1)⊤′=⊤,⊥′=⊥,(¬θ)′≜¬θ′,(θ1⟶θ2)′≜θ1′⟶θ2′.Anassignment is a subset V of P. Intuitively, it assigns 1 (or true) to the propositions belonging to V and assigns 0 (or false) to the other propositions. For each V⊆U⊆P and θ∈B(U), we denote by V⊩θ if θ is evaluated to 1 under the assignment V.Aunited assignment is a pair (V1,V2), where both V1 and V2 are subsets of P. It assigns 1 to the propositions belonging to V1∪V2′ and assigns 0 to the other propositions. Suppose that V1,V2⊆U⊆P and θ∈B(U∪U′); we also write (V1,V2)⊩θ if θ is evaluated to 1 under the united assignment (V1,V2).LTL formulae can be inductively defined as follows.(i)
⊥ and ⊤ are LTL formulae.(ii)
Each propositionp∈P is an LTL formula.(iii)
If bothφ1 and φ2 are LTL formulae, so does φ1→φ2.(iv)
Ifφ is an LTL formula, then Xφ and Yφ are LTL formulae.(v)
Ifφ1 and φ2 are LTL formulae, then both φ1Uφ2 and φ1Sφ2 are LTL formulae.Semantics of an LTL formula is defined w.r.t. alinear structureπ∈(2P)ω (i.e., π is an infinite word over the alphabet 2P) and a position i≺ω. Inductively:(i)
π,i⊨⊤ and π,i⊭⊥;(ii)
π,i⊨p if and only if π(i)⊩p (where π(i) is the ith letter of π, which can be viewed as an assignment);(iii)
π,i⊨φ1→φ2 if and only if either π,i⊭φ1 or π,i⊨φ2;(iv)
π,i⊨Xφ if and only if π,i+1⊨φ;(v)
π,i⊨Yφ if and only if i>0 and π,i-1⊨φ;(vi)
π,i⊨φ1Uφ2 if and only if there is some j≥i, s.t. π,j⊨φ2, and π,k⊨φ1 for each i≤k<j;(vii)
π,i⊨φ1Sφ2 if and only if there is some j≤i, s.t. π,j⊨φ2 and π,k⊨φ1 for each i≥k>j. For the sake of convenience, we may directly write π,0⊨φ as π⊨φ.As usual, we employ some derived Boolean connectives such as(2)¬φ≜φ⟶⊥,φ∨ψ≜¬φ⟶ψ,φ∧ψ≜¬(¬φ∨¬ψ)
and derived temporal operators such as
(3)Fφ≜⊤Uφ,Zφ≜¬Y¬φ,Oφ≜⊤Sφ,Gφ≜¬F¬φ,Hφ≜¬O¬φ,φRψ≜¬(¬φU¬ψ),φTψ≜¬(¬φS¬ψ).Temporal operators likeX, U, F, G, and R are calledfuture operators, whereas Y, Z, S, O, H, and T are calledpast operators. An LTL formula is said to bepure future (resp.,pure past) if it involves no past (resp., future) operators.Theorem 1 (see [13]).
Each LTL formula has an equivalent pure future expression.Theorem1 tells the fact that past operators do not add any expressive power to LTL formulae. Nevertheless, with these, we can give a much more succinct description in defining specifications.Given an LTL formulaφ, we denote by sub(φ) the set constituted with subformulae of φ. Particularly, we, respectively, denote by subU(φ) and subS(φ) the set consisting of “U-subformulae” and “S-subfomulae” of φ, where an U-formula (resp., S-formula) is a formula rooted at U (resp., S). (Note that Fφ is also a U-formula whereas Gφ is not.)Amodel is a tuple M=〈V,ρ,θ0,F〉, where(i)
V⊆P is a finite set of atomic propositions,(ii)
ρ∈B(V∪V') is thetransition relation,(iii)
θ0∈B(V) is theinitial condition,(iv)
F⊆B(V) is a set offairness constraints.Aderived linear structure of M is an infinite word π∈(2V)ω, such that(1)
π(0)⊩θ0;(2)
(π(i),π(i+1))⊩ρ for each i≺ω;(3)
for eachφ∈F, there are infinitely many i's having π(i)⊩φ.We denote byL(M) the set of derived linear structures of M and call it thelanguage of M.For a modelM and an LTL formula φ, we denote as M⊨φ if π⊨φ for each π∈L(M). Meanwhile, we define
(4)CE(φ,M)≜{π∈L(M)∣π⊭φ}
and call it thecounterexample set of φ w.r.t. M.


## 3. Counterexample-Preserving Reduction

We describe the CePRe technique in this section, but first of all, let us fix the components of the model and just let M be 〈V,ρ,θ0,F〉 in the rest of this section. For M, we are particularly concerned about formulae having the same counterexample set—we say that φ and ψ areinterreduceable w.r.t. M if and only if CE(φ,M)=CE(ψ,M), denoted as φ≈Mψ. Hence, φ≈Mψ implies that M⊨φ⇔M⊨ψ.The central part of CePRe is a series ofreduction rules being of the form
(5)Cond⊳φ≈Mψ(NAME),
where “Cond” is called theadditional condition.Though the relation≈M is actually symmetric, we always write the reduced formula on the righthand of the “≈” sign in a reduction rule. Since the model M is fixed, in this section, we omit it from the subscript. In addition, if the additional condition trivially holds, we will discard this part and directly write the rule as φ≈ψ, and in this case we say that this rule is “model-independent”; otherwise, we say that the underlying reduction rule is “model-dependent.”


### 3.1. The Basic Reduction Rules

In this section, we define some basic CePRe rules. First of all, we have some elementary reduction rules relating to model components, as depicted in Table 1. For the rules (Init), (Ind), and (Trans), the notation “⊢” occurring in the condition part stands for the “inferring” relation in propositional logic (ρ⊢θ if and only if ρ∧¬θ is unsatisfiable), and we here require that θ,θ1,θ2∈B(V).Table 1
Reduction rules about model components.
θ
0
⊢
θ
⊳
θ
≈
⊤ (Init)
ρ
⊢
θ
⊳
G
θ
≈
⊤ (Trans)
θ
∈
F
⊳
G
F
θ
≈
⊤ (Fair)
θ
0
⊢
θ; ρ⊢θ→θ′⊳Gθ≈⊤ (Ind)Subsequently, let us define a partial order “⊑” over unary temporal operators (and their combinations) as follows:
(6)F⊑GF⊑FG⊑GF⊑Xi⊑G(i≺ω)O⊑HO⊑OH⊑H,
where X0φ≜φ and Xi+1φ≜X(Xiφ).Assume thatPw,Ps∈{F,FG,GF,G,O,HO,OH,H}∪{Xi∣i≺ω} and Pw⊑Ps; then we have two model-indenpendent rules, as depicted in Table 2. Though these rules seem to be trivial, they are useful in doing combinational reductions (see the example given in Section 3.3).Table 2
Reduction rules of (Conj) and (Disj).
(
P
w
φ
∧
P
s
φ
)
≈
P
s
φ (Conj)
(
P
w
φ
∨
P
s
φ
)
≈
P
w
φ (Disj)Table3 provides some reduction rules that can be used to simplify nested temporal operators.Table 3
Reduction rules for formulae involving nested pure future operators.
F
(
φ
U
ψ
)
≈
F
ψ (FU)
φ
U
(
F
ψ
)
≈
F
ψ (UF)
F
F
φ
≈
F
φ (FF)
G
F
G
φ
≈
F
G
φ (GFG)Since we always stand at the starting point when doing model checking (i.e., the goal is to check ifπ,0⊨φ for each π∈L(M)), we can sometimes “erase” the outermost past operators, as depicted in Table 4.Table 4
Reduction rules for formulae involving (outermost) past operators.
Y
φ
≈
⊥ (Y)
O
φ
≈
φ (O)
φ
S
ψ
≈
φ (S)Table5 introduces a series of rules handling formulae involving adjacent past and future temporal operators.Table 5
Reduction rules for formulae involving adjacent past and future operators.
X
Y
φ
≈
φ (XY)
F
H
φ
≈
H
φ (FH)
F
O
φ
≈
F
φ
∨
O
φ (FO)
F
(
φ
S
ψ
)
≈
F
ψ
∨
φ
S
ψ (FS)We letθ1,θ2,… range over B(V) and let φ1,φ2,… be arbitrary LTL formulae, and then we have some model-dependent rules. The first group of such rules is listed in Table 6. Table 7 provides another set of model-dependent reduction rules, and these rules are mainly concerned with LTL formulae involving adjacent U-operators. Lastly, Table 8 provides some reduction rules that can be used to simplify formulae with mixed usage of U and R.Table 6
Reduction rules of (U) and (R).
ρ
⊢
θ
1
∨
θ
2
⊳
θ
1
U
θ
2
≈
F
θ
2 (U)
ρ
⊢
θ
2
→
θ
1
∨
θ
2
′
⊳
θ
1
R
θ
2
≈
θ
2 (R)Table 7
Reduction rules for formulae involving adjacentU operators.
ρ
⊢
θ
1
→
θ
2
⊳
θ
1
U
θ
2
≈
θ
2
(U[1→2])
ρ
⊢
θ
1
→
θ
3
⊳
(
θ
1
U
φ
2
)
U
θ
3
≈
φ
2
U
θ
3
(UU[1→3])
ρ
⊢
θ
2
→
θ
3
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
θ
3
∨
(
φ
1
U
θ
2
)
(UU[2→3])
ρ
⊢
θ
3
→
θ
2
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
(
φ
1
∨
θ
2
)
U
θ
3
(UU[3→2])
ρ
⊢
θ
2
→
θ
3
′
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
(
φ
1
∨
θ
2
)
U
θ
3
(UU[2→3′])
ρ
⊢
¬
θ
2
→
θ
3
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
F
θ
3
(UU[¬2→3])
ρ
⊢
θ
1
→
θ
2
⊳
θ
1
U
(
θ
2
U
φ
3
)
≈
θ
2
U
φ
3
(UU[1→2])
ρ
⊢
θ
1
→
θ
3
⊳
θ
1
U
(
φ
2
U
θ
3
)
≈
φ
2
U
θ
3
(UU[1→3])
ρ
⊢
θ
2
→
θ
1
⊳
θ
1
U
(
θ
2
U
φ
3
)
≈
θ
1
U
φ
3
(UU[2→1])Table 8
Reduction rules for formulae involving adjacentU and R operators.
ρ
⊢
θ
1
→
θ
3
⊳
(
θ
1
R
φ
2
)
U
θ
3
≈
(
(
θ
1
R
φ
2
)
∨
θ
3
)
∧
F
θ
3
(UR[1→3])
ρ
⊢
¬
θ
1
→
θ
3
⊳
(
θ
1
R
φ
2
)
U
θ
3
≈
φ
2
U
θ
3
(UR[¬1→3])
ρ
⊢
θ
1
→
θ
3
⊳
θ
1
U
(
φ
2
R
θ
3
)
≈
φ
2
R
θ
3
(UR[1→3])


### 3.2. Principles for Rule Generation

Actually, we may acquire more CePRe rules by applying someprinciples to the existing rules. In this section, we introduce four major principles in our framework.


#### 3.2.1. The Inversion Principle

We say that the temporal opertors “U and S,” “R and T,” “G and H,” and “F and O” are pairwiseinverse operators (The inverse operator of X may be Z or Y, which is judged from the context. Fortunately, in this paper, we need not consider this case). Then, for CePRe rules list in Table 3 and Tables 6–8, we may apply the following principle:
(7)ρ⊢θ⊳φ≈ψρ⊢θ~⊳inv(φ)≈inv(ψ),
namely,Inversion Principle. In detail:(i)
ifθ∈B(V) then θ~=θ; if θ∈B(V∪V'), then θ~ is obtained from θ by switching the primed and unprimed propositions;(ii)
inv(φ) and inv(ψ) are obtained from φ and ψ by swithing the temporal operators with their inverse operators, respectively.For example, one can apply this principle to(U) and (R), and then the following two rules
(8)ρ⊢θ1∨θ2⊳θ1Sθ2≈Oθ2(S)ρ⊢θ2′⟶θ1′∨θ2⊳θ1Tθ2≈θ2(T)
are immediately obtained.


#### 3.2.2. The Duality Principle

We say that “⊤ and ⊥,” “∧ and ∨,” “F and G,” “O and H,” “Y and Z,” “X and X itself,” “U and R,” and “T and S” are pairwise thedual operators. Then, theduality principle could be described as follows:
(9)Cond⊳φ≈ψCond-⊳dual(φ)≈dual(ψ).
We require that the condition “Cond” should be either trivial (in this case, the rule is a model-independent one) or of the form ρ⊢θ1→θ2, and in the latter case we have Cond¯=ρ⊢θ2→θ1. The formulae dual(φ) and dual(ψ) are obtained from φ and ψ by switching the operators with their dual.For example, apply the duality principle to the rules(FU), (UF), (FF), and (GFG), one may get the following new rules:
(10)G(φRψ)≈Gψ(GR),φR(Gψ)≈Gψ(RG),GGφ≈Gφ(GG),FGFφ≈GFφ(FGF).Note that when applying the duality principle to model-dependent rules, besides switching the operators, we also need to exchange the antecedent and subsequent on the righthand of⊢ in the condition part, in the case that the condition is of the form ρ⊢θ1→θ2. As an example, we may obtain the reduction rule
(11)ρ⊢θ3⟶θ2⊳(φ1Rθ2)Rθ3≈θ3∧(φ1Rθ2)(RR[3⟶2]),
by applying the duality principle to (UU[2→3]).


#### 3.2.3. The Composition Principle

Thecomposition principle can be formally described as follows:
(12)Cond1⊳φ1≈ψ1Cond2⊳φ2≈ψ2Cond1&Cond2⊳φ1≈ψ1ψ2φ2;
that is, if φi and ψi are interreduceable under the conditin Condi (i=1,2), then φ1 and ψ1ψ2φ2 are also interreduceable. In using this principle, we have the following constraints.(1)
Cond2 must be θ0-free; that is, it must be irrelevant to the initial condition.(2)
If the second rule is one of these listed in Table4 (or the inversion/duality version), then we require that the (designated) occurrences of φ2 in ψ1 must betemporally outermost; that is, φ2 does not appear in the scope of any temporal operators.(3)
Sinceη≈η trivially holds, we have the following special case of the composition principle:
(13)Cond⊳φ≈ψCond⊳η≈ηψφ,and call it the local application of (the above) CePRe rule.To explaint the reason why we need to impose the second constraint, just consider the following fact: we haveYφ≈⊥ according to (Y); yet this does not imply that FYφ≈F⊥ holds.


#### 3.2.4. The Decomposition Principle

The last principle, which could be corporately used inmodular model checking [14], is described as follows:
(14)Cond1⊳φ1≈M1ψ1Cond2⊳φ2≈M2ψ2Cond1&Cond2⊳φ1≈M1∥M2ψ1ψ2φ2,
where all constraints imposed to thecomposition principle are still required. M1∥M2 is thesynchronized composition of M1 and M2; that is, M1∥M2=〈V1∪V2,ρ1∧ρ2,θ0,1∧θ0,2,F1∪F2〉 if Mi=〈Vi,ρi,θ0,i,Fi〉.


### 3.3. Reduction Strategy

We show the usage of CePRe reduction rules by illustrating the reduction process of M⊨(θ1Uθ2)Uθ3; see Algorithm 1.(1)
We may first try with the rule (UU[1→3]) by inquiring the SAT-solver if ρ⊢θ1→θ3 holds.(2)
If the SAT-solver returns “unsatisfiable” with the inputρ∧θ1∧¬θ3, then it implies that the additional condition is stated, and we may replace the specification with θ2Uθ3.(3)
Otherwise, we will try with another reduction rule, such as (UU[2→3]).Algorithm 1:The “max-match” rule-selection strategy.
Input: The original specification φ.
Output: The reduced specification.
(1)let  Γ:=∅;/*  Γ memorizes the sub-formulae with infeasible condition */
(2)let  Δ:={ψ∈ (sub(φ)∖Γ) such that ψ matches some reduction rule(s)};
(3)foreach  ψ1,ψ2∈Δ s.t. ψ1≠ψ2  do
(4)if  ψ1∈  sub(ψ2 )  then
(5)Δ≔Δ∖{ψ1};/* that is, we only proceed “max” subformulae */
(6)end
(7)end
(8)if  Δ=∅  then
(9)return  φ;
(10)end
(11)foreach  ψ∈Δ  do
(12)let  Θ≔ the set of rules that can be applied to ψ;
(13)/* note that we have |Θ|≤5 for each  ψ  */
(14)while  Θ≠∅  do
(15)choose R≔(Cond⊳ψ≈η) in  Θ;
(16)if Cond is statedthen
(17)φ:=φηψ; /*  φηψ is obtained from φ by replacing ψ with η  */
(18)break;
(19)end
(20)Θ:=Θ∖{R};
(21)end
(22)Δ:=Δ∖{ψ};
(23)if  Θ=∅  then
(24)Γ:=Γ∪{ψ}; /*  ψ would be excluded in the next iteration */
(25)end
(26)end
(27)goto2;Compositional use of reduction rules may lead to a more aggressive reduction. For example,(1)
for the task of model checkingM⊨FOp, we may firstly change the goal as M⊨Fp∨Op, according to the rule (FO);(2)
now, the subformulaOp is a temporally outermost one; hence we may make a local application of (O), and then the goal becomes M⊨Fp∨p;(3)
finally, we may change the model checking problem intoM⊨Fp via the rule (Disj).In the real implementation, we perform a “max-match” rule-selection strategy, as depicted in Algorithm 1. Note that in this algorithm, only(1)
basic rules,(2)
rules obtained from the inversion principle or the duality principlecould be directly used (maybe in a local manner). This guarantees the finiteness for rule selection.In line 15, a rule having simpler condition always has the higher precedence to be chosen. Hence, a model-independent rule always has a higher priority than a model-dependent one.Lastly, we can see that the reduction can be accomplished withinO(|φ|) iterations.


## 3.1. The Basic Reduction Rules

In this section, we define some basic CePRe rules. First of all, we have some elementary reduction rules relating to model components, as depicted in Table 1. For the rules (Init), (Ind), and (Trans), the notation “⊢” occurring in the condition part stands for the “inferring” relation in propositional logic (ρ⊢θ if and only if ρ∧¬θ is unsatisfiable), and we here require that θ,θ1,θ2∈B(V).Table 1
Reduction rules about model components.
θ
0
⊢
θ
⊳
θ
≈
⊤ (Init)
ρ
⊢
θ
⊳
G
θ
≈
⊤ (Trans)
θ
∈
F
⊳
G
F
θ
≈
⊤ (Fair)
θ
0
⊢
θ; ρ⊢θ→θ′⊳Gθ≈⊤ (Ind)Subsequently, let us define a partial order “⊑” over unary temporal operators (and their combinations) as follows:
(6)F⊑GF⊑FG⊑GF⊑Xi⊑G(i≺ω)O⊑HO⊑OH⊑H,
where X0φ≜φ and Xi+1φ≜X(Xiφ).Assume thatPw,Ps∈{F,FG,GF,G,O,HO,OH,H}∪{Xi∣i≺ω} and Pw⊑Ps; then we have two model-indenpendent rules, as depicted in Table 2. Though these rules seem to be trivial, they are useful in doing combinational reductions (see the example given in Section 3.3).Table 2
Reduction rules of (Conj) and (Disj).
(
P
w
φ
∧
P
s
φ
)
≈
P
s
φ (Conj)
(
P
w
φ
∨
P
s
φ
)
≈
P
w
φ (Disj)Table3 provides some reduction rules that can be used to simplify nested temporal operators.Table 3
Reduction rules for formulae involving nested pure future operators.
F
(
φ
U
ψ
)
≈
F
ψ (FU)
φ
U
(
F
ψ
)
≈
F
ψ (UF)
F
F
φ
≈
F
φ (FF)
G
F
G
φ
≈
F
G
φ (GFG)Since we always stand at the starting point when doing model checking (i.e., the goal is to check ifπ,0⊨φ for each π∈L(M)), we can sometimes “erase” the outermost past operators, as depicted in Table 4.Table 4
Reduction rules for formulae involving (outermost) past operators.
Y
φ
≈
⊥ (Y)
O
φ
≈
φ (O)
φ
S
ψ
≈
φ (S)Table5 introduces a series of rules handling formulae involving adjacent past and future temporal operators.Table 5
Reduction rules for formulae involving adjacent past and future operators.
X
Y
φ
≈
φ (XY)
F
H
φ
≈
H
φ (FH)
F
O
φ
≈
F
φ
∨
O
φ (FO)
F
(
φ
S
ψ
)
≈
F
ψ
∨
φ
S
ψ (FS)We letθ1,θ2,… range over B(V) and let φ1,φ2,… be arbitrary LTL formulae, and then we have some model-dependent rules. The first group of such rules is listed in Table 6. Table 7 provides another set of model-dependent reduction rules, and these rules are mainly concerned with LTL formulae involving adjacent U-operators. Lastly, Table 8 provides some reduction rules that can be used to simplify formulae with mixed usage of U and R.Table 6
Reduction rules of (U) and (R).
ρ
⊢
θ
1
∨
θ
2
⊳
θ
1
U
θ
2
≈
F
θ
2 (U)
ρ
⊢
θ
2
→
θ
1
∨
θ
2
′
⊳
θ
1
R
θ
2
≈
θ
2 (R)Table 7
Reduction rules for formulae involving adjacentU operators.
ρ
⊢
θ
1
→
θ
2
⊳
θ
1
U
θ
2
≈
θ
2
(U[1→2])
ρ
⊢
θ
1
→
θ
3
⊳
(
θ
1
U
φ
2
)
U
θ
3
≈
φ
2
U
θ
3
(UU[1→3])
ρ
⊢
θ
2
→
θ
3
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
θ
3
∨
(
φ
1
U
θ
2
)
(UU[2→3])
ρ
⊢
θ
3
→
θ
2
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
(
φ
1
∨
θ
2
)
U
θ
3
(UU[3→2])
ρ
⊢
θ
2
→
θ
3
′
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
(
φ
1
∨
θ
2
)
U
θ
3
(UU[2→3′])
ρ
⊢
¬
θ
2
→
θ
3
⊳
(
φ
1
U
θ
2
)
U
θ
3
≈
F
θ
3
(UU[¬2→3])
ρ
⊢
θ
1
→
θ
2
⊳
θ
1
U
(
θ
2
U
φ
3
)
≈
θ
2
U
φ
3
(UU[1→2])
ρ
⊢
θ
1
→
θ
3
⊳
θ
1
U
(
φ
2
U
θ
3
)
≈
φ
2
U
θ
3
(UU[1→3])
ρ
⊢
θ
2
→
θ
1
⊳
θ
1
U
(
θ
2
U
φ
3
)
≈
θ
1
U
φ
3
(UU[2→1])Table 8
Reduction rules for formulae involving adjacentU and R operators.
ρ
⊢
θ
1
→
θ
3
⊳
(
θ
1
R
φ
2
)
U
θ
3
≈
(
(
θ
1
R
φ
2
)
∨
θ
3
)
∧
F
θ
3
(UR[1→3])
ρ
⊢
¬
θ
1
→
θ
3
⊳
(
θ
1
R
φ
2
)
U
θ
3
≈
φ
2
U
θ
3
(UR[¬1→3])
ρ
⊢
θ
1
→
θ
3
⊳
θ
1
U
(
φ
2
R
θ
3
)
≈
φ
2
R
θ
3
(UR[1→3])


## 3.2. Principles for Rule Generation

Actually, we may acquire more CePRe rules by applying someprinciples to the existing rules. In this section, we introduce four major principles in our framework.


### 3.2.1. The Inversion Principle

We say that the temporal opertors “U and S,” “R and T,” “G and H,” and “F and O” are pairwiseinverse operators (The inverse operator of X may be Z or Y, which is judged from the context. Fortunately, in this paper, we need not consider this case). Then, for CePRe rules list in Table 3 and Tables 6–8, we may apply the following principle:
(7)ρ⊢θ⊳φ≈ψρ⊢θ~⊳inv(φ)≈inv(ψ),
namely,Inversion Principle. In detail:(i)
ifθ∈B(V) then θ~=θ; if θ∈B(V∪V'), then θ~ is obtained from θ by switching the primed and unprimed propositions;(ii)
inv(φ) and inv(ψ) are obtained from φ and ψ by swithing the temporal operators with their inverse operators, respectively.For example, one can apply this principle to(U) and (R), and then the following two rules
(8)ρ⊢θ1∨θ2⊳θ1Sθ2≈Oθ2(S)ρ⊢θ2′⟶θ1′∨θ2⊳θ1Tθ2≈θ2(T)
are immediately obtained.


### 3.2.2. The Duality Principle

We say that “⊤ and ⊥,” “∧ and ∨,” “F and G,” “O and H,” “Y and Z,” “X and X itself,” “U and R,” and “T and S” are pairwise thedual operators. Then, theduality principle could be described as follows:
(9)Cond⊳φ≈ψCond-⊳dual(φ)≈dual(ψ).
We require that the condition “Cond” should be either trivial (in this case, the rule is a model-independent one) or of the form ρ⊢θ1→θ2, and in the latter case we have Cond¯=ρ⊢θ2→θ1. The formulae dual(φ) and dual(ψ) are obtained from φ and ψ by switching the operators with their dual.For example, apply the duality principle to the rules(FU), (UF), (FF), and (GFG), one may get the following new rules:
(10)G(φRψ)≈Gψ(GR),φR(Gψ)≈Gψ(RG),GGφ≈Gφ(GG),FGFφ≈GFφ(FGF).Note that when applying the duality principle to model-dependent rules, besides switching the operators, we also need to exchange the antecedent and subsequent on the righthand of⊢ in the condition part, in the case that the condition is of the form ρ⊢θ1→θ2. As an example, we may obtain the reduction rule
(11)ρ⊢θ3⟶θ2⊳(φ1Rθ2)Rθ3≈θ3∧(φ1Rθ2)(RR[3⟶2]),
by applying the duality principle to (UU[2→3]).


### 3.2.3. The Composition Principle

Thecomposition principle can be formally described as follows:
(12)Cond1⊳φ1≈ψ1Cond2⊳φ2≈ψ2Cond1&Cond2⊳φ1≈ψ1ψ2φ2;
that is, if φi and ψi are interreduceable under the conditin Condi (i=1,2), then φ1 and ψ1ψ2φ2 are also interreduceable. In using this principle, we have the following constraints.(1)
Cond2 must be θ0-free; that is, it must be irrelevant to the initial condition.(2)
If the second rule is one of these listed in Table4 (or the inversion/duality version), then we require that the (designated) occurrences of φ2 in ψ1 must betemporally outermost; that is, φ2 does not appear in the scope of any temporal operators.(3)
Sinceη≈η trivially holds, we have the following special case of the composition principle:
(13)Cond⊳φ≈ψCond⊳η≈ηψφ,and call it the local application of (the above) CePRe rule.To explaint the reason why we need to impose the second constraint, just consider the following fact: we haveYφ≈⊥ according to (Y); yet this does not imply that FYφ≈F⊥ holds.


### 3.2.4. The Decomposition Principle

The last principle, which could be corporately used inmodular model checking [14], is described as follows:
(14)Cond1⊳φ1≈M1ψ1Cond2⊳φ2≈M2ψ2Cond1&Cond2⊳φ1≈M1∥M2ψ1ψ2φ2,
where all constraints imposed to thecomposition principle are still required. M1∥M2 is thesynchronized composition of M1 and M2; that is, M1∥M2=〈V1∪V2,ρ1∧ρ2,θ0,1∧θ0,2,F1∪F2〉 if Mi=〈Vi,ρi,θ0,i,Fi〉.


## 3.2.1. The Inversion Principle

We say that the temporal opertors “U and S,” “R and T,” “G and H,” and “F and O” are pairwiseinverse operators (The inverse operator of X may be Z or Y, which is judged from the context. Fortunately, in this paper, we need not consider this case). Then, for CePRe rules list in Table 3 and Tables 6–8, we may apply the following principle:
(7)ρ⊢θ⊳φ≈ψρ⊢θ~⊳inv(φ)≈inv(ψ),
namely,Inversion Principle. In detail:(i)
ifθ∈B(V) then θ~=θ; if θ∈B(V∪V'), then θ~ is obtained from θ by switching the primed and unprimed propositions;(ii)
inv(φ) and inv(ψ) are obtained from φ and ψ by swithing the temporal operators with their inverse operators, respectively.For example, one can apply this principle to(U) and (R), and then the following two rules
(8)ρ⊢θ1∨θ2⊳θ1Sθ2≈Oθ2(S)ρ⊢θ2′⟶θ1′∨θ2⊳θ1Tθ2≈θ2(T)
are immediately obtained.


## 3.2.2. The Duality Principle

We say that “⊤ and ⊥,” “∧ and ∨,” “F and G,” “O and H,” “Y and Z,” “X and X itself,” “U and R,” and “T and S” are pairwise thedual operators. Then, theduality principle could be described as follows:
(9)Cond⊳φ≈ψCond-⊳dual(φ)≈dual(ψ).
We require that the condition “Cond” should be either trivial (in this case, the rule is a model-independent one) or of the form ρ⊢θ1→θ2, and in the latter case we have Cond¯=ρ⊢θ2→θ1. The formulae dual(φ) and dual(ψ) are obtained from φ and ψ by switching the operators with their dual.For example, apply the duality principle to the rules(FU), (UF), (FF), and (GFG), one may get the following new rules:
(10)G(φRψ)≈Gψ(GR),φR(Gψ)≈Gψ(RG),GGφ≈Gφ(GG),FGFφ≈GFφ(FGF).Note that when applying the duality principle to model-dependent rules, besides switching the operators, we also need to exchange the antecedent and subsequent on the righthand of⊢ in the condition part, in the case that the condition is of the form ρ⊢θ1→θ2. As an example, we may obtain the reduction rule
(11)ρ⊢θ3⟶θ2⊳(φ1Rθ2)Rθ3≈θ3∧(φ1Rθ2)(RR[3⟶2]),
by applying the duality principle to (UU[2→3]).


## 3.2.3. The Composition Principle

Thecomposition principle can be formally described as follows:
(12)Cond1⊳φ1≈ψ1Cond2⊳φ2≈ψ2Cond1&Cond2⊳φ1≈ψ1ψ2φ2;
that is, if φi and ψi are interreduceable under the conditin Condi (i=1,2), then φ1 and ψ1ψ2φ2 are also interreduceable. In using this principle, we have the following constraints.(1)
Cond2 must be θ0-free; that is, it must be irrelevant to the initial condition.(2)
If the second rule is one of these listed in Table4 (or the inversion/duality version), then we require that the (designated) occurrences of φ2 in ψ1 must betemporally outermost; that is, φ2 does not appear in the scope of any temporal operators.(3)
Sinceη≈η trivially holds, we have the following special case of the composition principle:
(13)Cond⊳φ≈ψCond⊳η≈ηψφ,and call it the local application of (the above) CePRe rule.To explaint the reason why we need to impose the second constraint, just consider the following fact: we haveYφ≈⊥ according to (Y); yet this does not imply that FYφ≈F⊥ holds.


## 3.2.4. The Decomposition Principle

The last principle, which could be corporately used inmodular model checking [14], is described as follows:
(14)Cond1⊳φ1≈M1ψ1Cond2⊳φ2≈M2ψ2Cond1&Cond2⊳φ1≈M1∥M2ψ1ψ2φ2,
where all constraints imposed to thecomposition principle are still required. M1∥M2 is thesynchronized composition of M1 and M2; that is, M1∥M2=〈V1∪V2,ρ1∧ρ2,θ0,1∧θ0,2,F1∪F2〉 if Mi=〈Vi,ρi,θ0,i,Fi〉.


## 3.3. Reduction Strategy

We show the usage of CePRe reduction rules by illustrating the reduction process of M⊨(θ1Uθ2)Uθ3; see Algorithm 1.(1)
We may first try with the rule (UU[1→3]) by inquiring the SAT-solver if ρ⊢θ1→θ3 holds.(2)
If the SAT-solver returns “unsatisfiable” with the inputρ∧θ1∧¬θ3, then it implies that the additional condition is stated, and we may replace the specification with θ2Uθ3.(3)
Otherwise, we will try with another reduction rule, such as (UU[2→3]).Algorithm 1:The “max-match” rule-selection strategy.
Input: The original specification φ.
Output: The reduced specification.
(1)let  Γ:=∅;/*  Γ memorizes the sub-formulae with infeasible condition */
(2)let  Δ:={ψ∈ (sub(φ)∖Γ) such that ψ matches some reduction rule(s)};
(3)foreach  ψ1,ψ2∈Δ s.t. ψ1≠ψ2  do
(4)if  ψ1∈  sub(ψ2 )  then
(5)Δ≔Δ∖{ψ1};/* that is, we only proceed “max” subformulae */
(6)end
(7)end
(8)if  Δ=∅  then
(9)return  φ;
(10)end
(11)foreach  ψ∈Δ  do
(12)let  Θ≔ the set of rules that can be applied to ψ;
(13)/* note that we have |Θ|≤5 for each  ψ  */
(14)while  Θ≠∅  do
(15)choose R≔(Cond⊳ψ≈η) in  Θ;
(16)if Cond is statedthen
(17)φ:=φηψ; /*  φηψ is obtained from φ by replacing ψ with η  */
(18)break;
(19)end
(20)Θ:=Θ∖{R};
(21)end
(22)Δ:=Δ∖{ψ};
(23)if  Θ=∅  then
(24)Γ:=Γ∪{ψ}; /*  ψ would be excluded in the next iteration */
(25)end
(26)end
(27)goto2;Compositional use of reduction rules may lead to a more aggressive reduction. For example,(1)
for the task of model checkingM⊨FOp, we may firstly change the goal as M⊨Fp∨Op, according to the rule (FO);(2)
now, the subformulaOp is a temporally outermost one; hence we may make a local application of (O), and then the goal becomes M⊨Fp∨p;(3)
finally, we may change the model checking problem intoM⊨Fp via the rule (Disj).In the real implementation, we perform a “max-match” rule-selection strategy, as depicted in Algorithm 1. Note that in this algorithm, only(1)
basic rules,(2)
rules obtained from the inversion principle or the duality principlecould be directly used (maybe in a local manner). This guarantees the finiteness for rule selection.In line 15, a rule having simpler condition always has the higher precedence to be chosen. Hence, a model-independent rule always has a higher priority than a model-dependent one.Lastly, we can see that the reduction can be accomplished withinO(|φ|) iterations.


## 4. Performance Analysis of CePRe

We now try to answer the question “why we can gain a better performance during verification if CePRe is conducted first.” To give a rigorous explanation, we briefly revisit the implementation of some symbolic model checking algorithms, and we are mainly concerned about the following techniques:(1)
the BDD-based model checking technique,(2)
the bounded model checking technique (BMC), for both syntactic encoding and semantic encoding approaches,(3)
the property directed reachability (alternatively, IC3) algorithm.


### 4.1. Analysis on BDD-Based Model Checking

The core procedure of BDD-based LTL symbolic model checking algorithm is to construct atableau for the (negated) property. In the following, we refer the tableau of ¬φ as T¬φ, and we would give an analysis on its major components affecting the cost of model checking.State Space. The state space of T¬φ consists of subsets of el(φ), and the set el(φ) can be inductively computed as follows:(i)
el(⊤)=el(⊥)=∅;(ii)
el(p)={p} if p∈P;(iii)
el(φ1→φ2)=el(φ1)∪el(φ2);(iv)
el(Xψ)={Xψ}∪el(ψ), and el(Yψ)={Yψ}∪el(ψ);(v)
el(φ1Uφ2)=el(φ1)∪el(φ2)∪{X(φ1Uφ2)} and el(φ1Sφ2)=el(φ1)∪el(φ2)∪{Y(φ1Sφ2)}. We can see from the definition that el(φ)=el(¬φ) holds. With symbolic representation, each formula ψ∈el(φ) corresponds to a proposition in building the tableau. Moreover, if ψ∈P, then no new proposition needs to be introduced (since it has already been introduced in building the symbolic representation of M); otherwise, a fresh proposition pψ is required. Hence the total number of newly introduced propositions equals |el(φ)∖P|. From an induction over formula's structure, we have the following claim.Proposition 2.
|
e
l
(
φ
)
∖
P
| equals the number of temporal operators in φ.Transitions. The transition relation of T¬φ is a conjunction of a set of constraints, and each constraint is either of the form pXψ↔(σ(ψ))′ or pYη′↔σ(η), where Xψ,Yη∈el(φ), and the function σ can be inductively defined as follows:(i)
σ(⊥)=⊥ and σ(⊤)=⊤;(ii)
σ(p)=p for each p∈P;(iii)
σ(ψ1→ψ2)=σ(ψ1)→σ(ψ2);(iv)
σ(Xψ1)=pXψ1 and σ(Yψ2)=pYψ2;(v)
σ(ψ1Uψ2)=σ(ψ2)∨σ(ψ1)∧pX(ψ1Uψ2) and σ(ψ1Sψ2)=σ(ψ2)∨σ(ψ1)∧pY(ψ1Uψ2). According to the definition of el, we can see that each ψ∈sub(φ) rooted at a future (resp., past) temporal operator exactly produces one formula Xη (resp., Yη) in el(φ), and hence a new proposition pXη (resp., pYη) would be introduced. Subsequently, each such pXη (resp., pYη) adds exactly one constraint to the transition relation. Hence, we have the following claim.Proposition 3.
The number of constraints in the transition relation ofT¬φ equals the number of temporal operators occurring in φ (alternatively, |el(φ)∖P|).Fairness Constraints. According to the tableau construction, each ψ∈subU(¬φ) would impose a fairness constraint to T¬φ. Hence, the number of fairness constraints equals |subU(¬φ)|.With a case-by-case checking, we can show the following theorem.Theorem 4.
Let “Cond⊳φ≈ψ” be a reduction rule; then we have |el(ψ)∖P|≤|el(φ)∖P| and |subU(ψ)|≤|subU(¬φ)|.


### 4.2. Analysis on Bounded Model Checking

In contrast, the cost of BMC is quite sensitive to the encoding approach. In a broad sense, we can categorize the encoding approaches into two fashions.Syntactic Encodings. Such kind of encodings are inductively produced w.r.t. the formula's structure. The very original one is presented in [7], and this is improved in [15] by observing some properties of that encoding. In [16, 17], a linear incremental syntactic encoding is suggested, and see [18] for the translation for ECTL*.Semantic Encodings. In [19], an alternative BMC technique is provided: it mimics the tableau-based model checking process, but it expresses the fair-path detection upon the product model with Boolean formula. (In [20], a “fixpoint”-based encoding is proposed, and it can also be subsumed to semantic encodings.)For the semantic encodings, the reason that we can benefit from CePRe is exactly the same as that for BDD-based approach. Because, the encoding is a conjunction of a k-step unrolling of M and a k-step unrolling of T¬φ (an unrolling is either a partial derived linear structure or one ending with a lasso). The former is usually in a fixed pattern, and for the latter, we need k×|el(φ)∖P| new propositions, and the sizes of Boolean formulae w.r.t the transition and fairness constraints (note that the part w.r.t. fairness constraints can be linearized) are, respectively, O(k×|el(φ)∖P|) and O(k2×|subU(¬φ)|).For a syntactic BMC encoding, one needs to generate a Boolean formula of the formEMk∧E¬φk, where EMk is the unrolling of M with k steps, and E¬φk describes that such k-step unrolling would cause a violation of φ. In general, EMk is almost the same in all kinds of syntactic encodings, and the key factor affecting the cost lies in E¬φk.Given a subformulaψ of φ, if we use ||Eψk|| to denote the maximum length of the Boolean formula describing that ψ is initially satisfied upon a k-step unrolling, then it can be inductively computed as follows:(i)
||E⊥k||=||EΤk||=0; (this is just for the case when ⊥ or ⊤ appears as a subformula in the specification and hence can be optimized; otherwise, we have ||E⊥k||=||E⊤k||=1);(ii)
||Epk||=1 for each p∈P;(iii)
||Eφ1→φ2k||=||Eφ1k||+||Eφ2k||+1;(iv)
||EXψk||=||EYψk||=||Eψk||;(v)
||Eφ1Uφ2k||=||Eφ1Sφ2k||=L(k)×||Eφ1k||+k×||Eφ2k||. (Note that this case does not imply that further blowup would be caused with deeper nesting of temporal operators. For example, in [17], by introducing fresh propositions and reusing, it still leads to a linear encoding for the whole formula.) Here, L(k) is some polynomial about k, related to the encoding approach. For example, with the technique proposed in [7, 15], we have L(k)∈O(k2), whereas L(k)∈O(k) in [16, 17]. This partly explains the reason that we tend to change temporal nestifications with Boolean combinations, as done in (UU[3→2]) and so forth.Another feature affecting the cost is the scale of propositions required for the encoding. If we denote byvark(φ) the set of additional propositions which only takes part in the encoding of E¬φk, then we have the following conclusions.(i)
For the techniques proposed in [7, 15], we have vark(φ)=0. i.o.w.; all propositions required in encoding E¬kφ can be shared with those for EMk.(ii)
In term of the encoding presented in [17], we need to add O(k) new propositions to vark(φ) for each U-subformula and for each S-subformula.Theorem 5.
Let “Cond⊳φ≈ψ” be a reduction rule; then we have ||Eψk||≤||Eφk|| and |vark(ψ)|≤|vark(φ)| in syntactic encodings.


### 4.3. Analysis on Property Directed Reachability Algorithm

Property directed reachability (PDR or IC3) is probably the most significant breakthrough in SAT based model checking. The aim of PDR is to show that the system issafe w.r.t. the property θ; that is, each reachable state satisfies the boolean constraint θ.The process of PDR retains a sequenceΓ0,…,Γk of clause sets fulfilling the following.(1)
Γ0={θ0}; and for each i⩽k we have(2)
⊢∧Γi→∧Γi+1;(3)
⊢∧Γi∧ρ→∧Γi+1′;(4)
⊢∧Γi→θ. This process stops and reports an affirmative answer if there exists some i>0 having Γi=Γi-1; and it reports failure when some reachable “unsafe” state is detected. Therefore, it intends to find a (intermediate) reachable-closure enclosed (orinductive set) with θ, as described in Algorithm 2.Algorithm 2:Framework of the PDR algorithm.
Input: The components V, ρ, θ0 of the model M; a safety property θ.
Output: The affirmative answer if M is safe w.r.t. θ; otherwise, a counterexample witnessing that ¬θ is reachable.
(1) let  k:=0;
(2) let  Γ0={θ0};
(3) let  Q:=∅; /* Q is a priority queue */
(4) repeat
(5) while there exists  U⊆V s.t. U⊩Γk∧¬θ  do
(6)   add (U,k) to the head of  Q;
(7)   if  strengthen({Γi}i⩽k,Q,V) fails then
(8)     return counterexample extracted from Q;
(9)   end
(10)propagate({Γi}i⩽k);
(11)if there exists some j≤k s.t.  Γj=Γ(j-1)  then
(12)return “M is safe from θ”;
(13)end
(14)let  Γk+1:=∅;
(15)k:=k+1;
(16)end
(17)until 1≠1;This algorithm employees two important subroutines—thestrengthen process (Line 7) and thepropagate process (Line 10):(i)
The processstrengthen aims to disprove the reachability of the point U which violates θ. If it succeeds, some new constraints would be added to some specific clause sets; if this process fails, then it implies that we have a feasible path which leads to an “unsafe” state. In [21], an effectivestrengthen algorithm is provided, and it results in a linear complexity in time w.r.t. the size of variable set.(ii)
The processpropagate is used to “compact” the clause sets and to accelerate the termination. Its purpose is to “push out” the clauses in a set as possible as they can. Suppose that there is a clause η∈Γi, in the case that ⊢∧Γi∧ρ→η′ holds; since we have ⊢∧Γi∧ρ→∧Γi+1′, it implies that ⊢∧Γi∧ρ→∧Γi+1′∧η′ also holds. In such situation, the clause η could be definitely propagated to Γi+1.Since the PDR algorithm could not directly handle general temporal properties, we need to first translate the LTL model checking problem to PDR solving, via the following steps.(1)
Build the tableauT¬φ from the LTL formula φ, as describled in Section 4.1.(2)
Thus, the problem is boiled down to a fair-circle detection problem on the production ofM and T¬φ.(3)
This problem could be further translated ton+1 PRD-solving problems, where n is the number of fairness constraints in the production. Interested readers may refer to [22] for the translation details.It could be seen that the features affecting the overhead of PDR-solving boiled from LTL input are the following:(1)
the scale of product system, which is determined by the number of variables in the tableau and model,(2)
the size (or number of clauses) of the transition relation, which is a summation of these of the tableau and the model,(3)
the number of fairness constrains in the product, which is also the summation of constraint numbers of the model and the tableau.For two LTL formulaeφ and ψ such that φ≈Mψ, since the model is the same, the “variable number,” “number of clauses in the transition relation,” and “the number of fairness contraints” are determined by the tableaux T¬φ and T¬ψ. Precisely like the analysis we have done in Section 4.1, we have the same conclusions shown in Propositions 2 and 3 and Theorem 4, and these would explain why we can also benefit from CePRe when using PDR as underlying checking approach.


## 4.1. Analysis on BDD-Based Model Checking

The core procedure of BDD-based LTL symbolic model checking algorithm is to construct atableau for the (negated) property. In the following, we refer the tableau of ¬φ as T¬φ, and we would give an analysis on its major components affecting the cost of model checking.State Space. The state space of T¬φ consists of subsets of el(φ), and the set el(φ) can be inductively computed as follows:(i)
el(⊤)=el(⊥)=∅;(ii)
el(p)={p} if p∈P;(iii)
el(φ1→φ2)=el(φ1)∪el(φ2);(iv)
el(Xψ)={Xψ}∪el(ψ), and el(Yψ)={Yψ}∪el(ψ);(v)
el(φ1Uφ2)=el(φ1)∪el(φ2)∪{X(φ1Uφ2)} and el(φ1Sφ2)=el(φ1)∪el(φ2)∪{Y(φ1Sφ2)}. We can see from the definition that el(φ)=el(¬φ) holds. With symbolic representation, each formula ψ∈el(φ) corresponds to a proposition in building the tableau. Moreover, if ψ∈P, then no new proposition needs to be introduced (since it has already been introduced in building the symbolic representation of M); otherwise, a fresh proposition pψ is required. Hence the total number of newly introduced propositions equals |el(φ)∖P|. From an induction over formula's structure, we have the following claim.Proposition 2.
|
e
l
(
φ
)
∖
P
| equals the number of temporal operators in φ.Transitions. The transition relation of T¬φ is a conjunction of a set of constraints, and each constraint is either of the form pXψ↔(σ(ψ))′ or pYη′↔σ(η), where Xψ,Yη∈el(φ), and the function σ can be inductively defined as follows:(i)
σ(⊥)=⊥ and σ(⊤)=⊤;(ii)
σ(p)=p for each p∈P;(iii)
σ(ψ1→ψ2)=σ(ψ1)→σ(ψ2);(iv)
σ(Xψ1)=pXψ1 and σ(Yψ2)=pYψ2;(v)
σ(ψ1Uψ2)=σ(ψ2)∨σ(ψ1)∧pX(ψ1Uψ2) and σ(ψ1Sψ2)=σ(ψ2)∨σ(ψ1)∧pY(ψ1Uψ2). According to the definition of el, we can see that each ψ∈sub(φ) rooted at a future (resp., past) temporal operator exactly produces one formula Xη (resp., Yη) in el(φ), and hence a new proposition pXη (resp., pYη) would be introduced. Subsequently, each such pXη (resp., pYη) adds exactly one constraint to the transition relation. Hence, we have the following claim.Proposition 3.
The number of constraints in the transition relation ofT¬φ equals the number of temporal operators occurring in φ (alternatively, |el(φ)∖P|).Fairness Constraints. According to the tableau construction, each ψ∈subU(¬φ) would impose a fairness constraint to T¬φ. Hence, the number of fairness constraints equals |subU(¬φ)|.With a case-by-case checking, we can show the following theorem.Theorem 4.
Let “Cond⊳φ≈ψ” be a reduction rule; then we have |el(ψ)∖P|≤|el(φ)∖P| and |subU(ψ)|≤|subU(¬φ)|.


## 4.2. Analysis on Bounded Model Checking

In contrast, the cost of BMC is quite sensitive to the encoding approach. In a broad sense, we can categorize the encoding approaches into two fashions.Syntactic Encodings. Such kind of encodings are inductively produced w.r.t. the formula's structure. The very original one is presented in [7], and this is improved in [15] by observing some properties of that encoding. In [16, 17], a linear incremental syntactic encoding is suggested, and see [18] for the translation for ECTL*.Semantic Encodings. In [19], an alternative BMC technique is provided: it mimics the tableau-based model checking process, but it expresses the fair-path detection upon the product model with Boolean formula. (In [20], a “fixpoint”-based encoding is proposed, and it can also be subsumed to semantic encodings.)For the semantic encodings, the reason that we can benefit from CePRe is exactly the same as that for BDD-based approach. Because, the encoding is a conjunction of a k-step unrolling of M and a k-step unrolling of T¬φ (an unrolling is either a partial derived linear structure or one ending with a lasso). The former is usually in a fixed pattern, and for the latter, we need k×|el(φ)∖P| new propositions, and the sizes of Boolean formulae w.r.t the transition and fairness constraints (note that the part w.r.t. fairness constraints can be linearized) are, respectively, O(k×|el(φ)∖P|) and O(k2×|subU(¬φ)|).For a syntactic BMC encoding, one needs to generate a Boolean formula of the formEMk∧E¬φk, where EMk is the unrolling of M with k steps, and E¬φk describes that such k-step unrolling would cause a violation of φ. In general, EMk is almost the same in all kinds of syntactic encodings, and the key factor affecting the cost lies in E¬φk.Given a subformulaψ of φ, if we use ||Eψk|| to denote the maximum length of the Boolean formula describing that ψ is initially satisfied upon a k-step unrolling, then it can be inductively computed as follows:(i)
||E⊥k||=||EΤk||=0; (this is just for the case when ⊥ or ⊤ appears as a subformula in the specification and hence can be optimized; otherwise, we have ||E⊥k||=||E⊤k||=1);(ii)
||Epk||=1 for each p∈P;(iii)
||Eφ1→φ2k||=||Eφ1k||+||Eφ2k||+1;(iv)
||EXψk||=||EYψk||=||Eψk||;(v)
||Eφ1Uφ2k||=||Eφ1Sφ2k||=L(k)×||Eφ1k||+k×||Eφ2k||. (Note that this case does not imply that further blowup would be caused with deeper nesting of temporal operators. For example, in [17], by introducing fresh propositions and reusing, it still leads to a linear encoding for the whole formula.) Here, L(k) is some polynomial about k, related to the encoding approach. For example, with the technique proposed in [7, 15], we have L(k)∈O(k2), whereas L(k)∈O(k) in [16, 17]. This partly explains the reason that we tend to change temporal nestifications with Boolean combinations, as done in (UU[3→2]) and so forth.Another feature affecting the cost is the scale of propositions required for the encoding. If we denote byvark(φ) the set of additional propositions which only takes part in the encoding of E¬φk, then we have the following conclusions.(i)
For the techniques proposed in [7, 15], we have vark(φ)=0. i.o.w.; all propositions required in encoding E¬kφ can be shared with those for EMk.(ii)
In term of the encoding presented in [17], we need to add O(k) new propositions to vark(φ) for each U-subformula and for each S-subformula.Theorem 5.
Let “Cond⊳φ≈ψ” be a reduction rule; then we have ||Eψk||≤||Eφk|| and |vark(ψ)|≤|vark(φ)| in syntactic encodings.


## 4.3. Analysis on Property Directed Reachability Algorithm

Property directed reachability (PDR or IC3) is probably the most significant breakthrough in SAT based model checking. The aim of PDR is to show that the system issafe w.r.t. the property θ; that is, each reachable state satisfies the boolean constraint θ.The process of PDR retains a sequenceΓ0,…,Γk of clause sets fulfilling the following.(1)
Γ0={θ0}; and for each i⩽k we have(2)
⊢∧Γi→∧Γi+1;(3)
⊢∧Γi∧ρ→∧Γi+1′;(4)
⊢∧Γi→θ. This process stops and reports an affirmative answer if there exists some i>0 having Γi=Γi-1; and it reports failure when some reachable “unsafe” state is detected. Therefore, it intends to find a (intermediate) reachable-closure enclosed (orinductive set) with θ, as described in Algorithm 2.Algorithm 2:Framework of the PDR algorithm.
Input: The components V, ρ, θ0 of the model M; a safety property θ.
Output: The affirmative answer if M is safe w.r.t. θ; otherwise, a counterexample witnessing that ¬θ is reachable.
(1) let  k:=0;
(2) let  Γ0={θ0};
(3) let  Q:=∅; /* Q is a priority queue */
(4) repeat
(5) while there exists  U⊆V s.t. U⊩Γk∧¬θ  do
(6)   add (U,k) to the head of  Q;
(7)   if  strengthen({Γi}i⩽k,Q,V) fails then
(8)     return counterexample extracted from Q;
(9)   end
(10)propagate({Γi}i⩽k);
(11)if there exists some j≤k s.t.  Γj=Γ(j-1)  then
(12)return “M is safe from θ”;
(13)end
(14)let  Γk+1:=∅;
(15)k:=k+1;
(16)end
(17)until 1≠1;This algorithm employees two important subroutines—thestrengthen process (Line 7) and thepropagate process (Line 10):(i)
The processstrengthen aims to disprove the reachability of the point U which violates θ. If it succeeds, some new constraints would be added to some specific clause sets; if this process fails, then it implies that we have a feasible path which leads to an “unsafe” state. In [21], an effectivestrengthen algorithm is provided, and it results in a linear complexity in time w.r.t. the size of variable set.(ii)
The processpropagate is used to “compact” the clause sets and to accelerate the termination. Its purpose is to “push out” the clauses in a set as possible as they can. Suppose that there is a clause η∈Γi, in the case that ⊢∧Γi∧ρ→η′ holds; since we have ⊢∧Γi∧ρ→∧Γi+1′, it implies that ⊢∧Γi∧ρ→∧Γi+1′∧η′ also holds. In such situation, the clause η could be definitely propagated to Γi+1.Since the PDR algorithm could not directly handle general temporal properties, we need to first translate the LTL model checking problem to PDR solving, via the following steps.(1)
Build the tableauT¬φ from the LTL formula φ, as describled in Section 4.1.(2)
Thus, the problem is boiled down to a fair-circle detection problem on the production ofM and T¬φ.(3)
This problem could be further translated ton+1 PRD-solving problems, where n is the number of fairness constraints in the production. Interested readers may refer to [22] for the translation details.It could be seen that the features affecting the overhead of PDR-solving boiled from LTL input are the following:(1)
the scale of product system, which is determined by the number of variables in the tableau and model,(2)
the size (or number of clauses) of the transition relation, which is a summation of these of the tableau and the model,(3)
the number of fairness constrains in the product, which is also the summation of constraint numbers of the model and the tableau.For two LTL formulaeφ and ψ such that φ≈Mψ, since the model is the same, the “variable number,” “number of clauses in the transition relation,” and “the number of fairness contraints” are determined by the tableaux T¬φ and T¬ψ. Precisely like the analysis we have done in Section 4.1, we have the same conclusions shown in Propositions 2 and 3 and Theorem 4, and these would explain why we can also benefit from CePRe when using PDR as underlying checking approach.


## 5. Experimental Results

We have implemented CePRe as an upfront option in NuSMV (the tool is available on http://sourceforge.net/projects/nusmvwithcepre/), and we have also conducted experiments upon both industrial benchmarks and randomly generated cases in terms of BDD-based model checking, bounded model checking, and PDR-based model checking.The BMC encoding approach we adopt here is that proposed in [15], which is the current BMC implementation of NuSMV. Since PDR verifiers could not directly take SMV models and/or LTL formulae as input, and they use AIGs (the And-Inverter Graphs) as standard input format, we first use the SMVtoAIG tool [23] to convert SMV-scripts into AIGs and then useiimc [24] to perform the PDR-based verification.We conduct the experiments under such platform: CPU-Intel Core Duo2 E4500 2.2 GHz, Mem-2 G Bytes, OS-Ubuntu 10.04 Linux, Cudd-v2.4.1.1, Zchaff-v2007.3.12.


### 5.1. Experiments upon Industrial Benchmarks

The benchmarks we choose in this paper are suggested in [4], and most of them come from real hardware verification.Table9 provides the experimental results for BDD-based LTL symbolic model checking. The field time is the executing time totally elapsed, and the field R.S. refers to the number of reachable states. For the experiments “with CePRe,” both the overheads of time and space are the summations of preprocessing and model checking. For Table 9, we have the following remarks.(1)
8 out of 16 specifications could be reduced with CePRe (and these specifications are marked with †).(2)
For the specifications that can be reduced, considerable improvements are made during verification. For example, for the specificationPit.g.ltl, with CePRe, the number of BDD nodes is decreased to 12.5% of that without using CePRe.(3)
When a specification cannot be reduced with CePRe, it spends a very low extra overhead for doing preprocessings.(4)
Something noteworthy we do not provide here is that in the case that a violated LTL specification can be reduced, the newly generated counterexample is usually shorter than that of before. Among 8 specifications that can be reduced, counterexample lengths ofPti.nuv.ltl,Pit.g.ltl,P0.ltl, andSeq.ltl are, respectively, shortened to 15, 10, and 194, opposing to the original values 16, 12, and 217. Meanwhile, counterexample lengths of others are kept unchanged.Table 9
Comparative results of BDD-based MC with/withoutCePRe.
Model
Spec.
WithoutCePRe
WithCePRe
BDD--Nodes
R.S.
Time(sec.)
BDD--Nodes
R.S.
Time(sec.)
srg5
Ptimo.ltl†
7946
720
0.024
2751
720
0.016
Pti.gnv.ltl†
29704
11460
0.058
5712
2880
0.012
Pti.g.ltl†
64749
130048
0.048
8119
32768
0.016
abp4
P2false.ltl
99577
559104
0.200
99625
559104
0.202
P2true.ltl†
61209
904384
0.066
56494
419296
0.064
Pold.ltl
52301
353536
0.060
52349
353536
0.064
Ptimo.ltl
78098
219616
0.080
78146
219616
0.088
Pti.g.ltl
8385
200704
0.060
8433
200704
0.062
dme3
P0.ltl†
889773
35964
5.756
527983
26316
5.096
P1.ltl
455148
8775
0.460
409432
5505
0.374
dme5
Mdl.ltl†
793942
8.64316
e
+
06
167.346
814494
3.2097
e
+
06
114.599
Wat.ltl†
412867
1.79217
e
+
07
302.005
967033
1.12567
e
+
07
286.850
Ptimo.neg
508036
1.26202
e
+
06
3.260
508081
1.26202
e
+
06
3.280
msi_w-trans
Sched.ltl
2275558
7.31055
e
+
07
6.612
2275655
7.31055
e
+
07
6.632
Safety.ltl
1213308
3.6528
e
+
07
7.568
1213460
3.6528
e
+
07
7.644
Seq.ltl†
1921973
3.5946
e
+
07
93.570
1702585
1.7973
e
+
07
94.085Table10 gives the experimental results for BMC-based model checking, and we here give some comments on that.(1)
With NuSMV, we need to preset a max-bound when doing bounded model checking. The column max-bound gives such values—a “star mark” means that this bound does not reach the completeness threshold. The field N.O.C. designates the number of clauses generated during model checking.(2)
From Table10, we can see that without CePRe the specificationPti.gnv.ltl generates 2101 clauses when the verification stops; in contrast, it only produces 299 clauses if CePRe is switched on.(3)
Another comparison is forP0.ltl upondme3: If we do not do any reduction, the SAT solver reports a SEGMENTATION FAULT at Step 35. In contrast, using CePRe, a counterexample could be found at Step 62.(4)
Since the encoding approach we use is taken from [15], propositions used in the encoding are only determined by the model and the bound; thus the number of required propositions does not change. For this reason, the corresponding experimental results on proposition numbers are not provided.Table 10
Experimental results of BMC-based MC with/withoutCePRe.
Model
Spec.
WithoutCePRe
WithCePRe
Max-bound
N.O.C.
Time (sec.)
N.O.C.
Time (sec.)
srg5
Ptimo.ltl†
272567
67.391
1371
0.143
20
Pti.gnv.ltl†
2101
0.116
299
0.024
6
Pti.g.ltl†
21
0.016
21
0.016
1
abp4
P2false.ltl
7532
3.972
7532
3.972
17
P2true.ltl†
12639
8.145
9369
7.753
20*
Pold.ltl
7499
9.087
7499
9.488
20*
Ptimo.ltl
6332
2.500
6332
2.512
16
Pti.g.ltl
11952
0.841
11952
0.976
20*
dme3
P0.ltl†
—
—
35102
524.207
62
P1.ltl
216
0.036
167
0.048
1
dme5
Mdl.ltl†
90
0.044
90
0.048
0
Wat.ltl†
367
0.048
274
0.052
1
Ptimo.neg
367
0.050
277
0.058
1
msi_w-trans
Sched.ltl
14235
1.076
14235
1.078
20*
Safety.ltl
12439
8.441
12439
8.448
20*
Seq.ltl†
1907
0.064
81
0.052
3Experimental results of PDR-based model checking are shown in Table11.(1)
For PDR-based model checking, we are mainly concerned about the time-overhead. Since that the PDR algorithm consumes memory evenly during verification, we do not provide the space-overhead here.(2)
Because the CePRe process is done in an individual phase in the PDR-based verification, we here also list the overhead for doing CePRe.(3)
We can see that a significant performance improvement could be made if we use CePRe in PDR-based model checking, and the extra overhead for preprocessing is still relatively negligible.Table 11
Experimental result of PDR-based MC with/withoutCePRe.
Model
Spec.
PDR time withoutCePRe (sec.)
PDR time withCePRe (sec.)
Extratime forCePRe (sec.)
srg5
Ptimo.ltl†
0.117
0.056
<0.001
Pti.gnv.ltl†
0.084
0.043
<0.001
Pti.g.ltl†
0.070
0.032
<0.001
abp4
P2false.ltl
3.187
3.185
0.004
P2true.ltl†
2.996
1.239
0.004
Pold.ltl
6.937
6.939
<0.001
Ptimo.ltl
0.910
0.912
<0.001
Pti.ltl
5.812
5.816
<0.001
dme3
P0.ltl†
9.815
6.086
<0.001
P1.ltl
0.147
0.142
0.004
dme5
Mdl.ltl†
3.072
1.731
0.004
Wat.ltl†
4.575
3.043
0.004
Ptimo.neg
0.073
0.073
0.004
msi_wtrans
Sched.ltl
0.135
0.136
<0.001
Safety.ltl
0.200
0.201
0.004
Seq.ltl†
0.091
0.045
0.006Note that both model-independent and model-dependent rules contribute to the reductions. For example, for the modelsrg5 and the specificationPti.g.ltl, the rules (FS) and (S) are applied; meanwhile, for the modelmsi_wtrans and the specificationSeq.ltl, the application of (UU[¬2→3]) is invoked.


### 5.2. Experiments w.r.t. Random Models and Specifications

We have also performed experiments upon randomly generated models and specifications with the tool Lbtt [25] and with the methodology suggested in [17].For BDD-based MC and bounded model checking, we conduct the comparison in the following manner. For each3≤l≤7, we randomly generate 40 specifications having length l. Subsequently, for each specification, we generate two models, respectively, for the BDD-based model checking and for BMC. Hence, we totally have 200 specifications and 400 models.For the BDD-based model checking, we give the comparative results on (1) the scale of BDD-nodes, (2) the number of reachable states, and (3) the time consumed, and the experimental results are, respectively, shown in Figures1, 2, and 3. For bounded model checking, we have set the maximum bound to 20 and we have compared (1) the number of clauses and (2) the executing time; the results are, respectively, shown in Figures 4 and 5. Each value here we provide is the average of the 40 executions.Figure 1
Results on the scale of BDD nodes in random BDD-MC experiments.Figure 2
Results on reachable states in random BDD-MC experiments.Figure 3
Time overhead in random BDD-MC experiments.Figure 4
The scale of clauses in random BMC experiments.Figure 5
Time overhead in random BMC experiments.For the BDD-based model checking, there are123 (out of 200) specifications that can be reduced, whereas for bounded model checking, the number of specifications that can be reduced is 118. Note that in this experiment, when CePRe is switched on, extra overheads (such as time) have also been taken into account.For the PDR-based model checking, the experiments are conducted as follows. We first generate50 SMV models with Lbtt and then we randomly generate LTL specifications for each model and each designated length. Next, we batchly do CePRe upon one group of specification copies and then obtain the product models (for each model and each specification). Subsequently, we convert the product models into AIG format with SMVtoAIG.We here compare the number of verfication obligations that could be accomplished within the preset time bound (i.e.,600 sec.), and the results are shown in Figure 6. From that, we can see that with the increment of the specification's length, the ratio (that could be done with CePRe to without CePRe) also monotonically increases.Figure 6
Experimental results of random PDR-based model checking.


## 5.1. Experiments upon Industrial Benchmarks

The benchmarks we choose in this paper are suggested in [4], and most of them come from real hardware verification.Table9 provides the experimental results for BDD-based LTL symbolic model checking. The field time is the executing time totally elapsed, and the field R.S. refers to the number of reachable states. For the experiments “with CePRe,” both the overheads of time and space are the summations of preprocessing and model checking. For Table 9, we have the following remarks.(1)
8 out of 16 specifications could be reduced with CePRe (and these specifications are marked with †).(2)
For the specifications that can be reduced, considerable improvements are made during verification. For example, for the specificationPit.g.ltl, with CePRe, the number of BDD nodes is decreased to 12.5% of that without using CePRe.(3)
When a specification cannot be reduced with CePRe, it spends a very low extra overhead for doing preprocessings.(4)
Something noteworthy we do not provide here is that in the case that a violated LTL specification can be reduced, the newly generated counterexample is usually shorter than that of before. Among 8 specifications that can be reduced, counterexample lengths ofPti.nuv.ltl,Pit.g.ltl,P0.ltl, andSeq.ltl are, respectively, shortened to 15, 10, and 194, opposing to the original values 16, 12, and 217. Meanwhile, counterexample lengths of others are kept unchanged.Table 9
Comparative results of BDD-based MC with/withoutCePRe.
Model
Spec.
WithoutCePRe
WithCePRe
BDD--Nodes
R.S.
Time(sec.)
BDD--Nodes
R.S.
Time(sec.)
srg5
Ptimo.ltl†
7946
720
0.024
2751
720
0.016
Pti.gnv.ltl†
29704
11460
0.058
5712
2880
0.012
Pti.g.ltl†
64749
130048
0.048
8119
32768
0.016
abp4
P2false.ltl
99577
559104
0.200
99625
559104
0.202
P2true.ltl†
61209
904384
0.066
56494
419296
0.064
Pold.ltl
52301
353536
0.060
52349
353536
0.064
Ptimo.ltl
78098
219616
0.080
78146
219616
0.088
Pti.g.ltl
8385
200704
0.060
8433
200704
0.062
dme3
P0.ltl†
889773
35964
5.756
527983
26316
5.096
P1.ltl
455148
8775
0.460
409432
5505
0.374
dme5
Mdl.ltl†
793942
8.64316
e
+
06
167.346
814494
3.2097
e
+
06
114.599
Wat.ltl†
412867
1.79217
e
+
07
302.005
967033
1.12567
e
+
07
286.850
Ptimo.neg
508036
1.26202
e
+
06
3.260
508081
1.26202
e
+
06
3.280
msi_w-trans
Sched.ltl
2275558
7.31055
e
+
07
6.612
2275655
7.31055
e
+
07
6.632
Safety.ltl
1213308
3.6528
e
+
07
7.568
1213460
3.6528
e
+
07
7.644
Seq.ltl†
1921973
3.5946
e
+
07
93.570
1702585
1.7973
e
+
07
94.085Table10 gives the experimental results for BMC-based model checking, and we here give some comments on that.(1)
With NuSMV, we need to preset a max-bound when doing bounded model checking. The column max-bound gives such values—a “star mark” means that this bound does not reach the completeness threshold. The field N.O.C. designates the number of clauses generated during model checking.(2)
From Table10, we can see that without CePRe the specificationPti.gnv.ltl generates 2101 clauses when the verification stops; in contrast, it only produces 299 clauses if CePRe is switched on.(3)
Another comparison is forP0.ltl upondme3: If we do not do any reduction, the SAT solver reports a SEGMENTATION FAULT at Step 35. In contrast, using CePRe, a counterexample could be found at Step 62.(4)
Since the encoding approach we use is taken from [15], propositions used in the encoding are only determined by the model and the bound; thus the number of required propositions does not change. For this reason, the corresponding experimental results on proposition numbers are not provided.Table 10
Experimental results of BMC-based MC with/withoutCePRe.
Model
Spec.
WithoutCePRe
WithCePRe
Max-bound
N.O.C.
Time (sec.)
N.O.C.
Time (sec.)
srg5
Ptimo.ltl†
272567
67.391
1371
0.143
20
Pti.gnv.ltl†
2101
0.116
299
0.024
6
Pti.g.ltl†
21
0.016
21
0.016
1
abp4
P2false.ltl
7532
3.972
7532
3.972
17
P2true.ltl†
12639
8.145
9369
7.753
20*
Pold.ltl
7499
9.087
7499
9.488
20*
Ptimo.ltl
6332
2.500
6332
2.512
16
Pti.g.ltl
11952
0.841
11952
0.976
20*
dme3
P0.ltl†
—
—
35102
524.207
62
P1.ltl
216
0.036
167
0.048
1
dme5
Mdl.ltl†
90
0.044
90
0.048
0
Wat.ltl†
367
0.048
274
0.052
1
Ptimo.neg
367
0.050
277
0.058
1
msi_w-trans
Sched.ltl
14235
1.076
14235
1.078
20*
Safety.ltl
12439
8.441
12439
8.448
20*
Seq.ltl†
1907
0.064
81
0.052
3Experimental results of PDR-based model checking are shown in Table11.(1)
For PDR-based model checking, we are mainly concerned about the time-overhead. Since that the PDR algorithm consumes memory evenly during verification, we do not provide the space-overhead here.(2)
Because the CePRe process is done in an individual phase in the PDR-based verification, we here also list the overhead for doing CePRe.(3)
We can see that a significant performance improvement could be made if we use CePRe in PDR-based model checking, and the extra overhead for preprocessing is still relatively negligible.Table 11
Experimental result of PDR-based MC with/withoutCePRe.
Model
Spec.
PDR time withoutCePRe (sec.)
PDR time withCePRe (sec.)
Extratime forCePRe (sec.)
srg5
Ptimo.ltl†
0.117
0.056
<0.001
Pti.gnv.ltl†
0.084
0.043
<0.001
Pti.g.ltl†
0.070
0.032
<0.001
abp4
P2false.ltl
3.187
3.185
0.004
P2true.ltl†
2.996
1.239
0.004
Pold.ltl
6.937
6.939
<0.001
Ptimo.ltl
0.910
0.912
<0.001
Pti.ltl
5.812
5.816
<0.001
dme3
P0.ltl†
9.815
6.086
<0.001
P1.ltl
0.147
0.142
0.004
dme5
Mdl.ltl†
3.072
1.731
0.004
Wat.ltl†
4.575
3.043
0.004
Ptimo.neg
0.073
0.073
0.004
msi_wtrans
Sched.ltl
0.135
0.136
<0.001
Safety.ltl
0.200
0.201
0.004
Seq.ltl†
0.091
0.045
0.006Note that both model-independent and model-dependent rules contribute to the reductions. For example, for the modelsrg5 and the specificationPti.g.ltl, the rules (FS) and (S) are applied; meanwhile, for the modelmsi_wtrans and the specificationSeq.ltl, the application of (UU[¬2→3]) is invoked.


## 5.2. Experiments w.r.t. Random Models and Specifications

We have also performed experiments upon randomly generated models and specifications with the tool Lbtt [25] and with the methodology suggested in [17].For BDD-based MC and bounded model checking, we conduct the comparison in the following manner. For each3≤l≤7, we randomly generate 40 specifications having length l. Subsequently, for each specification, we generate two models, respectively, for the BDD-based model checking and for BMC. Hence, we totally have 200 specifications and 400 models.For the BDD-based model checking, we give the comparative results on (1) the scale of BDD-nodes, (2) the number of reachable states, and (3) the time consumed, and the experimental results are, respectively, shown in Figures1, 2, and 3. For bounded model checking, we have set the maximum bound to 20 and we have compared (1) the number of clauses and (2) the executing time; the results are, respectively, shown in Figures 4 and 5. Each value here we provide is the average of the 40 executions.Figure 1
Results on the scale of BDD nodes in random BDD-MC experiments.Figure 2
Results on reachable states in random BDD-MC experiments.Figure 3
Time overhead in random BDD-MC experiments.Figure 4
The scale of clauses in random BMC experiments.Figure 5
Time overhead in random BMC experiments.For the BDD-based model checking, there are123 (out of 200) specifications that can be reduced, whereas for bounded model checking, the number of specifications that can be reduced is 118. Note that in this experiment, when CePRe is switched on, extra overheads (such as time) have also been taken into account.For the PDR-based model checking, the experiments are conducted as follows. We first generate50 SMV models with Lbtt and then we randomly generate LTL specifications for each model and each designated length. Next, we batchly do CePRe upon one group of specification copies and then obtain the product models (for each model and each specification). Subsequently, we convert the product models into AIG format with SMVtoAIG.We here compare the number of verfication obligations that could be accomplished within the preset time bound (i.e.,600 sec.), and the results are shown in Figure 6. From that, we can see that with the increment of the specification's length, the ratio (that could be done with CePRe to without CePRe) also monotonically increases.Figure 6
Experimental results of random PDR-based model checking.


## 6. Concluding Remarks

In this paper, we present a new technique to reduce LTL specifications' complexity towards symbolic model checking, namely, CePRe. The novelty in this technique is that the reduced formula needs not be logically equivalent with the original one but just preserves the counterexample set. Moreover, the condition enabling such a reduction can be usually detected with lightweight approaches, such as SAT-solving. Hence, this technique could leverage the power of SAT-solvers.The central part of CePRe is a set of reduction rules, and soundness of these reduction rules is fairly easy to check. For the model-dependent rules, additional conditions mainly concern the invariants and transitions, and we do not make a sufficient use of other features, such as fairness. In this paper, the rules are given by enumerating all possible combinations of (at most two) temporal operators. Indeed, there might be some other reduction schemas we are not aware of.From the experimental results, we can see that in a statistical perspective, a better performance and lower overhead can be achieved with CePRe. For the future work, we would consider how to extend our idea to symbolic model checking upon rich assertional languages, such as PSL.



---

*Source: 702165-2014-05-14.xml*