# Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives

Authors: Rui Wang; Wanwei Liu; Tun Li; Xiaoguang Mao; Ji Wang
Journal: Journal of Applied Mathematics
 (2013)

---

## Abstract

As a complementary technique of the BDD-based approach, bounded model checking (BMC) has
been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is
rather limited, and some important properties cannot be captured by such logic. In this paper, we
present a semantic BMC encoding approach to deal with the mixture ofETLf and ETLl. Since
such kind of temporal logic involves both finite and looping automata as connectives, all regular
properties can be succinctly specified with it. The presented algorithm is integrated into the model
checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.


---

## Body

## 1. Introduction

A crucial bottleneck of model checking is thestate-explosion problem, and the symbolic model checking technique has proven to be an applicable approach to alleviate it. In the early 1990s, McMillan presented the BDD [1] based model checking technique [2]. It is first applied to CTL model checking and is later adapted to deal with LTL. With the rapid evolvement of SAT solvers, an entirely new approach, namely, bounded model checking (BMC), is presented in [3]. It rerpresents the problem “there is a path (with bounded length) violating the specification in the model” with a Boolean formula and then tests its satisfiability via a SAT solver. Usually, BMC is considered to be a complementary approach of the BDD-based approach: BMC is normally used for hunting bugs not for proving their absence. It performs better when handling a model having a large reachable state set but involving (relatively) shallow error runnings.BMC has been successfully employed in LTL model checking. However, LTL has the drawback of limited expressiveness. Wolper was the first to complain about this by addressing the fact that somecounting properties such as “p holds at every even moment” cannot be expressed by any LTL formula [4]. Indeed, LTL formulae are just as expressive as star-freeω-expressions, that is, ω-regular expressions disallowing arbitrary (in a star-free expression, Kleene-closure operators (•* and •ω) can only be applied upon Σ, which is the whole set of alphabet) use of Kleene-closure operators.As pointed in [5, 6], it is of great importance for a specification language to have the power to express all ω-regular properties—as an example, it is a necessary requirement to support modular model checking. Actually, such specification language like PSL [7] has been accepted as industrial standard.For temporal logics within linear framework, there are several ways to pursue such an expressiveness.(1)
The first way is to add fixed-point operators or propositional quantifiers to the logic, such as linearμ-calculus [8] and QLTL [9].(2)
An alternative choice is to add regular expressions to LTL-like logics, as done in RLTL [10], FTL [11, 12], and PSL [7].(3)
The third approach is to cooperate infinitely many temporal connectives with the logic, just like various of ETLs [4, 9, 13].The first extension requires finitely many operators in defining formulae. Meanwhile, the use of fixed-point operators and higher-order quantifiers tends to rise difficulties in understanding. In contrast, using regular expressions or automata as syntactical ingredients is much more intuitive in comprehension. To some extent, since nesting of automata connectives is allowed, the third approach generalizes the second one.In [4], Wolper suggested using right linear grammars as connectives. Later, Wolper, Vardi, and Sistla consider taking various ω-automata [9, 13]. Depending on the type of automata used as temporal connectives, we may obtain various ETLs. As a result, ETLs employing ω-automata with looping, finite, and repeating (alternatively, Büchi [14]) acceptance are, respectively, named ETLl, ETLf, and ETLr, and all of them are known to be as expressive as ω-regular expressions [13].We have presented a BDD-based model checking algorithm forETLf in [15] and an algorithm for BDD-based model checking of an invariant of PSL in [16]. Jehle et al. present a bounded model checking algorithm for linear μ-calculus in [17]. And in [18], a tester based symbolic model checking approach is proposed by Pnueli and Zacks to deal with PSL properties. Meanwhile, a modular symbolic Büchi automata construction is presented in [19] by Cimatti et al.In this paper, we present a semantic BMC encoding for ETL employing both finite acceptance and looping acceptance automata connectives (we in the following refer to it asETLl+f). The reason that we study BMC algorithm for such kind of logic is for the following considerations.(1)
The BDD-based symbolic model checking technique forETLf has been established in [15] by extending LTL construction [20]. Nevertheless, in a pure theoretical perspective, looping and finite acceptance, respectively, correspond to safety and liveness properties, and looping acceptance automata can be viewed as the counterparts of finite acceptance automata. Actually, both similarities and differences could be found in compiling the semantic models and translating Boolean representations when dealing with these two types of connectives. Since ETLl+f has a rich set of fragments, such as LTL, it is hopeful to develop a unified semantic BMC framework of such logics.(2)
Practically, things would usually be much more succinct when employing both types of automata connectives, in comparison to merely using finite or looping ones. As an example, there is no direct encoding for the temporal operatorG just with finite acceptance automata—to do this with ETLf, we need to use a two-state and two-letter connective to represent the operator F and then to dualize it. In contrast, with looping automata, we just need to define a one-state and one-letter connective. It would save much space overhead in building tableaux.(3)
Lastly, unlike syntactic BMC encodings (such kind of encodings give inductive Boolean translations with the formulae’s structure, cf. [21, 22] for a survey), the semantic fashion [22] yields a natural completeness threshold computation approach, and it describes the fair path finding problem over the product model with Boolean formulae. In this paper, we give a linear semantic encoding approach (opposing to the original quadratic semantic encoding) for ETLl+f. Moreover, the technique can also be tailored to semantic LTL BMC.We have implemented the presented algorithm with our model checker ENuSMV (Ver. 1.2), and this tool allows end users to customize temporal connectives by defining automata. We have also justified the algorithm by conducting a series of comparative experiments.The paper is structured as follows: Section2 briefly revisits basic notions. Section 3 introduces semantic BMC encoding technique for ETLl+f. In Section 4, experimental results of ETLl+f BMC are given. Finally, we conclude the whole paper with Section 5.


## 2. Preliminaries

