We consider two symbolic approaches to bounded model checking (BMC) of distributed time Petri nets (DTPNs). We focus on the properties expressed in Linear Temporal Logic without the neXt-time operator (LTL−X) and the existential fragment of Computation Tree Logic without the neXt-time operator (ECTL−X). We give a translation of BMC to SAT and describe a BDD-based BMC for both LTL−X and ECTL−X. The two translations have been implemented, tested, and compared with each other on two standard benchmarks. Our experimental results reveal the advantages and disadvantages of both the approaches.
Verification of time dependent systems is a very active field of research. Many
efficient approaches have been put forward for the verification of timed automata
[
Bounded model checking (BMC) is an efficient verification method using a
model truncated up to a specific depth only. In turn, SAT-based BMC
verification consists in translating a model checking problem solvable on a fraction of a
model into a test of propositional satisfiability, which is then performed using a
SAT-solver [
In this paper we investigate bounded model checking (BMC) approaches to verification of Distributed Time Petri Nets with discrete semantics, based on both SAT and BDD translations. There are several decisions taken that aim at making the verification of TPNs as efficient as possible. Below, we discuss them in detail to motivate clearly our approach. First of all, we believe that BMC is one of the main practical approaches, which can be used in case of dealing with huge or infinite state spaces. We motivate this point of view by comparing our experimental results with these of Tina, which operate on full state spaces. Clearly, BMC is restricted to verifying existential properties only, but it allows for tackling bounded models of large systems, whereas other approaches suffer from lack of memory.
Our second choice consists in dealing with distributed TPNs rather than with just 1-safe TPNs. The reason is that a representation of a global state contains only one clock for each process rather than one clock for each transition, which makes the encoding and the verification much more efficient. Another choice is related to the semantics. In this paper we investigate discrete semantics as we believe that in this case model checking is again more efficient. However, independently we are working on extending our approach to the dense semantics as we are aware that this is also a very interesting issue. Since there are several discrete semantics, we consider for each translation these which can be applied.
As to the temporal properties, we start with defining CTL∗−X, but restrict ourselves two its two subsets CTL−X and LTL−X, as these sublanguages allow for optimising the translations to SAT and BDDs. The languages do not contain the next step operator X as we are dealing with time systems, in which, for some discrete semantics, the next step may be not definable.
Next, we need to motivate our translations to SAT and BDDs. We are aware
of the fact that there has been a tremendous speed-up due to applying the
saturation technique [
The above discussion motivates all the choices made in our paper and leads us to the main result, which is offering and comparing two symbolic BMC approaches for DTPNs. We show that for existential properties our BMC is much more efficient than Tina. We also compare efficiency of BMC depending on whether it is based on a translation to SAT or to BDD.
The main contribution of this paper is thus the combination of the three
issues, as BMC has been studied, with both BDDs and, especially, SAT, but
mostly for standard untimed models, while discrete time Petri nets have been
studied with BDDs and extensions (e.g., [
To our best knowledge, no BMC method supporting ELTL−X and ECTL−X
for time Petri nets has been defined so far, although some solutions for untimed
Petri nets exist [
The rest of the paper is organised as follows. Section 2 presents logics LTL−X and CTL−X. Section 3 introduces time Petri nets. SAT-based BMC for ELTL−X and ECTL−X is described in Section 4, whereas BDD-based BMC for these logics is in Section 5. Sections 6 and 7 contain respectively experimental results and concluding remarks. 2
We start with defining the logic CTL∗−X, which can express both linear- and branching-time properties. Then, we introduce variants of linear time temporal logic (LTL−X) as well as of branching time temporal logic (CTL−X) as sublogics of CTL∗−X. All the considered logics do not contain the next step operator X, which is reflected in their acronyms by −X.
Let P V be a set of propositional variables such that {true, f alse} ⊆ P V , and ℘ ∈ P V . The language of CTL∗−X is given as the set of all the state formulae ϕs (interpreted at states of a model), defined using path formulae ϕp (interpreted along paths of a model), by the following grammar:
ϕs := ℘ | ¬ϕs | ϕs ∨ ϕs | Aϕp ϕp := ϕs | ¬ϕp | ϕp ∨ ϕp | ϕp Uϕp | ϕp Rϕp In the above A (’for All paths’) is a path quantifier, whereas U (’Until’), and R (’Release’) are state operators. Further, the following standard abbreviations def def are used in writing CTL∗−X formulae: ϕs ∧ ϕs = ¬(¬ϕs ∨ ¬ϕs ), ϕp ∧ ϕp = ¬(¬ϕp ∨ ¬ϕp ), Eϕp d=ef ¬A(¬ϕp ), Gϕp d=ef f alseRϕp , and Fϕp d=ef trueUϕp .
Next, we define several sublogics of CTL∗−X including variants of LTL−X as well as of CTL−X. Although a standard model for LTL−X is a path, for verification aims the logic is typically interpreted over all the paths of a Kripke model. So, two semantics are possible depending on whether a formula holds at all the paths or at some path of a model. Since we need to distinguish between these two semantics (in order to specify counterexamples), we find it useful to do it already at the level of the language by defining the universal ( ALTL−X) and the existential (ELTL−X) versions of the logic. In the literature on the verification of linear time properties, if this distinction is not necessary, then ALTL−X is typically called LTL−X.
ALTL−X (ELTL−X) is the fragment of CTL∗−X in which only the formulae of the form Aϕp (Eϕp , respectively) are allowed, where ϕp is a path formula which does not contain the path quantifiers A, E.
CTL−X is the fragment of CTL∗−X in which the syntax of path formulae is restricted such that each state operators must be preceded by a path quantifier (i.e., the modalities A, E, U, R can only appear paired in the combinations AU, EU, AR, ER).
ACTL−X (ECTL−X) is the fragment of CTL−X such that the formulae are restricted to the positive boolean combinations of A(ϕUψ) and A(ϕRψ) (E(ϕUψ) and E(ϕRψ), respectively). Negation can be applied to propositions only.
A model for CTL∗−X is a Kripke structure M = (L, S, s0, →, V ), where L is a set of labels, S is a set of states, s0 ∈ S is the initial state, → ⊆ S × L × S is a total successor relation (i.e., (∀s ∈ S)(∃s0 ∈ S)(s→s0)), and V : S −→ 2P V is a valuation function.
In our paper we assume the standard semantics of CTL∗−Xwhich can be found
in several papers, among others in [
Time Petri Nets Let IN denote the set of natural numbers. We start with a definition of time Petri nets: Definition 1. A time Petri net (TPN) is a tuple N = (P, T, F, m0, Ef t, Lf t), where P = {p1, . . . , pnP } is a finite set of places, T = {t1, . . . , tnT } is a finite set of transitions, F ⊆ (P × T ) ∪ (T × P ) is the flow relation , m0 ⊆ P is the initial marking of N , and Ef t : T → IN, Lf t : T → IN ∪ {∞} are functions describing the earliest and the latest firing time of the transition; where for each t ∈ T we have Ef t(t) ≤ Lf t(t).
For a transition t ∈ T we define its preset •t = {p ∈ P | (p, t) ∈ F } and postset t• = {p ∈ P | (t, p) ∈ F }, and consider only the nets such that for each transition the preset and the postset are nonempty. We need also the following notations and definitions: – a marking of N is any subset m ⊆ P ; – a transition t ∈ T is called enabled at m (m[ti for short) if •t ⊆ m and t • ∩(m \ •t) = ∅; and leads from m to m0, if it is enabled at m, and m0 = (m \ •t) ∪ t•. The marking m0 is denoted by m[ti as well, if this does not lead to misunderstanding; – en(m) = {t ∈ T | m[ti} is the set of all the transitions enabled at the marking m; – a marking m ⊆ P is reachable if there exists a sequence of transitions t1, . . . , tl ∈ T and a sequence of markings m0, . . . , ml such that m0 = m0, ml = m, and for each i ∈ {1, . . . , l} ti ∈ en(mi−1) and mi = mi−1[tii; – a marking m concurrently enables two transitions t, t0 ∈ T if t ∈ en(m) and t0 ∈ en(m \ •t); – a net is sequential if no reachable marking of N concurrently enables two transitions.
It should be mentioned that the time Petri nets defined as above are often called
1-safe in the literature. In this work we consider a subclass of TPNs – distributed
time Petri nets (DTPNs) [
Notice that the function Ef ti1 (Lf ti1 ) coincides with Ef ti2 (Lf ti2 , resp.) for the joint transitions of each two processes i1 and i2. The interpretation of such a system is a collection of sequential, nondeterministic processes with communication capabilities (via joint transitions).
In what follows, we consider DTPNs only, assume that their initial markings
contain exactly one place of each of the processes of the net, and that all their
processes are state machines (i.e., for each i ∈ I and each t ∈ Ti, it holds
| • t| = |t • | = 1). This implies that in any marking of N there is exactly one
place of each process. It is important to mention that a large class of distributed
nets can be decomposed to satisfy the above requirement [
Concrete State Spaces and Models
The current state of the net is given by its marking and the time passed since
each of the enabled transitions became enabled (which influences the future
behaviour of the net). In our work we assume a discrete-time semantics of DTPNs,
i.e., consider integer time passings only (cf. [
For δ ∈ IN, let clock + δ denote the function given by (clock + δ)(i) = clock(i) + δ, and let (m, clock) + δ denote (m, clock + δ). The states of N can change when the time passes or a transition fires. In consequence, we introduce a labelled timed consecution relation →c⊆ Σ × (T ∪ IN) × Σ given as follows: – In a state σ = (m, clock) a time δ ∈ IN can pass leading to a new state δ σ0 = (m, clock + δ) (denoted σ →c σ0) iff for each t ∈ en(m) there exists i ∈ IV(t) such that clock(i) + δ ≤ Lf t(t) (time-successor relation); – In a state σ = (m, clock) a transition t ∈ T can fire leading to a new state t σ0 = (m0, clock0) (denoted σ →c σ0) if t ∈ en(m), for each i ∈ IV(t) we have clock(i) ≥ Ef t(t), and there is i ∈ IV(t) such that clock(i) ≤ Lf t(t). Then, m0 = m[ti,and for all i ∈ I we have clock0(i) = 0 if i ∈ IV(t), and clock0(i) = clock(i) otherwise (action-successor relation).
Intuitively, the time-successor relation does not change the marking of the net, but increases the clocks of all the processes, provided that no enabled transition becomes disabled by passage of time (i.e., for each t ∈ en(m) the clock of at least one process involved in the transition does not exceed Lf t(t)). Firing of a transition t takes no time – the action-successor relation does not increase the clocks, but only sets to zero the clocks of the involved processes (note that each of these processes contains exactly one input and one output place of t, as the processes are state machines); and is allowed provided that t is enabled, the clocks of all the involved processes are greater than Ef t(t), and there is at least one such process whose clock does not exceed Lf t(t).
We define a timed run of N starting at a state σ0 ∈ Σ (σ0-run) as a maximal a0 a1 sequence of concrete states, transitions, and time passings ρ = σ0 →c σ1 →c a2 σ2 →c . . ., where σi ∈ Σ and ai ∈ T ∪ IN for all i ∈ IN. An alternating run is a timed run in which ai ∈ IN when i is even, and ai ∈ T when i is odd. A non-alternating run is a timed run with ai ∈ T ∪ (IN \ {0}) for all i. Given a set of propositional variables P V , we introduce a valuation function Vc : Σ → 2P V which assigns the same propositions to the states with the same markings. We assume the set P V to be such that each q ∈ P V corresponds to exactly one place p ∈ P , and use the same names for the propositions and the places. The function Vc is defined by p ∈ Vc(σ) ⇔ p ∈ m for each σ = (m, ·). The structure Mc(N ) = (T ∪ IN, Σ, σ0, →c, Vc) is called a concrete (discrete-timed) model of N . 3.2
A Model for CTL∗−XVerification of DTPNs The concrete model Mc(N ) = (T ∪ IN, Σ, σ0, →c, Vc) for a DTPN N defined in Section 3 involves timed steps of arbitrary length. However, it can be proven that without loss of generality one can consider a model with a restricted set of timed labels, and of restricted values of the clock function. Let cmax(N ) denote the greatest finite value of Ef t and Lf t of the net N , cm1 denote the value cmax(N ) + 1, and CN be the set of natural numbers from the interval [0, cm1]. Next, for a function f : T → IN and a ∈ IN, let f |a denote the function given by f |a(t) = f (t) if f (t) ≤ a, and f |a(t) = a otherwise. Let clocks : I → CN denote the function which for each index i of a process of N gives the time either elapsed since the marked place of this process became marked most recently, or “frozen” on the value cm1 if the time elapsed since the marked place becomes marked exceeded cmax(N ). Let σ|cm1 , for σ = (m, clock) ∈ Σ, be the state (m, clocks) with clocks = clock|cm1 . Moreover, for δ ∈ IN, let clocks ⊕ δ denote the function given by (clocks ⊕δ)(i) = clocks(i)+δ if clocks(i)+δ ≤ cm1, and (clocks ⊕δ)(i) = cm1 otherwise. The reduced (discrete-timed) model for DTPN N is defined as follows: Mcc(N ) = (T ∪ CN , Σs, σ0, →s, Vs), where Σs = {σ|cm1 | σ ∈ Σ}, Vs is given by Vs(σ|cm1 ) = Vc(σ), and the relation →s⊆ Σs × (T ∪ CN ) × Σs is defined by – in a state σs = (m, clocks) a time δ ∈ CN can pass leading to a new state δ σs0 = (m, clocks ⊕ δ) (denoted σs →s σs0) iff for each t ∈ en(m) there exists i ∈ IV(t) such that clocks(i) ⊕ δ ≤ Lf t(t), – a transition t ∈ T can fire in a state σs = σ|cm1 leading to a state σs0 (denoted σs →s σs0) iff σ →tc σ0 for some σ0 ∈ Σ s.t. σs0 = σ0|cm1 .
t In order to show that Mcc(N ) can replace Mc(N ) in CTL∗−X verification we shall prove the following lemma: Lemma 1. For a given DTPN N the models Mc(N ) = (T ∪ IN, Σ, σ0, →c, Vc) and Mcc(N ) = (T ∪ CN , Σs, σ0, →s, Vs) are bisimulation equivalent. The proof can be found in the appendix. In the proof we use an “intermediate” model Mfc(N ) = (T ∪ CN , Σ, σ0, →r, Vc) with →r⊆ Σ × (T ∪ CN ) × Σ given by – in a state σ = (m, clock) a time δ ∈ CN can pass leading to a new state δ σ0 = (m, clock + δ) (denoted σ →r σ0) iff for each t ∈ en(m) there exists i ∈ IV(t) such that clock(i) + δ ≤ Lf t(t), t – a transition t ∈ T can fire in a state σ leading to a state σ0 (σ →r σ0) iff σ →tc σ0, (i.e., the model which differs from Mcc(N ) in such a way that the values of the clock function are not restricted to cm1) which is bisimulation equivalent to Mc(N ). Further, we define the following equivalence relation, which is used in the next section to define a SAT-based BMC method.
Definition 3. Let σ = (m, clock) and σ0 = (m0, clock0) be two states of a DTPN N (σ, σ0 ∈ Σ). The states σ, σ0 are ?-equivalent (denoted σ '? σ0) iff m = m0 and ∀t∈en(m)[(mini∈IV(t) clock(i) = mini∈IV(t) clock0(i) ∧ mini∈IV(t) clock(i) ≤ cmax(N )) ∨ (mini∈IV(t) clock(i) > cmax(N ) ∧ mini∈IV(t) clock0(i) > cmax(N ))]. The following lemma shows that the equivalence preserves the behaviours of the net. Its proof can be found in the appendix.
Lemma 2. Let σ, σ0 ∈ Σ be ?-equivalent. Thus, for any l ∈ T ∪ IN we have: – if σ →lc σ1 for some σ1 ∈ Σ then there is σ10 ∈ Σ s.t. σ0 →lc σ10 and σ1 '? σ10, – if σ0 →lc σ10 for some σ10 ∈ Σ then there is σ1 ∈ Σ s.t. σ →lc σ1 and σ10 '? σ1. 4
BMC is a verification technique whose main idea consists in considering a model truncated up to a specific depth. Thus, BMC is mostly used to find counterexamples for the properties expressed in “universal” logics (in our case ACTL−X and ALTL−X), or to prove that properties expressed in “existential” logics (ECTL−X, ELTL−X) hold.
The BMC method used in our paper is based on the BMC method for the
existential fragment of CTL∗−X (ECTL∗−X) [
How to define the formula [Mfc(N )ϕ,σ0 ]k in the DTPN settings we show in the next subsection. Note however that for a given DTPN N , the formula [Mfc(N )ϕ,σ0 ]k can be implemented either using the model Mfc(N ) or using Mcc(N ). We have chosen Mfc(N ) in order to simplify the implementation. It should be explained that although in Mfc(N ) there is no upper bound on the values of clocks, restricting the lengths of the time steps allows to bound the values of clocks on k-paths by a value depending on k and cmax(N ). The definition of the formula [ϕ]M0 depends on whether ϕ is in ECTL−X or in ELTL−X, and whether considered k-paths are, or are not loops; a k-path πk = (σ0, σ1, . . . , σk) is called a (k, l)-loop, if – σk '? σl for some 0 ≤ l < k (the non-alternating semantics). – σk '? σl for some 0 ≤ l < k, and either both k and l are odd or they are both even (the alternating semantics).
The difference in the above definitions follows from the fact that in the alternating semantics the looping runs need to preserve the alternating structure when "unfolded", while in the non-alternating semantics their stucture is preserved without any additional conditions. Using '? instead of the standard equality of states follows from the fact that for the further possible behaviours of the net at a given state only the minimal values of the clocks of the processes involved in the enabled transitions are important.
A k-path πk is called a loop, if it is (k, l)-loop for some l ∈ {0, . . . , k − 1}. In
this paper we assume the definitions of [ϕ]M0 that can be found, respectively, in
[
Let w, w0 be two global state variables. We define the following auxiliary propositional formulae: • Iσ(w) is a formula that encodes the state σ of the model Mfc(N ), i.e., σ[i] = 1 is encoded by w[i], and σ[i] = 0 is encoded by ¬w[i]. • T S(w, w0) (T S0(w, w0)) is a formula over w and w0 which is true for two δ valuations σw of w and σw0 of w0 iff σw →r σw0 , for δ ∈ CN (δ ∈ CN \ {0}, respectively). It encodes the time-successor relation of Mfc(N ). • AS(w, w0) is a formula over w and w0 which is true for two valuations σw t of w and σw0 of w0 iff σw →r σw0 , for t ∈ T . It encodes the action-successor relation of Mfc(N ).
The propositional formula [Mfcϕ,σ0 ]k is defined as follows: [Mfcϕ,σ0 ]k := Iσ0 (w0,0) ∧
R(wi,j, wi+1,j) fk(ϕ)−1 k−1 ^ ^ j=0 i=0 where wi,j for 0 ≤ i ≤ k and 0 ≤ j < fk(ϕ) are global state variables, and (a) R(wi,j, wi+1,j) := T S(wi,j, wi+1,j) when i is even, and R(wi,j, wi+1,j) :=
AS(wi,j, wi+1,j) when i is odd (the alternating semantics), or (b) R(wi,j, wi+1,j) := T S0(wi,j, wi+1,j) ∨ AS(wi,j, wi+1,j) (the non-alternating semantics). 5 Notice that we distinguish between states of Σ encoded as sequences of 0’s and 1’s (we refer to these as valuations of w), and their representations in terms of propositional variables w[i]. Note that if ϕ is an ELTL−X formula, then fk(ϕ) = 1, and the above definition is equivalent to the following one: [Mfcϕ,σ0 ]k := Iσ0 (w0,0) ∧ Vik=−01 R(wi,0, wi+1,0). 5
Binary decision diagrams (BDDs) [
To introduce a BDD-based bounded model checking method, we start with
describing ECTL−X in terms of sets of reachable states at which the given
formula holds [
Let S be a finite set and τ : 2S −→ 2S a monotone function, i.e., X ⊆ Y implies τ (X) ⊆ τ (Y ) for all X, Y ⊆ S. Let τ i(X) be defined by τ 0(X) = X and τ i+1(X) = τ (τ i(X)). We say that X0 ⊆ S is a fixed point of τ if τ (X0) = X0. It can be proven that if τ is monotone, S is a finite set and |S| is a number of its elements, then there exist m, n ≤ |S| such that τ m(∅) is the least fixed point of τ (denoted by μX.τ (X)) and τ n(S) is the greatest fixed point of τ (denoted by νX.τ (X)).
Let M = (L, S, s0, →, V ) be a model, and SR ⊆ S a set of all the reachable states of the model M . For X ⊆ SR, let pre∃(X) = {s ∈ SR | (∃s0 ∈ X)(∃l ∈ L) s →l s0} be a set of all the reachable states from which there is a transition to some state in X. Further, we denote the set of all the reachable states of the model M at which ϕ holds by [[M, ϕ]] or by [[ϕ]], if M is implicitly understood. For ECTL−X formulae ϕ and ψ we define the following sets: [[true]] d=ef SR, [[℘]] d=ef {s ∈ SR | ℘ ∈ V (s)}, [[¬ϕ]] d=ef SR \ [[ϕ]], [[ϕ ∧ ψ]] d=ef [[ϕ]] ∩ [[ψ]], [[ϕ ∨ ψ]] d=ef [[ϕ]]∪[[ψ]]. The remaining operators can be defined as fixed points in the following way: [[EGϕ]] d=ef νX.[[ϕ]] ∩ pre∃(X), [[E[ϕUψ]]] d=ef μX.[[ψ]] ∪ ([[ϕ]] ∩ pre∃(X)).
To define the sets corresponding to ELTL−X formulae we proceed as follows.
Let M = (L, S, s0, →, V ) be a model, and ϕ an ELTL−X formula. We begin
with constructing the tableau for ϕ, as described in [
Before describing the BDD-based bounded model checking method, we first define a submodel. Namely, for the model M = (L, S, s0, →, V ) and U ⊆ S such that s0 ∈ U , we define a submodel M |U = (L0, U, s0, →0, V 0), where: L0 = {l ∈ L | (∃s, s0 ∈ U ) s →l s0}, →0 = {s →l s0 | s, s0 ∈ U }, V 0 : U −→ 2P V is defined by V 0(s) = V (s) for all s ∈ U . As the method can be applied to BMC of both ECTL−X and ELTL−X, we do not distinguish between ECTL−X and ELTL−X formulae, and in what follows, by ϕ we understand either an ECTL−X formula or an ELTL−X formula.
Let M = (L, S, s0, →, V ) be a model. For any set X ⊆ S we define the set of successors of all the states in X by X; d=ef {s0 ∈ S | (∃s ∈ X)(∃l ∈ L) s →l s0}. The complete set of the reachable states is obtained by computing the least fixed point μReach.{s0} ∪ Reach ∪ Reach;. With each iteration, when the set Reach is extended with new states, i.e., with the set Reach;, the verified formula is checked in the submodel M |Reach. The loop terminates and the algorithm returns true, if the initial state s0 is in the set of states of the obtained submodel at which ϕ holds. The search continues until no new states can be discovered from the states in Reach, i.e., the fixed point is reached. When we obtain the complete set of reachable states, and a path from the initial state on which ϕ holds could not be found in any of the obtained submodels, the algorithm terminates with f alse.
BDD-based Verification of DTPNs In order to verify a DTPN using BDDs
first we need to translate its underlying reduced model into boolean formulae that
are encoded with BDDs. Let Mcc(N ) = (T ∪ CN , Σs, σ0, →s, Vs) be a model of
a given DTPN N = (P, T, F, m0, Ef t, Lf t). We assume that every state σ ∈ Σs
can be encoded as a bit vector (σ[
Let w, w0 be two global state variables. We define the following boolean formulae that are used in the encoding: • Iσ(w) is a formula that encodes the state σ of the model Mc(N ), i.e., σ[i] = 1 is encoded by w[i], and σ[i] = 0 is encoded by ¬w[i]. • T S(w, w0) is a formula over w and w0 which is true for two valuations σw of w δ and σw0 of w0 iff σw →s σw0 , for δ ∈ CN \ {0}. It encodes the time-successor relation of Mcc(N ). • ASt(w, w0), where t ∈ T , is a formula over w and w0 which is true for two valuations σw of w and σw0 of w0 iff σw →ts σw0 . It encodes the actionsuccessor relation of Mcc(N ) for the transition t ∈ T . • T (w, w0) = Wt∈T ASt(w, w0) ∨ T S(w, w0) is a formula over w and w0 which is true for two valuations σw of w and σw0 of w0 iff σw →s σw0 . It encodes the transition relation of Mcc(N ).
Notice that due to the fact that an implementation of the alternating semantics would be inefficient in the case of the BDD-based method, we apply only the non-alternating semantics.
In our implementation we use the order of variables suggested in [
Experimental Results In this section we consider two scalable DTPNs which we use to evaluate the performance of our SAT- and BDD-based BMC algorithms, as well as of the tool Tina, for the verification of several properties expressed in ECTL−X and ELTL−X. The evaluation is given by means of the running time and the consumed memory. Graphs representing the benchmarks described below can be found at the webpage of VerICS – http://verics.ipipan.waw.pl/.
The first benchmark we consider is the Generic Timed Pipeline Paradigm
(GTPP) Petri net model [
The second benchmark of our interest is the DTPN model for Fischer’s mutual exclusion protocol (Mutex). The model consists of n time Petri nets, each one modelling a process, plus one additional net used to coordinate the access of processes to their critical sections Mutual exclusion means that no two processes are in their critical sections at the same time. The preservation of this property depends on the relative values of the time-delay constants δ and Δ. In particular, Fischer’s protocol ensures mutual exclusion iff Δ < δ. This DTPN can be scaled in the number of processes.
The GTPP Petri net model, where all the intervals are set to [
iynBM 1111802460000000000 SSBBBBAADDDDTTDDDD,,,,,,nafrppieloxaatoenerrttrr-diidnattiiealooottrernniednriinndnegggars,,tienfriemxgoe.srddeeomrre.dder r o em 600 M 400 200
0 0
The above systems have been carefully selected in order to reveal the advantages and disadvantages of both SAT- and BDD-based BMC approaches.
Memory usage for GTPP, ECTLX formula ψ1
Total time for GTPP, ECTLX formula ψ1 10 15 Number of processes 20 25 0 5
10 15 Number of processes 20 25
For the SAT-based BMC method two semantics are implemented: the alternating and the non-alternating one. The results obtained for the non-alternating semantics are superior to those for the alternating one in the following two cases: (1) the length of the witness and the number of k-paths depends on the number of components of the considered system; (2) the number of k-paths is constant and their lengths are at least twice as long in the alternating semantics as in the non-alternating one. On the other hand, the non-alternating semantics is inferior to the alternating one in the case when the length of k-paths is independent of the number of components of the considered system and their number is independent of their lengths. Further, the assumed time limit (1800s) prefers the non-alternating semantics, i.e., if a larger time limit than 1800s is set, then for the alternating semantics much more components of a given system can be verified than for the non-alternating one (see Mutex and the formula ψ1). The reason is that the SAT-based BMC method for systems with a large number of components (for the non-alternating semantics) generates the propositional formulae that are more complicated than in case of the alternating semantics. This results in the fact that the memory consumed by the SAT-solver is significantly larger for the set of clauses generated in case of the non-alternating semantics, therefore only smaller systems can be model-checked.
The method based on BDDs is implemented with reordering, and with the
fixed interleaving order of the BDD variables. The reordering is performed by
the Rudell’s sifting algorithm available in the implementation of CUDD library.
Moreover, we also use partitioned transition relations. In the case of GTPP, the
BDD-based method is remarkably superior to the SAT-based method in terms
of the verification times and the consumed memory for the tested formulae. The
reason is the substantial number of k-paths in SAT-BMC, which causes a larger
memory consumption and longer running times in comparison with the
BDDbased method. Where the length of the witness is constant regardless of the
number of the processes (i.e., in Mutex for ψ1 and the corresponding formula
ψ3), the SAT-based method is more efficient than the BDD-based one. Our
partitioning of the transition relation does not reduce noticeably the memory
usage, although in most of the considered cases the method benefits from the
reordering of the BDD variables. The BDD-based method deals better with the
increasing length of the witness when scaling in the number of processes or nodes.
In the case of Mutex, our experiments revealed that the method based on BDDs
is more efficient for small and medium models, but it consumes more memory.
The above observations seem to be consistent with other existing comparisons
of SAT versus BDD [
We compare also our results with those of Tina, however, as Tina does not support a verification of ECTL−X formulae, the results only for ELTL−X are taken into account. Unsurprisingly, as Tina is a non-bounded model checker, the results are inferior to the results of our BMC methods. Although Tina seems to perform well in the case of ψ4 for Mutex, it suffers from a significant increase of the memory usage for 8 processes and is unable to verify more than 9 processes.
All the benchmarks can be found at the webpage of VerICS, together with an
instruction how to reproduce our results. For the tests we have used a computer
running Linux 2.6.38 with two Intel Xeon 2.00GHz processors and 4 GB of
memory. Both the algorithms have been implemented in C++. The BDD-based
method uses CUDD [
Conclusions In this paper we have presented two different approaches for bounded model checking of DTPNs: via a reduction to SAT and via BDDs. The two methods have been tested and compared to each other on two standard benchmarks. The specifications were given in the ECTL−X and ELTL−X languages. Additionally we have compared our results with those obtained using the tool Tina. The experimental results revealed that SAT-based BMC and BDD-based BMC are complementary solutions to the BMC problem, as their performance depends
Memory usage for Mutex, ECTLX formula ψ1
Total time for Mutex, ECTLX formula ψ1 0 10 20 30 40 50 60 70 80 7
SAT-BMC BDD-BMC alternating sem. non-alternating sem. non-alternating sem. Formula (k, fk(ψ)) (k, fk(ψ)) the number of iterations GPP, ψ1 (4 · n + 6, 4 · n + 8) (2 · n + 3, 2 · n + 5) 2 · n + 2 GPP, ψ2 (4 · n + 6, 1) (2 · n + 3, 1) 2 · n + 2 Mutex, ψ1 (8, 10) (4, 6) 4 Mutex, ψ2 (2 · n + 8, 2) (n + 2, 2) 2 · n + 1 Mutex, ψ3 (14, 1) (6, 1) 5 Mutex, ψ4 (4 · n + 8, 1) (2 · n + 2, 1) 2 · n + 1 Table 1. The sizes of the witnesses. The number of nodes/processes is denoted by n. on the system and the property that are verified. The approach based on BDDs scales better than the SAT-based one, when witnesses are found at small and constant depths with respect to the scaling parameter. From two of the considered semantics for SAT-BMC, the non-alternating one is more efficient.
The paper is the first one to present bounded model checking methods for verifying ECTL−X and ELTL−X properties of time Petri nets. The encodings that are used in the SAT-based method, are applied in the context of BMC and DTPNs for the first time. Similarly, the verification methods for ECTL−X and ELTL−X used in BDD-BMC have not been considered before in the bounded model checking of time Petri nets. The dependence on the length of the witnesses, and the performance of the two BMC methods for DTPNs has not been observed before as well.
As this is our early attempt at BDD-based bounded model checking, it suffers from some weaknesses. In particular, the encoding of the transition relation could be improved, and some more recent developments in BDD-based symbolic model checking could be applied.
In our future work we are going to consider dense semantics and more general time Petri nets.
A
Appendix: Models for DTPNs - Proofs In order to show that Mcc(N ) can replace Mc(N ) in CTL∗−Xverification (i.e., to prove Lemma 1) we shall prove the following lemma: Lemma 3. For a given distributed time Petri net N the models Mc(N ) = (T ∪ IN, Σ, σ0, →c), Vc and Mfc(N ) = (T ∪ CN , Σ, σ0, →r, Vc) are bisimulation equivalent.
Proof. We shall show that the relation R = {((m, clock), (m0, clock0)) | m = m0 ∧∀(i ∈ I s.t. clock(i) ≤ cmax(N )) clock(i) = clock0(i) ∧ ∀(i ∈ I s.t. clock(i) > cmax(N )) clock0(i) > cmax(N )} is a bisimulation. It is easy to see that σ0Rσ0, and the valuations of the related states are equal (due to equality of their markings). Consider σ = (m, clock) ∈ Σ and σ0 = (m, clock0) ∈ Σ such that σRσ0. – if σ →δc σ1, where δ ∈ IN, then for each t ∈ en(m) there exists i ∈ IV(t) s.t. clock(i) + δ ≤ Lf t(t). Consider the following cases: • if en(m) contains at least one transition t with Lf t(t) < ∞, then this implies that δ ≤ cmax(N ). In this case consider δ0 = δ; it is easy to see from the definition of R that for any t ∈ en(m) s.t Lf t(t) < ∞ if in σ for some i ∈ I we have clock(i)+δ ≤ Lf t(t), then in σ0 clock0(i)+δ0 ≤ Lf t(t) holds as well, and therefore the time δ0 can pass at σ0, leading to the state σ0 + δ0, which satisfies (σ + δ)R(σ0 + δ0) in an obvious way. • if en(m) contains no transition t with Lf t(t) < ∞, then we can have either δ < cm1 or δ ≥ cm1, where by cm1 we mean the value cmax(N )+1. In the first case consider δ0 = δ; it is obvious that such a passage of time at σ0 disables no transition and is allowed therefore; it is also easy to see that (σ + δ)R(σ0 + δ0). In the case δ ≥ cm1 assume δ0 = cm1. Again, it is obvious that such a passage of time at σ0 disables no transition and due to this is allowed, and that in both the states σ + δ and σ0 + δ0 we have clock(i) > cmax(N ) for all i ∈ I, and therefore (σ + δ)R(σ0 + δ0). – the three remaining cases are straightforward.
Next, we can prove Lemma 1: Proof. To prove the lemma, it is sufficient to show that Mfc(N ) and Mcc(N ) are bisimulation equivalent. So, we shall show that the relation R ⊆ Σ ×Σs given by R = {((m, clock), (m0, clocks)) | m = m0 ∧ clocks = clock|cm1 } is a bisimulation. It is easy to see that σ0Rσ0, and that the valuations of the related states are equal (due to equality of their markings). Consider σ = (m, clock) ∈ Σ and σ0 = (m, clocks) ∈ Σs with clocks = clock|cm1 .
– if σ →δr σ1, where δ ∈ CN , then for each t ∈ en(m) there exists i ∈ IV(t) s.t. clock(i) + δ ≤ Lf t(t). Due to the fact that for each i ∈ I it holds clock|cm1 (i) ≤ clock(i), the time δ can pass at σ0 as well, leading to the state (m, clock|cm1 ⊕ δ). Consider the states (m, clock + δ) and (m, clock|cm1 ⊕ δ); we should show that (clock + δ)|cm1 = clock|cm1 ⊕ δ. We have the following cases: if clock(i) = clock|cm1 (i) and clock(i) + δ < cm1, then clock(i) + δ = clock|cm1 (i)+δ = clock|cm1 (i)⊕δ. If clock(i) = clock|cm1 (i) and clock(i)+δ ≥ cm1 then clock|cm1 (i) ⊕ δ = cm1, and therefore (clock + δ)|cm1 (i) = clock|cm1 (i) ⊕ δ. If clock(i) ≥ cm1 and clock|cm1 (i) = cm1 then clock(i) + δ ≥ cm1 and clock|cm1 (i) ⊕ δ = cm1 = (clock + δ)|cm1 (i), which ends this part of the proof. – if σ0 →δs σ10, where δ ∈ CN then for each t ∈ en(m) there exists i ∈ IV(t) s.t. clock|cm1 (i) ⊕ δ ≤ Lf t(t). If Lf t(t) < ∞, then this implies clock|cm1 (i) ⊕ δ ≤ cmax(N ), which in turn gives that clock|cm1 (i) ≤ cmax(N ), and therefore clock(i) = clock|cm1 (i), clock(i) + δ ≤ cmax(N ) and finally clock(i) + δ ≤ Lf t(t), while if Lf t(t) = ∞ then clock(i) + δ ≤ Lf t(t) in an obvious way. Thus, the time δ can pass in σ as well. Consider the states (m, clock + δ) and (m, clock|cm1 ⊕ δ); we should show that (clock + δ)|cm1 = clock|cm1 ⊕ δ, which can be done analogously as in the previous part of the proof. – The remaining two cases are straightforward.
Finally, we prove that the relation '? preserves the behaviours of the net (Lemma 2): Proof. Consider the states σ = (m, clock) and σ0 = (m, clock0) (σ, σ0 ∈ Σ) s.t. σ '? σ0.
– Consider l = δ ∈ IN. The time δ can pass in σ iff for each t ∈ en(m) there is i ∈ IV(t) s.t. clock(i) + δ ≤ Lf t(t). If Lf t(t) < ∞, then we have that mini∈IV(t) clock(i) + δ ≤ Lf t(t) ≤ cmax(N ), which implies that the states σ, σ0 satisfy mini∈IV(t) clock(i) = mini∈IV(t) clock0(i), and in turn mini∈IV(t) clock0(i) + δ = mini∈IV(t) clock(i) + δ ≤ Lf t(t). If Lf t(t) = ∞ we can have two cases: if mini∈IV(t) clock(i) = mini∈IV(t) clock0(i) ≤ cmax(N ) then mini∈IV(t) clock(i) + δ = mini∈IV(t) clock0(i) + δ which is not greater than Lf t(t) in an obvious way, while if mini∈IV(t) clock(i) > cmax(N ) and mini∈IV(t) clock0(i) > cmax(N ) then both mini∈IV(t) clock(i) + δ and mini∈IV(t) clock0(i) + δ are greater than cmax(N ) and do not exceed Lf t(t). Thus, the same time can pass at σ and at σ0, and the obtained states are ?-equivalent. – Consider l = t ∈ T such that t ∈ en(m). The transition t can fire at σ leading to a state σ1 = (m1, clock1) iff for each i ∈ IV(t) we have clock(i) ≥ Ef t(t) and there is i ∈ IV(t) such that clock(i) ≤ Lf t(t).
• If Lf t(t) < ∞ then from σ '? σ0 we have that mini∈IV(t) clock(i) = mini∈IV(t) clock0(i), which implies that for each i ∈ IV(t) clock0(i) ≥ Ef t(t) and there is i ∈ IV(t) such that clock0(i) ≤ Lf t(t), which means that t can fire at σ0 as well, leading to a state σ10 = (m01, clock10). In the obtained states we have m1 = m01, clock1(i) = 0 = clock10(i) for each i ∈ IV(t), and clock1(i) = clock(i), clock10(i) = clock0(i) otherwise. Consider a transition t0 ∈ en(m0). If IV(t)∩IV(t0) 6= ∅ then mini∈IV(t0) clock1(i) = mini∈IV(t0) clock10(i) = 0, while if IV(t) ∩ IV(t0) = ∅ then for each i ∈ IV(t0) the relation between clock1(i) and clock10(i) is the same as between clock(i) and clock0(i), which implies that either mini∈IV(t0) clock1(i) = mini∈IV(t0) clock10(i) ≤ cmax(N ) or mini∈IV(t0) clock1(i) > cmax(N ) ∧ mini∈IV(t0) clock10(i) > cmax(N ). Thus, we have σ1 '? σ0 . 1 • If Lf t(t) = ∞ then from the definition of cmax(N ) we have that Ef t(t) ≥ cmax(N ), and therefore from the definition of '? for each i ∈ IV(t) it holds clock0(i) ≥ Ef t(t), while for all i ∈ IV(t) clock0(t) < Lf t(t) in an obvious way. Thus, the transition can fire at σ0 as well, leading to a state σ10 = (m1, clock10). The proof that σ1 '? σ10 is analogous to the case Lf t(t) < ∞. – The rest of the proof is straightforward.