An infinitewordw over the alphabet Σ is a mapping from ℕ to Σ; hence we may use w(i) to denote the ith letter of w. For the sake of simplicity, we usually write w as the sequence w(0)w(1)⋯. A finite prefix of w with length n is a restriction of w to the domain {0,…,n-1}, denoted by w[n].A (nondeterministic)automaton is a tuple 𝒜=〈Σ,Q,δ,q,F〉, where:  (i)
Σ is a finite alphabet,(ii)
Q is a finite set of states,(iii)
δ:Q×Σ→2Q is a transition function,(iv)
q∈Q is an initial state, and(v)
F⊆Q is a set of accepting states.Aninfinite run of 𝒜=〈Σ,Q,δ,q,F〉 over an infinite word w is an infinite sequence σ=q0q1⋯∈Qω, where q0=q and qi+1∈δ(qi,w(i)) for each i. In addition, we say that each prefix q0⋯qn+1 is a finite run over w[n].In this paper, we are concerned with two acceptance types forω-automata.  Looping. An infinite word w is accepted if it has an infinite run over w.Finite. An infinite word w is accepted if it has a finite prefix w[n], over which there is a finite run q0⋯qn+1 and qn+1 is an accepting state (call such a prefix accepting prefix).In both cases, we denote byℒ(𝒜) the set of infinite words accepted by 𝒜.Given an automaton𝒜=〈Σ,Q,δ,q,F〉 and a state r∈Q, we denote by 𝒜r the automaton 〈Σ,Q,δ,r,F〉. That is, 𝒜r is almost identical to 𝒜, except for that its initial state is replaced by r. Hence, 𝒜 and 𝒜q are the same.Given a set ofatomic propositionsAP, the class of ETLl+f formulae can be inductively defined as follows.  (i)
Both⊤ and ⊥ are ETLl+f formulae.(ii)
Each propositionp∈AP is an ETLl+f formula.(iii)
Ifφ is an ETLl+f formula, then ¬φ and ○φ are ETLl+f formulae.(iv)
Ifφ1, φ2 are ETLl+f formulae, then both φ1∧φ2 and φ1∨φ2 are ETLl+f formulae.(v)
If𝒜 is an automaton with the alphabet Σ={a1,…,an} and φ1,…,φn are ETLl+f formulae, then 𝒜(φ1,…,φn) is also an ETLl+f formula.Remark 1.
In the original definition of various ETLs (sayETLl, ETLf, and ETLr), the “next operator” (○) is not explicitly declared. However, this operator is extremely important in building the semantic BMC encodings for ETLl+f. Hence, we explicitly use this operator in our definition, and it would not change the expressiveness of the logic.Remark 2.
Since we employ both finite and looping acceptance automata connectives, our logic is a mixture ofETLl and ETLf. On the one hand, ETLl+f generalizes both of these two logics; on the other hand, it can be embedded into ETLr; hence this logic is also as expressive as omega-regular expressions.Thesatisfaction relation of an ETLl+f formula φ with respect to an infinite word π∈(2AP)ω and a position i∈ℕ is inductively given as follows.  (i)
π,i⊨⊤ and π,i⊭⊥.(ii)
π,i⊨p if and only if p∈π(i).(iii)
π,i⊨¬φ if and only if π,i⊭φ.(iv)
π,i⊨○φ if and only if π,i+1⊨φ.(v)
π,i⊨φ1∧φ2 if and only if π,i⊨φ1 and π,i⊨φ2.(vi)
π,i⊨φ1∨φ2 if and only if π,i⊨φ1 or π,i⊨φ2.(vii)
If𝒜 is a looping acceptance automaton with the alphabet {a1,…,an}, then π,i⊨𝒜(φ1,…,φn) if and only if: there is an infinite word w∈ℒ(𝒜), and, for each j∈ℕ, w(j)=ak implies π,i+j⊨φk.(viii)
If𝒜 is a finite acceptance automaton with the alphabet {a1,…,an}, then π,i⊨𝒜(φ1,…,φn) if and only if: there is an infinite word w∈ℒ(𝒜) with an accepting prefix w[n], such that, for each j<n, w(j)=ak implies π,i+j⊨φk.As usual, we directly useπ⊨φ in place of π,0⊨φ.To make a better understanding ofETLl+f formulas, we here give some examples of the use of automata connectives.  (1)
Considering the LTL formulaφ1Uφ2, it can be described with an ETLl+f formula 𝒜U(φ1,φ2), where 𝒜U is the finite acceptance automaton 〈{a1,a2},{q1,q2},δU,q1,{q2}〉, and we let δU(q1,a1)={q1}, δU(q1,a2)={q2}, and δU(q2,a1)=δU(q2,a2)=∅.(2)
The LTL formulaGφ is equivalent to the ETLl+f formula 𝒜G(φ), where 𝒜G=〈{a},{q},δG,q,∅〉 is a looping acceptance automaton and δG(q,a)={q}.Remark 3.
The order of letters is important in defining automata connectives. Hence, the alphabet should be considered as a vector, rather than a set.We usesub(φ) to denote the set of subformulae of φ. A formula φ is in negation normal form (NNF) if all negations in φ are adjacent to atomic propositions or automata connectives. One can achieve this by repeatedly using De Morgan’s law and the schemas of ¬○φ≡○¬φ and ¬¬φ≡φ. In addition, we call a formula φ being of the form 𝒜(φ1,…,φn) an automaton formula.Given a formulaφ (in NNF), we use a two-letter-acronym to designate the type of an automaton subformula of φ: the first letter is either “P” or “N,” which means “positive” or “negative”; and the second letter can be “F” or “L,” which describes the acceptance type. For example, NL-subformulae stand for “negative automata formulae with looping automata connectives,” such as ¬𝒜q(φ1,φ2), where 𝒜 is a two-letter looping automaton.Amodel or interchangeably a labeled transition system (LTS) is a tuple ℳ=〈S,ρ,I,L,ℱ〉, where:  (i)
S is a finite set of states,(ii)
ρ⊆S×S is a transition relation (usually, we require ρ to be total; that is, for each s∈S, there is some s′∈S having (s,s′)∈ρ),(iii)
I⊆S is the set of initial states,(iv)
L:S→2AP is the labeling function, and(v)
ℱ⊆2S is a set of fairness constraints.Apath of ℳ is an infinite sequence σ=s0s1⋯∈Sω, where s0∈I and (si,si+1)∈ρ for each i∈ℕ. In addition, σ is a fair path if σ visits each F∈ℱ infinitely often. Formally, σ is a fair path if inf(σ)∩F≠∅ for each F∈ℱ, where inf(σ) denotes the set of states occurring infinitely many times in σ.An infinite wordπ=a0a1⋯ is derived from a path σ of ℳ (denoted by π=L(σ)) if ai=L(si) for each i∈ℕ. We use ℒ(ℳ) to denote the set of infinite words derived from fair paths of ℳ.Given anETLl+f formula φ and an LTS ℳ, we denote by ℳ⊨φ if π⊨φ for each π∈ℒ(ℳ). The model checking problem of ETLl+f is just to verify if ℳ⊨φ holds for the given LTS ℳ and the given ETLl+f formula φ.


## 3. Semantic BMC Encoding for ETLl+f

In this section, we will give a detailed description of the semantic BMC encoding forETLl+f. Firstly, we show how to extend the tableau construction of LTL [20] to that of ETLl+f, and hence a product model can also be constructed. Subsequently, we interpret the fairness path finding problem (upon the product model) into SAT, and the size blow-up of this encoding is linear with the bound.For the sake of convenience, in this section, we always assume that the givenETLl+f formulae have been normalized into NNF.


### 3.1. The Tableaux of ETLl+f Formulae

Given anETLl+f formula φ, we first inductively define its elementary formula setel(φ) as follows.  (i)
el(⊤)=el(⊥)=∅.(ii)
el(p)=el(¬p)={p} for each p∈AP.(iii)
el(φ1∧φ2)=el(φ1∨φ2)=el(φ1)∪el(φ2).(iv)
el(○φ)=el(φ)∪{○φ}.(v)
Ifφ=𝒜q(φ1,…,φn) or φ=¬𝒜q(φ1,…,φn) and the states set of 𝒜 is Q, then
(1)el(φ)=⋃1≤k≤n‍el(φk)∪{○𝒜q′(φ1,…,φn)∣q′∈Q}.Hence, ifψ∈el(φ), then ψ is either an atomic proposition or a formula rooted at the next operator.Subsequently, we define the function sat, which maps each subformulaψ of φ to a set of members in 2el(φ). Inductively the following hold.  (i)
sat(⊤)=2el(φ); sat(⊥)=∅.(ii)
sat(p)={Γ⊆el(φ)∣p∈Γ} and sat(¬p)={Γ⊆el(φ)∣p∉Γ}.(iii)
sat(○ψ)={Γ⊆el(φ)∣○ψ∈Γ}.(iv)
sat(φ1∧φ2)=sat(φ1)∩sat(φ2) and sat(φ1∨φ2)=sat(φ1)∪sat(φ2).(v)
Suppose that𝒜=〈{a1,…,an},Q,δ,q,F〉.
(1)
If𝒜 is a looping acceptance automaton or a finite acceptance automaton and q∉F, then
(2)sat(𝒜q(φ1,…,φn))=⋃1≤k≤n‍(sat(φk)∩⋃q′∈δ(q,ak)‍sat(○𝒜q′(φ1,…,φn))).(2)
If𝒜 is a finite acceptance automaton and q∈F, then sat(𝒜q(φ1,…,φn))=2el(φ).(vi)
sat(¬𝒜q(φ1,…,φn))=2el(φ)∖sat(𝒜q(φ1,…,φn)).Recall the tableau construction for LTL [20], an “until subformula” would generate a fairness constraint to the tableau. Indeed, such a subformula corresponds to a “least-fixpoint subformula” if we translate the specification into a logic employing higher-order quantifiers, such as μ-calculus. Similarly, for ETLl+f, the PF- and NL-subformulae also impose fairness constraints. For this reason, we need to define the following two auxiliary relations before giving the tableau construction.For a PF-subformulaψ=𝒜(φ1,…,φn) of φ, where 𝒜=〈{a1,…,an},Q,δ,q,F〉, we define a relation Δψ+⊆(2el(φ)×2Q)×(2el(φ)×2Q) as follows: suppose that Γ,Γ′⊆el(φ) and P,P′⊆Q; then ((Γ,P),(Γ′,P′))∈Δψ+ if and only if the following hold.  (i)
WhenP≠∅, then, for each q∈P∖F, there exists some 1≤k≤n such that Γ∈sat(φk) and P′∩δ(q,ak)≠∅.(ii)
WhenP=∅, then q∈P′ if and only if Γ′∈sat(𝒜q(φ1,…,φn)) for each q∈Q.Likewise, for each NL-subformulaψ=¬𝒜(φ1,…,φn) of φ, we also define a relation Δψ-⊆(2el(φ)×2Q)×(2el(φ)×2Q). In detail, for any Γ,Γ′⊆el(φ) and P,P′⊆Q, we have ((Γ,P),(Γ′,P′))∈Δψ- if and only if the following hold.  (i)
WhenP≠∅, then, for each q∈P and 1≤k≤n, we have: Γ∈sat(φk) implies δ(q,ak)⊆P′.(ii)
WhenP=∅, then q∈P′ if and only if Γ′∉sat(𝒜q(φ1,…,φn)), for each q∈Q.We now describe the tableau construction forφ. Suppose that ψ1,…,ψm and ¬η1,…,¬ηn are, respectively, all the PF-subformulae and NL-subformulae occurring in φ then the tableau 𝒯φ is such an LTS 〈Sφ,ρφ,Iφ,Lφ,ℱφ〉, where:(i)
Sφ consists of tuples like 〈Γ;P1,…,Pm;R1,…,Rn〉, where Γ⊆el(φ) and each Pi (resp., Ri) is a subset of ψi’s (resp., ηi’s) connective’s state set.(ii)
For two statess=〈Γ;P1,…,Pm;R1,…,Rn〉 and s′=〈Γ′;P1′,…,Pm′;R1′,…,Rn′〉, (s,s′)∈ρφ if and only if the following three conditions hold.
(1)
Γ∈sat(○ψ) if and only if Γ′∈sat(ψ) for each ○ψ∈el(φ).(2)
((Γ,Pi),(Γ′,Pi′))∈Δψi+ for each 1≤i≤m.(3)
((Γ,Rj),(Γ′,Rj′))∈Δ¬ηj- for each 1≤j≤n.(iii)
Iφ={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Γ∈sat(φ)}.(iv)
Lφ(〈Γ;P1,…,Pm;R1,…,Rn〉)=Γ∩AP.(v)
ℱφ={Fi+∣1≤i≤m}∪{Fj-∣1≤j≤n}, where
(3)Fi+={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Pi=∅},Fj-={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Rj=∅}.The below two theorems (Theorems4 and 5) reveal the language property of ETLl+f tableaux. To remove the lengthiness, we here just provide the proof sketches, and rigorous proofs of them are postponed to the appendices.Theorem 4.
For eachπ∈(2AP)ω, if π∈ℒ(𝒯φ), then π⊨φ.Proof (sketch).
Just assume thatσ=s0s1⋯∈Sφω is the corresponding fair path of 𝒯φ such that π=Lφ(σ), where si=〈Γi;P1,i,…,Pm,i;R1,i,…,Rn,i〉. We may inductively prove the following claim.
“For eachψ∈sub(φ)∪el(φ), we have: Γi∈sat(ψ) implies π,i⊨ψ.”
Because we require thatΓ0∈sat(φ), hence we have π,0⊨φ.Theorem 5.
For eachπ∈(2AP)ω, if π⊨φ, then π∈ℒ(𝒯φ).Proof (sketch).
Suppose thatπ⊨φ; to show π∈ℒ(𝒯φ), we need to first construct an infinite state sequence σ=s0s1⋯∈Sφω guided by π (the detailed construction is given in Section A.2), and then we will subsequently show that σ is a fair path of 𝒯φ and π=Lφ(σ).The following theorem is immediate from Theorems4 and 5.Theorem 6.
The modelℳ violates the ETLl+f property φ if and only if ℒ(ℳ)∩ℒ(𝒯¬φ)≠∅, equivalently; there exists some fair path in ℳ×𝒯¬φ.Theorem 7.
For anETLl+f formula φ, its tableau 𝒯φ has at most 4|el(φ)| states.Proof.
Observe that a state should be of the form〈Γ;P1,…,Pm;R1,…,Rn〉. For Γ, there are 2|el(φ)| possible choices. Suppose that ψj=𝒜j(φ1,…,φk) (resp., ¬ηi=¬𝒜i(φ1′,…,φr′)) and the state set of 𝒜j is Qj (resp., 𝒜i with Qi′). According to the construction, each q∈Qj (resp., q∈Qi′) corresponds to a unique elementary formula ○𝒜jq(φ1,…,φk) (resp., ○𝒜iq(φ1′,…,φr′)), and such a mapping is an injection. Hence we have
(4)(∑1≤j≤m‍|Qj|+∑1≤i≤n‍|Qi′|)≤|el(φ)∖AP|.
Note that Pj⊆Qj (resp., Ri⊆Qi′), and hence we have |Sφ|≤(2|el(φ)|)2=4|el(φ|).


### 3.2. The Linear Semantic Encoding

Practically, a model’s state space is determined by the evaluation of a set of variables. Further, we may assume that each of them is a “Boolean variable” (which corresponds to a proposition belonging toAP), because every variable over finite domain could be encoded with several Boolean variables.Let𝒞=〈S,ρ,I,L,ℱ〉 be an arbitrary LTS, and we also assume that the corresponding variable set is V={p1,…,pn}; then each state s∈S uniquely corresponds to an assignment of such pis.If we uses(pi) to denote the value of pi at s, then each subset Z⊆S can be represented by a Boolean formula ΦZ over V. In detail, it fulfills
(5)s∈S⟺s⊩ΦZ,
where s⊩ΦZ means that ΦZ is evaluated to be true if we assign each pi with the value s(pi).LetV′={p1′,…,pn′}, and each binary relation λ⊆S×S also has a Boolean representation Φλ over the variable set V∪V′. That is,
(6)(s1,s2)∈λ⟺(s1,s2)⊩Φλ,
where (s1,s2)⊩Φλ  means that Φλ is evaluated to be true if we assign each pi with s1(pi) and assign each pi′ with s2(pi).Hence, all components ofℳ can be encoded: I and ρ can be represented by two Boolean formulae ΦI and Φρ, respectively; we subsequently create a Boolean formula ΦF for each F∈ℱ; note that the labeling function L is not concerned any longer, because the sates labeled with p can be captured by the Boolean formula p.For example, from Theorem7, we have that the symbolic representation of 𝒯φ requires 2×|el(φ)∖AP|  new Boolean variables—because variables in el(φ)∩AP can be shared with the encoding of the original model.A canonical Boolean encoding of fair path existence detection upon LTSs is presented in [22]: given a model 𝒞=〈S,ρ,I,L,ℱ〉 and a boundk∈ℕ, one may use the formula
(7)ΦI(0)∧⋀0≤i<kΦρ(i,i+1)∧⋁0≤ℓ≤k(Φρ(k,ℓ)∧⋀F∈ℱ⋁ℓ≤j≤kΦF(j)),
where ΦI(j) and ΦF(j) are, respectively, the Boolean formulae obtained from ΦI and ΦF by replacing each variable p with a new copy p(j), and Φρ(i,j) is obtained from Φρ by replacing each p with p(i) and replacing each p′ with p(j).It can be seen that this formula is satisfiable if and only if𝒞 involves a fair path of the form s0s1⋯sℓ-1(sℓ⋯sk)ω (call it is of the lasso shape). Since that ℒ(𝒞)≠∅ if and only if 𝒞 contains some lasso fair path (note that from each fair path we may derive another fair path of lasso shape), hence we may convert the fair path detection into the satisfiability problem of the above Boolean formula.However, a closer look shows that the size of such encoding is quadratic with the bound. To reduce the blow-up in size, we need to introduce the following new variables (the linearization can also be done with the syntactic fashion presented in [23, 24]. We would draw a comparison of these two approaches in Section 4.).  (1)
For each0≤ℓ≤k, we introduce a new variable rℓ. Intuitively, rℓ indicates that sℓ is a successor of sk.(2)
For each fairness constraintF∈ℱ and each 0≤ℓ≤k, we introduce a variable fF(ℓ), and this variable is evaluated to be true only if there is some ΦF(j) which is evaluated to true, where ℓ≤j≤k.And the new encoding (with the boundk∈ℕ) can be formulated as
(8)ΦI(0)∧⋀0≤i<kΦρ(i,i+1)∧⋁0≤ℓ≤krℓ,Ψ𝒞(k)=∧⋀0≤ℓ≤k(rℓ⟶(Φρ(k,ℓ)∧⋀F∈ℱfF(ℓ)))∧⋀F∈ℱ(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))∧(fF(k)⟶ΦF(k))(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))).Hence, both the number of variables and the size of this encoding are linear withk. Moreover, the following theorem guarantees the correctness of such encoding.Theorem 8.
ℒ
(
𝒞
)
≠
∅ if and only if  Ψ𝒞(k) is satisfiable for some k.Proof.
We begin with the “if” direction: suppose that the variable set is{p1,…,pm}; if there is some k such that Ψ𝒞k is evaluated to 1 (i.e., true) under the assignment e, then we denote si=(e(p1(i)),…,e(pm(i))) for each 1≤i≤m. Hence, each si is a state of 𝒞.  (i)
Since the truth value ofΦI(0) is 1 under e, then we have s0⊩ΦI(0); this implies that s0∈I.(ii)
For each0≤i<k, we have (si,si+1)⊩Φρ(i,i+1), and thus (si,si+1)∈ρ.(iii)
Because we have the conjunct⋁0≤ℓrℓ, then there is some 0≤ℓ≤k such that e(rℓ)=1. In the following, we fix this specific value ℓ for the discussion.(iv)
According to the constraintrℓ→(Φρ(k,ℓ)∧⋀F∈ℱfF(ℓ)), we have the following.
(1)
e(Φρ(k,ℓ))=1, which indicates that (sk,sℓ)∈ρ.(2)
For eachF∈ℱ, we have e(fF(ℓ))=1.(v)
For each fairness constraintF∈ℱ and 0≤i≤k, we now inductively show that “e(fF(i))=1 implies e(ΦF(j))=1 (alternatively, sj∈F) for some i≤j≤k.” First of all, it holds in the case of i=k, because we have the constraint f(k)→ΦF(k). In addition, the fact of “when i=c, it holds” can be immediately inferred from the hypothesis “when i=c+1, it holds,” according to the conjunct fF(i)→(fF(i+1)∨ΦF(i)). Since we have shown that e(fF(ℓ))=1, we can conclude that there exists some ℓ≤j≤k such that sj∈F.
The above shows thats0s1⋯sℓ-1(sℓ⋯sk)ω is a fair path of 𝒞, and hence ℒ(𝒞)≠∅.
Conversely, for the “only if” direction, it suffices to find somek and some assignment e evaluating Ψ𝒞(k) to be true. Since ℒ(𝒞)≠∅, there must exist some fair path of lasso shape in 𝒞. Without loss of generality, assume that σ=s0s1⋯sℓ-1(sℓ⋯sk)ω is such a path; just let k be this value, and we now illustrate how the assignment e is constructed.  (i)
For each variablepj and each i≤k, let e(pj(i))=si(pj). Since s0 is an initial state, according to the definition, we have e(ΦI(0))=1. Meanwhile, because each (si,si+1)∈ρ, we have that the conjunction ⋀0≤i≤kΦρ(i,i+1) is satisfied under e.(ii)
For each0≤i≤k, we let
(9)e(ri)={1,i=ℓ,0,i≠ℓ.
Then it can be seen that e(⋁0≤i≤kri)=1.(iii)
For eachF∈ℱ and each 0≤i≤k, we let
(10)e(fF(i))={1,ifthereissomej≥isuchthatsj∈F,0,otherwise.
Then it can be directly checked that the conjunct
(11)⋀F∈ℱ(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))∧(fF(k)⟶ΦF(k)))
is evaluated to be true under e.(iv)
Since(sk,sℓ)∈ρ, we have e(Φρ(k,ℓ))=1. Also note that σ is a fair path; then for each F∈ℱ there is some sj∈F, where ℓ≤j≤k. According to the previous definition, we can infer that e(⋀F∈ℱfF(ℓ))=1. Thus the conjunct
(12)⋀0≤i≤k(ri⟶(Φρ(k,i)∧⋀F∈ℱfF(i)))
is also satisfied under e (recall that we have assigned e(ri)=0 in the case of i≠ℓ).Thus, the formulaΨ𝒞(k) is satisfiable.For bounded model checking, an important issue is thecompleteness threshold, which is the specific value k such that we may declare ℒ(𝒞)=∅ in the case that Ψ𝒞(k) is not satisfiable, and we denote it by CT(𝒞) in this paper.Since we need only to concern about fair paths of the formσ1(σ2)ω, as pointed in [22], a possible candidate for the completeness threshold CT(𝒞) is
(13)DI(𝒞)+|ℱ|×D(𝒞),
where D and DI are, respectively, the diameter and the initialized diameter (cf. [22]). Since [22] just considers LTSs having only one fairness constraint, we here add the factor |ℱ|.Observe that the partσ2 must be enclosed in some SCC (i.e., strongly connected component) of 𝒞, and we may replace D(𝒞) with D(𝒮), where 𝒮 is the largest SCC that intersects all fairness constraints. Therefore, we may get a more compact upper bound of the completeness threshold.Then, for a given LTSℳ and the given ETLl+f formula φ, since we have shown that ℳ⊭φ if and only if ℳ×𝒯¬φ involves some fair path, we now just need to test if there is some k making Ψℳ×𝒯¬φ(k) satisfiable, where k≤CT(ℳ×𝒯¬φ).Remark 9.
In the case that𝒞=𝒞1×𝒞2, where 𝒞=〈S,ρ,I,L,ℱ〉 and 𝒞i=〈Si,ρi,Ii,Li,ℱi〉 for i=1,2, we have ΦI=ΦI1∧ΦI2, Φρ=Φρ1∧Φρ2, and Φℱ=Φℱ1∪Φℱ1, and in addition, the variable set of 𝒞 is just the union of the variable sets of 𝒞1 and 𝒞2.Remark 10.
Actually, for anETLl+f formula φ, the symbolic representation of 𝒯φ can be directly given without the detour of explicit construction of the LTS. Because, the relation sat could be inductively constructed if we introduce corresponding new variables in el(φ). Subsequently, encodings of ΦΔψ+ or ΦΔη- could be naturally obtained from the underlying Boolean variables corresponding to states of automata connectives. Hence, the Boolean representation of Φρφ is obtained. And, encodings of other components are as routine.


## 3.1. The Tableaux of ETLl+f Formulae

Given anETLl+f formula φ, we first inductively define its elementary formula setel(φ) as follows.  (i)
el(⊤)=el(⊥)=∅.(ii)
el(p)=el(¬p)={p} for each p∈AP.(iii)
el(φ1∧φ2)=el(φ1∨φ2)=el(φ1)∪el(φ2).(iv)
el(○φ)=el(φ)∪{○φ}.(v)
Ifφ=𝒜q(φ1,…,φn) or φ=¬𝒜q(φ1,…,φn) and the states set of 𝒜 is Q, then
(1)el(φ)=⋃1≤k≤n‍el(φk)∪{○𝒜q′(φ1,…,φn)∣q′∈Q}.Hence, ifψ∈el(φ), then ψ is either an atomic proposition or a formula rooted at the next operator.Subsequently, we define the function sat, which maps each subformulaψ of φ to a set of members in 2el(φ). Inductively the following hold.  (i)
sat(⊤)=2el(φ); sat(⊥)=∅.(ii)
sat(p)={Γ⊆el(φ)∣p∈Γ} and sat(¬p)={Γ⊆el(φ)∣p∉Γ}.(iii)
sat(○ψ)={Γ⊆el(φ)∣○ψ∈Γ}.(iv)
sat(φ1∧φ2)=sat(φ1)∩sat(φ2) and sat(φ1∨φ2)=sat(φ1)∪sat(φ2).(v)
Suppose that𝒜=〈{a1,…,an},Q,δ,q,F〉.
(1)
If𝒜 is a looping acceptance automaton or a finite acceptance automaton and q∉F, then
(2)sat(𝒜q(φ1,…,φn))=⋃1≤k≤n‍(sat(φk)∩⋃q′∈δ(q,ak)‍sat(○𝒜q′(φ1,…,φn))).(2)
If𝒜 is a finite acceptance automaton and q∈F, then sat(𝒜q(φ1,…,φn))=2el(φ).(vi)
sat(¬𝒜q(φ1,…,φn))=2el(φ)∖sat(𝒜q(φ1,…,φn)).Recall the tableau construction for LTL [20], an “until subformula” would generate a fairness constraint to the tableau. Indeed, such a subformula corresponds to a “least-fixpoint subformula” if we translate the specification into a logic employing higher-order quantifiers, such as μ-calculus. Similarly, for ETLl+f, the PF- and NL-subformulae also impose fairness constraints. For this reason, we need to define the following two auxiliary relations before giving the tableau construction.For a PF-subformulaψ=𝒜(φ1,…,φn) of φ, where 𝒜=〈{a1,…,an},Q,δ,q,F〉, we define a relation Δψ+⊆(2el(φ)×2Q)×(2el(φ)×2Q) as follows: suppose that Γ,Γ′⊆el(φ) and P,P′⊆Q; then ((Γ,P),(Γ′,P′))∈Δψ+ if and only if the following hold.  (i)
WhenP≠∅, then, for each q∈P∖F, there exists some 1≤k≤n such that Γ∈sat(φk) and P′∩δ(q,ak)≠∅.(ii)
WhenP=∅, then q∈P′ if and only if Γ′∈sat(𝒜q(φ1,…,φn)) for each q∈Q.Likewise, for each NL-subformulaψ=¬𝒜(φ1,…,φn) of φ, we also define a relation Δψ-⊆(2el(φ)×2Q)×(2el(φ)×2Q). In detail, for any Γ,Γ′⊆el(φ) and P,P′⊆Q, we have ((Γ,P),(Γ′,P′))∈Δψ- if and only if the following hold.  (i)
WhenP≠∅, then, for each q∈P and 1≤k≤n, we have: Γ∈sat(φk) implies δ(q,ak)⊆P′.(ii)
WhenP=∅, then q∈P′ if and only if Γ′∉sat(𝒜q(φ1,…,φn)), for each q∈Q.We now describe the tableau construction forφ. Suppose that ψ1,…,ψm and ¬η1,…,¬ηn are, respectively, all the PF-subformulae and NL-subformulae occurring in φ then the tableau 𝒯φ is such an LTS 〈Sφ,ρφ,Iφ,Lφ,ℱφ〉, where:(i)
Sφ consists of tuples like 〈Γ;P1,…,Pm;R1,…,Rn〉, where Γ⊆el(φ) and each Pi (resp., Ri) is a subset of ψi’s (resp., ηi’s) connective’s state set.(ii)
For two statess=〈Γ;P1,…,Pm;R1,…,Rn〉 and s′=〈Γ′;P1′,…,Pm′;R1′,…,Rn′〉, (s,s′)∈ρφ if and only if the following three conditions hold.
(1)
Γ∈sat(○ψ) if and only if Γ′∈sat(ψ) for each ○ψ∈el(φ).(2)
((Γ,Pi),(Γ′,Pi′))∈Δψi+ for each 1≤i≤m.(3)
((Γ,Rj),(Γ′,Rj′))∈Δ¬ηj- for each 1≤j≤n.(iii)
Iφ={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Γ∈sat(φ)}.(iv)
Lφ(〈Γ;P1,…,Pm;R1,…,Rn〉)=Γ∩AP.(v)
ℱφ={Fi+∣1≤i≤m}∪{Fj-∣1≤j≤n}, where
(3)Fi+={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Pi=∅},Fj-={〈Γ;P1,…,Pm;R1,…,Rn〉∈Sφ∣Rj=∅}.The below two theorems (Theorems4 and 5) reveal the language property of ETLl+f tableaux. To remove the lengthiness, we here just provide the proof sketches, and rigorous proofs of them are postponed to the appendices.Theorem 4.
For eachπ∈(2AP)ω, if π∈ℒ(𝒯φ), then π⊨φ.Proof (sketch).
Just assume thatσ=s0s1⋯∈Sφω is the corresponding fair path of 𝒯φ such that π=Lφ(σ), where si=〈Γi;P1,i,…,Pm,i;R1,i,…,Rn,i〉. We may inductively prove the following claim.
“For eachψ∈sub(φ)∪el(φ), we have: Γi∈sat(ψ) implies π,i⊨ψ.”
Because we require thatΓ0∈sat(φ), hence we have π,0⊨φ.Theorem 5.
For eachπ∈(2AP)ω, if π⊨φ, then π∈ℒ(𝒯φ).Proof (sketch).
Suppose thatπ⊨φ; to show π∈ℒ(𝒯φ), we need to first construct an infinite state sequence σ=s0s1⋯∈Sφω guided by π (the detailed construction is given in Section A.2), and then we will subsequently show that σ is a fair path of 𝒯φ and π=Lφ(σ).The following theorem is immediate from Theorems4 and 5.Theorem 6.
The modelℳ violates the ETLl+f property φ if and only if ℒ(ℳ)∩ℒ(𝒯¬φ)≠∅, equivalently; there exists some fair path in ℳ×𝒯¬φ.Theorem 7.
For anETLl+f formula φ, its tableau 𝒯φ has at most 4|el(φ)| states.Proof.
Observe that a state should be of the form〈Γ;P1,…,Pm;R1,…,Rn〉. For Γ, there are 2|el(φ)| possible choices. Suppose that ψj=𝒜j(φ1,…,φk) (resp., ¬ηi=¬𝒜i(φ1′,…,φr′)) and the state set of 𝒜j is Qj (resp., 𝒜i with Qi′). According to the construction, each q∈Qj (resp., q∈Qi′) corresponds to a unique elementary formula ○𝒜jq(φ1,…,φk) (resp., ○𝒜iq(φ1′,…,φr′)), and such a mapping is an injection. Hence we have
(4)(∑1≤j≤m‍|Qj|+∑1≤i≤n‍|Qi′|)≤|el(φ)∖AP|.
Note that Pj⊆Qj (resp., Ri⊆Qi′), and hence we have |Sφ|≤(2|el(φ)|)2=4|el(φ|).


## 3.2. The Linear Semantic Encoding

Practically, a model’s state space is determined by the evaluation of a set of variables. Further, we may assume that each of them is a “Boolean variable” (which corresponds to a proposition belonging toAP), because every variable over finite domain could be encoded with several Boolean variables.Let𝒞=〈S,ρ,I,L,ℱ〉 be an arbitrary LTS, and we also assume that the corresponding variable set is V={p1,…,pn}; then each state s∈S uniquely corresponds to an assignment of such pis.If we uses(pi) to denote the value of pi at s, then each subset Z⊆S can be represented by a Boolean formula ΦZ over V. In detail, it fulfills
(5)s∈S⟺s⊩ΦZ,
where s⊩ΦZ means that ΦZ is evaluated to be true if we assign each pi with the value s(pi).LetV′={p1′,…,pn′}, and each binary relation λ⊆S×S also has a Boolean representation Φλ over the variable set V∪V′. That is,
(6)(s1,s2)∈λ⟺(s1,s2)⊩Φλ,
where (s1,s2)⊩Φλ  means that Φλ is evaluated to be true if we assign each pi with s1(pi) and assign each pi′ with s2(pi).Hence, all components ofℳ can be encoded: I and ρ can be represented by two Boolean formulae ΦI and Φρ, respectively; we subsequently create a Boolean formula ΦF for each F∈ℱ; note that the labeling function L is not concerned any longer, because the sates labeled with p can be captured by the Boolean formula p.For example, from Theorem7, we have that the symbolic representation of 𝒯φ requires 2×|el(φ)∖AP|  new Boolean variables—because variables in el(φ)∩AP can be shared with the encoding of the original model.A canonical Boolean encoding of fair path existence detection upon LTSs is presented in [22]: given a model 𝒞=〈S,ρ,I,L,ℱ〉 and a boundk∈ℕ, one may use the formula
(7)ΦI(0)∧⋀0≤i<kΦρ(i,i+1)∧⋁0≤ℓ≤k(Φρ(k,ℓ)∧⋀F∈ℱ⋁ℓ≤j≤kΦF(j)),
where ΦI(j) and ΦF(j) are, respectively, the Boolean formulae obtained from ΦI and ΦF by replacing each variable p with a new copy p(j), and Φρ(i,j) is obtained from Φρ by replacing each p with p(i) and replacing each p′ with p(j).It can be seen that this formula is satisfiable if and only if𝒞 involves a fair path of the form s0s1⋯sℓ-1(sℓ⋯sk)ω (call it is of the lasso shape). Since that ℒ(𝒞)≠∅ if and only if 𝒞 contains some lasso fair path (note that from each fair path we may derive another fair path of lasso shape), hence we may convert the fair path detection into the satisfiability problem of the above Boolean formula.However, a closer look shows that the size of such encoding is quadratic with the bound. To reduce the blow-up in size, we need to introduce the following new variables (the linearization can also be done with the syntactic fashion presented in [23, 24]. We would draw a comparison of these two approaches in Section 4.).  (1)
For each0≤ℓ≤k, we introduce a new variable rℓ. Intuitively, rℓ indicates that sℓ is a successor of sk.(2)
For each fairness constraintF∈ℱ and each 0≤ℓ≤k, we introduce a variable fF(ℓ), and this variable is evaluated to be true only if there is some ΦF(j) which is evaluated to true, where ℓ≤j≤k.And the new encoding (with the boundk∈ℕ) can be formulated as
(8)ΦI(0)∧⋀0≤i<kΦρ(i,i+1)∧⋁0≤ℓ≤krℓ,Ψ𝒞(k)=∧⋀0≤ℓ≤k(rℓ⟶(Φρ(k,ℓ)∧⋀F∈ℱfF(ℓ)))∧⋀F∈ℱ(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))∧(fF(k)⟶ΦF(k))(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))).Hence, both the number of variables and the size of this encoding are linear withk. Moreover, the following theorem guarantees the correctness of such encoding.Theorem 8.
ℒ
(
𝒞
)
≠
∅ if and only if  Ψ𝒞(k) is satisfiable for some k.Proof.
We begin with the “if” direction: suppose that the variable set is{p1,…,pm}; if there is some k such that Ψ𝒞k is evaluated to 1 (i.e., true) under the assignment e, then we denote si=(e(p1(i)),…,e(pm(i))) for each 1≤i≤m. Hence, each si is a state of 𝒞.  (i)
Since the truth value ofΦI(0) is 1 under e, then we have s0⊩ΦI(0); this implies that s0∈I.(ii)
For each0≤i<k, we have (si,si+1)⊩Φρ(i,i+1), and thus (si,si+1)∈ρ.(iii)
Because we have the conjunct⋁0≤ℓrℓ, then there is some 0≤ℓ≤k such that e(rℓ)=1. In the following, we fix this specific value ℓ for the discussion.(iv)
According to the constraintrℓ→(Φρ(k,ℓ)∧⋀F∈ℱfF(ℓ)), we have the following.
(1)
e(Φρ(k,ℓ))=1, which indicates that (sk,sℓ)∈ρ.(2)
For eachF∈ℱ, we have e(fF(ℓ))=1.(v)
For each fairness constraintF∈ℱ and 0≤i≤k, we now inductively show that “e(fF(i))=1 implies e(ΦF(j))=1 (alternatively, sj∈F) for some i≤j≤k.” First of all, it holds in the case of i=k, because we have the constraint f(k)→ΦF(k). In addition, the fact of “when i=c, it holds” can be immediately inferred from the hypothesis “when i=c+1, it holds,” according to the conjunct fF(i)→(fF(i+1)∨ΦF(i)). Since we have shown that e(fF(ℓ))=1, we can conclude that there exists some ℓ≤j≤k such that sj∈F.
The above shows thats0s1⋯sℓ-1(sℓ⋯sk)ω is a fair path of 𝒞, and hence ℒ(𝒞)≠∅.
Conversely, for the “only if” direction, it suffices to find somek and some assignment e evaluating Ψ𝒞(k) to be true. Since ℒ(𝒞)≠∅, there must exist some fair path of lasso shape in 𝒞. Without loss of generality, assume that σ=s0s1⋯sℓ-1(sℓ⋯sk)ω is such a path; just let k be this value, and we now illustrate how the assignment e is constructed.  (i)
For each variablepj and each i≤k, let e(pj(i))=si(pj). Since s0 is an initial state, according to the definition, we have e(ΦI(0))=1. Meanwhile, because each (si,si+1)∈ρ, we have that the conjunction ⋀0≤i≤kΦρ(i,i+1) is satisfied under e.(ii)
For each0≤i≤k, we let
(9)e(ri)={1,i=ℓ,0,i≠ℓ.
Then it can be seen that e(⋁0≤i≤kri)=1.(iii)
For eachF∈ℱ and each 0≤i≤k, we let
(10)e(fF(i))={1,ifthereissomej≥isuchthatsj∈F,0,otherwise.
Then it can be directly checked that the conjunct
(11)⋀F∈ℱ(⋀0≤i<k(fF(i)⟶(fF(i+1)∨ΦF(i)))∧(fF(k)⟶ΦF(k)))
is evaluated to be true under e.(iv)
Since(sk,sℓ)∈ρ, we have e(Φρ(k,ℓ))=1. Also note that σ is a fair path; then for each F∈ℱ there is some sj∈F, where ℓ≤j≤k. According to the previous definition, we can infer that e(⋀F∈ℱfF(ℓ))=1. Thus the conjunct
(12)⋀0≤i≤k(ri⟶(Φρ(k,i)∧⋀F∈ℱfF(i)))
is also satisfied under e (recall that we have assigned e(ri)=0 in the case of i≠ℓ).Thus, the formulaΨ𝒞(k) is satisfiable.For bounded model checking, an important issue is thecompleteness threshold, which is the specific value k such that we may declare ℒ(𝒞)=∅ in the case that Ψ𝒞(k) is not satisfiable, and we denote it by CT(𝒞) in this paper.Since we need only to concern about fair paths of the formσ1(σ2)ω, as pointed in [22], a possible candidate for the completeness threshold CT(𝒞) is
(13)DI(𝒞)+|ℱ|×D(𝒞),
where D and DI are, respectively, the diameter and the initialized diameter (cf. [22]). Since [22] just considers LTSs having only one fairness constraint, we here add the factor |ℱ|.Observe that the partσ2 must be enclosed in some SCC (i.e., strongly connected component) of 𝒞, and we may replace D(𝒞) with D(𝒮), where 𝒮 is the largest SCC that intersects all fairness constraints. Therefore, we may get a more compact upper bound of the completeness threshold.Then, for a given LTSℳ and the given ETLl+f formula φ, since we have shown that ℳ⊭φ if and only if ℳ×𝒯¬φ involves some fair path, we now just need to test if there is some k making Ψℳ×𝒯¬φ(k) satisfiable, where k≤CT(ℳ×𝒯¬φ).Remark 9.
In the case that𝒞=𝒞1×𝒞2, where 𝒞=〈S,ρ,I,L,ℱ〉 and 𝒞i=〈Si,ρi,Ii,Li,ℱi〉 for i=1,2, we have ΦI=ΦI1∧ΦI2, Φρ=Φρ1∧Φρ2, and Φℱ=Φℱ1∪Φℱ1, and in addition, the variable set of 𝒞 is just the union of the variable sets of 𝒞1 and 𝒞2.Remark 10.
Actually, for anETLl+f formula φ, the symbolic representation of 𝒯φ can be directly given without the detour of explicit construction of the LTS. Because, the relation sat could be inductively constructed if we introduce corresponding new variables in el(φ). Subsequently, encodings of ΦΔψ+ or ΦΔη- could be naturally obtained from the underlying Boolean variables corresponding to states of automata connectives. Hence, the Boolean representation of Φρφ is obtained. And, encodings of other components are as routine.


## 4. Experimental Results

To justify our idea, we have integrated (the tool is available athttps://sourceforge.net/projects/enusmv12/) the ETLl+f BMC algorithm into ENuSMV (Ver. 1.2). This tool is completely compatible with NuSMV [25], and it allows end-users to customize new temporal connectives by defining automata.For example, Figure1 illustrates how to declare a finite acceptance automata connective (to define a looping acceptance automata connective, just replace the keyword FIN with LOOP), namely, A. Since it has three states q1, q2, and q3 (where q1 is the initial state and q3 is an accepting state), then A[q1], A[q2], and A[q3] are also connectives—for example, A[q2] just replaces the initial state with q2. Subsequently, one may define ETLl+f specifications; for example,ETLSPECA(p,A[q2]  (q,p))is a proper declaration.Figure 1
An automata connective declaration in ENuSMV.In this redistribution, both BDD-based and bounded model checkings forETLl+f are supported. To perform (semantic encoding based) BMC, we need to use the command option bmc_tab.We have conducted some experiments to test the correctness and efficiency of our algorithm. In this paper, we are especially concerned with the following issues.(1)
The comparison of BDD-based symbolic model checking and bounded model checking.(2)
The overhead contrast in verifications ofETLf and ETLl+f upon both star-free and nonstar-free properties.(3)
The comparison of performances with syntactic/semantic BMC of LTL and semantic BMC ofETLl+f.To compare the efficiencies between BDD-based MC and BMC, we chose the (distributed mutual exclusion) DME circuit as the model (which involves a buggy design), as described in [3]. It consists of n cells for n users that want to have exclusive access to a shared resource. We conducted the experiment by describing the liveness property that “a request for using the resource will eventually be acknowledged” (with ETLl+f formula). The max bound are set to 100, and the comparative results are shown in Table 1, where “C.L." stands for the length of counterexample.Table 1
Comparative results of BDD-based and BMC approaches.
Cells
BDD
BMC
Time (s)
Memory (MB)
C.L.
Variables
Clauses
Time (s)
Memory (MB)
C.L.
5
170.56
68.32
78
3939
8126
13.50
34.98
39
6
513.06
209.17
84
4677
9620
29.14
42.37
39
7
2372.28
976.14
90
5415
11113
41.32
58.48
39
8
8074.05
1482.15
96
6154
12609
52.45
67.32
39
9
≥5 h
≥2 G
—
6892
14102
68.17
82.13
39
10
≥5 h
≥2 G
—
7630
15599
85.13
101.21
39As a previous work, we have implemented the symbolic model checking algorithm forETLf in ENuSMV 1.0. To justify that in general ETLl+f could be more effectively checked, we would make a comparison of BMC for ETLf and ETLl+f.To draw the comparison upon non-start-free regular properties, we use a “mod2n counter” as the model. The model consists of n “cells” bit_0,…,bit_n-1. Each cell is a (mod2) counter having an input carry_in and an output signal carry_out. These cells are connected in a serial manner; that is, bit_0’s carry_in is set to 1, and bit_i’s carry_in is connected to bit_i−1’s carry_out as described in Figure 2.Figure 2
The circuit of MOD2n counter.We, respectively, describe theperiodicity property that “bit_0 carries out at every even (except for 0) moment” with ETLf and ETLl+f. We set the time bound to 1 hour, and Table 2 provides the max bounds (together with related information) which can be handled by the SAT solver within the time bound. From it, we can see that a deeper search could be done when specifications are described with ETLl+f.Table 2
Comparison ofETLf and ETLl+f with periodicity properties.
Cells
ETL
f
ETL
l
+
f
Max bound
Memory (MB)
Variables
Clauses
Max bound
Memory (MB)
Variables
Clauses
10
11032
279.44
154461
1180431
13009
382.784
182140
1417990
11
5138
148.22
77084
631981
6037
173.59
90570
754461
12
3702
129.571
3702
518287
4316
143.802
69072
612888To compare the overhead ofETLf and ETLl+f upon star-free properties, we would first use the DME model to check the safety property: “no two cells will be simultaneously acknowledged.” The results are shown in Table 3, and the time bound is also set to 1 hour.Table 3
Comparison ofETLf and ETLl+f with safety properties.
Cells
ETL
f
ETL
l
+
f
Max bound
Memory (MB)
Variables
Clauses
Max-bound
Memory (MB)
Variables
Clauses
3
68
29.14
4002
8091
101
38.03
4958
9898
4
62
34.76
4864
9764
87
40.34
5712
11512
5
54
40.12
5170
10313
73
45.37
6072
12088At the same time, we can also compare the verification performances of the DME model upon the aforementioned liveness property that “each request will be acknowledged in the further.” Note that for this property, the verification could be accomplished within the given time bound, and a counterexample could be detected at the boundk=39. The comparative results are given in Table 4.Table 4
Comparison ofETLf and ETLl+f with liveness properties.
Cells
ETL
f
ETL
l
+
f
Time (s)
Variables
Clauses
Memory (MB)
Time (s)
Variables
Clauses
Memory (MB)
3
25.09
2400
4796
29.66
13.78
2340
4747
26.34
4
31.42
3120
6200
38.61
20.06
3042
6115
31.38
5
42.56
3840
7604
44.28
24.70
3744
7843
36.12The last group of experiments aims at comparing the efficiencies of (syntactic/semantic) LTL BMC andETLl+f BMC. First of all, for LTL BMC, we are also concerned with two types of encoding approaches.  (1)
The Syntactic Approach. We here adopt the linear incremental syntactic encoding proposed in [26]—to the best of our knowledge, this is the most effective syntactic encoding for full LTL.(2)
The Semantic Approach. ENuSMV 1.2 also supports semantic encoding for LTL—this is tailored from our linear encoding presented in Section 3.2.We still use the DME circuit as the model and the liveness property as specification; Table5 provides the experimental results on LTL BMC based on syntactic and semantic encodings. From that, we can see that, with semantic encoding, it tends to generate less clauses and tends to terminate earlier than that with the syntactic encoding, whereas the latter requires fewer variables.Table 5
Comparison of syntactic/semantic LTL BMC with liveness properties.
Cells
Syntactic LTL BMC encoding
Semantic LTL BMC encoding
Time (s)
Variables
Clauses
Memory (MB)
Time (s)
Variables
Clauses
Memory (MB)
3
9.34
2052
5474
32.66
8.59
2128
4291
24.79
4
16.71
2736
6806
35.74
10.87
2812
5623
28.44
5
24.06
3420
8138
37.02
15.90
3469
6955
32.28Meanwhile, we can also make a comparison between Tables4 and 5; we may find that the variable numbers of semantic ETL BMC and LTL BMC are almost at a fixed ratio—for this experiment, the ratio is 1.09 (approximately).


## 5. Concluding Remarks

The logicETLl+f is a variant of extended temporal logic, it employs both finite and looping acceptance automata connectives, and it can be considered a mixture of ETLl and ETLf. Thus, any omega-regular properties can be succinctly described with this kind of logic, particularly for safety and liveness properties.We have presented the semantic bounded model checking algorithm forETLl+f. The central part of this approach is the tableau construction. Meanwhile, we also illustrate how to give a linear BMC encoding for it. To justify it, we have implemented the presented algorithm (in ENuSMV 1.2). Experimental results show that ETLl+f could be more efficiently verified via BMC (in comparison to our previous implementation for ETLl+f).In this paper, verification ofETLr, namely, extended temporal logic using Büchi (alternatively, repeating) automata as connectives, has not been studied. This is partly because of the inherited difficulties of Büchi complementation [27]. Indeed, we may mimic the ranking complementing technique of Büchi automata [28–30]. However, this would cause an asymptotically quadratic blow-up of variable number in building the tableaux. Hence, a further work is about to study the semantic BMC encodings of ETLr.



---

*Source: 462532-2013-07-14.xml*