=Paper=
{{Paper
|id=None
|storemode=property
|title=Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-723/paper6.pdf
|volume=Vol-723
|dblpUrl=https://dblp.org/rec/conf/apn/MeskiPPWZ11
}}
==Bounded Model Checking Approaches for Verification of Distributed Time Petri Nets==
https://ceur-ws.org/Vol-723/paper6.pdf
Bounded Model Checking Approaches for
Verification of Distributed Time Petri Nets?
Artur Mȩski1,2 , Wojciech Penczek2,3 , Agata Półrola1 , Bożena
Woźna-Szcześniak4 , and Andrzej Zbrzezny4
1
University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland
polrola@math.uni.lodz.pl
2
Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland
{meski,penczek}@ipipan.waw.pl
3
University of Natural Sciences and Humanities, Institute of Informatics,
3 Maja 54, 08-110 Siedlce, Poland
4
Jan Długosz University, IMCS, Armii Krajowej 13/15, 42-200 Czȩstochowa, Poland
{b.wozna,a.zbrzezny}@ajd.czest.pl
Abstract. 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 com-
pared with each other on two standard benchmarks. Our experimental
results reveal the advantages and disadvantages of both the approaches.
1 Introduction
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
[1] and time Petri nets [22] by means of model checking [12, 26]. However, the
state explosion still remains the main problem to deal with while verifying a
timed system by searching through its state space, which in most cases is very
large due to infinity of the dense time domain. Furthermore, the size of the state
space is likely to grow exponentially in the number of the concurrent system
components. Symbolic model checking techniques [21] can be used to overcome
the above problem. These exploit various kinds of binary decision diagrams to
represent the model [24] or are based on a translation to a propositional satisfi-
ability problem.
Bounded model checking (BMC) is an efficient verification method using a
model truncated up to a specific depth only. In turn, SAT-based BMC verifica-
tion consists in translating a model checking problem solvable on a fraction of a
?
Partly supported by the Polish Ministry of Science and Higher Education under the
grant No. N N206 258035.
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 73
model into a test of propositional satisfiability, which is then performed using a
SAT-solver [28]. The method has been successfully applied to verification of both
timed and untimed systems [3–5, 33]. Alternatively, one can use binary decision
diagrams to represent a truncated model and to perform BDD-based verification
[2, 13].
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 [15] when performing decision diagram based verification.
Moreover, the saturation combined with BMC was presented in [34], however
only reachability checking was considered. Still, we believe, in most cases, BMC
approach to BDD-based verification can be viewed as an alternative way of
avoiding the BDD peak size when using BFS. In case of SAT we exploit the
most efficient translations known for ECTL−X and ELTL−X .
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 ap-
proaches 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
74 PNSE’11 – Petri Nets and Software Engineering
mostly for standard untimed models, while discrete time Petri nets have been
studied with BDDs and extensions (e.g., [31]), but not for BMC.
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 [27, 16]. Symbolic model checking has been investigated in many
papers [2, 5]. Verification of CTL properties based on BDDs was introduced in [9].
In [27] SAT-based BMC for the existential fragment of CTL was described and
implemented for elementary net systems. Verification methods using BDD-based
BMC were studied in [10, 13] for simple invariant properties, in [23] for CTL
over elementary nets systems, and in [19] for CTL extended with an epistemic
component over multi-agent systems. On the other hand, verification of temporal
properties for time Petri nets was a subject of intensive research of the teams of
H. Boucheneb and O.H. Roux [6, 7, 20].
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 Temporal Logics LTL−X and CTL−X
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 =
def def def
¬(¬ϕp ∨ ¬ϕp ), Eϕp = ¬A(¬ϕp ), Gϕp = f alseRϕp , and Fϕp = 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 )
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 75
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 re-
stricted 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 proposi-
tions 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∗−X which can be found
in several papers, among others in [11, 12], so we do not deliver it here. Moreover,
we assume that a CTL∗−X formula ϕ is true in the model M (denoted by M |= ϕ)
iff ϕ is true at the initial state of the model, i.e., M, s0 |= ϕ.
3 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;
76 PNSE’11 – Petri Nets and Software Engineering
– 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 [ti i;
– 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) [26]:
Definition 2. Let I = {i1 , . . . , in } be a finite ordered set of indices, and let
N = {Ni = (Pi , Ti , Fi , m0i , Ef ti , Lf ti ) | i ∈ I} be a family of 1-safe, sequen-
tial time Petri nets (called processes), indexed with I, with the pairwise dis-
joint sets Pi of places, and satisfying the condition (∀i1 , i2 ∈ I)(∀t ∈ Ti1 ∩
Ti2 ) (Ef ti1 (t) = Ef ti2 (t) ∧ Lf ti1 (t) = Lf ti2 (t)). A distributed time Petri
net N = (P, T,
S
0
St) is the 0unionSof the0 processes SNi , i.e., P =
SF, m , Ef t, Lf
P
i∈I iS, T = T
i∈I i , F = i∈I Fi , m = i∈I mi , Ef t = i∈I Ef ti , and
Lf t = i∈I Lf ti .
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 sys-
tem 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 [18]. Moreover, for
t ∈ T we define IV(t) = {i ∈ I | •t ∩ Pi 6= ∅}, and say that a process Ni is
involved in a transition t iff i ∈ IV(t).
3.1 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 be-
haviour of the net). In our work we assume a discrete-time semantics of DTPNs,
i.e., consider integer time passings only (cf. [26]). Thus, a concrete state σ of a
distributed TPN N can be defined as an ordered pair (m, clock), where m is
a marking, and clock : I → IN is a function which for each index i of a pro-
cess of N gives the time elapsed since the marked place of this process became
marked most recently [29]. The set of all the concrete states is denoted by Σ.
The initial state of N is σ 0 = (m0 , clock 0 ), where m0 is the initial marking, and
clock 0 (i) = 0 for each i ∈ I.
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
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 77
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 , clock 0 ) (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 clock 0 (i) = 0 if i ∈ IV(t), and
clock 0 (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
a a
sequence of concrete states, transitions, and time passings ρ = σ0 →0 c σ1 →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∗−X Verification 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
78 PNSE’11 – Petri Nets and Software Engineering
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
cc (N ) = (T ∪ CN , Σs , σ 0 , →s , Vs ), where Σs = {σ|c | σ ∈ Σ}, Vs is
follows: M m1
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
t t
σs →s σs0 ) iff σ →c σ 0 for some σ 0 ∈ Σ s.t. σs0 = σ 0 |cm1 .
In order to show that M cc (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 )
cc (N ) = (T ∪ CN , Σs , σ 0 , →s , Vs ) are bisimulation equivalent.
and M
The proof can be found in the appendix. In the proof we use an “intermediate”
fc (N ) = (T ∪ CN , Σ, σ 0 , →r , Vc ) with →r ⊆ Σ × (T ∪ CN ) × Σ given by
model M
– 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
t
σ →c σ 0 ,
(i.e., the model which differs from M cc (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 , clock 0 ) 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) clock 0 (i) ∧ mini∈IV(t) clock(i) ≤
cmax (N )) ∨ (mini∈IV(t) clock(i) > cmax (N ) ∧ mini∈IV(t) clock 0 (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:
l l
– if σ →c σ1 for some σ1 ∈ Σ then there is σ10 ∈ Σ s.t. σ 0 →c σ10 and σ1 '? σ10 ,
l l
– if σ 0 →c σ10 for some σ10 ∈ Σ then there is σ1 ∈ Σ s.t. σ →c σ1 and σ10 '? σ1 .
4 SAT-Based BMC for ELTL−X and ECTL−X
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 counterexam-
ples for the properties expressed in “universal” logics (in our case ACTL−X and
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 79
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 ) [32], and on an improved BMC trans-
lation for the ECTL−X fragment [35]. In particular, in the paper we adapt
the BMC techniques mentioned above to the DTPN setting. Let M fc (N ) =
(T ∪CN , Σ, σ , →r , Vc ) be a model for a given DTPN N = (P, T, F, m , Ef t, Lf t)
0 0
, and ϕ an ECTL−X or ELTL−X formula describing an undesired property. To
show that ϕ is true in M fc (N ), it is enough to prove that ϕ holds in a frag-
ment (submodel) M of M 0 f. Thus, we start by taking a submodel M 0 of the
model M fc (N ) that consists of the finite prefixes of paths from Mfc (N ) restricted
by a bound k ∈ IN – traditionally called k-paths. The number of k-paths in
M 0 depends on the checked formula ϕ, and it is specified by a value of a
function fk : FECTL∗−X → IN defined by: for ℘ ∈ P V , fk (℘) = fk (¬℘) = 0,
fk (ϕ ∧ ψ) = fk (ϕ) + fk (ψ), fk (ϕ ∨ ψ) = max{fk (ϕ), fk (ψ)}, fk (Eϕ) = fk (ϕ) + 1,
fk (ϕUψ) = k · fk (ϕ) + fk (ψ), fk (ϕRψ) = (k + 1) · fk (ψ) + fk (ϕ). Next, we trans-
late the problem of checking whether the M 0 is a model for ϕ to the problem of
checking the satisfiability of the following propositional formula:
0
fc (N ), ϕ]k := [M
[M fc (N )ϕ,σ ]k ∧ [ϕ]M 0 (1)
The first conjunct of Formula 1 represents all the submodels M 0 of M fc (N ) that
consists of fk (ϕ) k-paths, and the second a number of constraints that must
be satisfied on these submodels for ϕ to be satisfied. Once this translation is
defined, satisfiability of an ECTL−X or ELTL−X formula can be tested with a
SAT-solver.
How to define the formula [M fc (N )ϕ,σ0 ]k in the DTPN settings we show
in the next subsection. Note however that for a given DTPN N , the formula
fc (N )ϕ,σ0 ]k can be implemented either using the model M
[M fc (N ) or using M cc (N ).
We have chosen M fc (N ) in order to simplify the implementation. It should be
explained that although in M fc (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 [ϕ]M 0 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 alternat-
ing 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.
80 PNSE’11 – Petri Nets and Software Engineering
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 [ϕ]M 0 that can be found, respectively, in
[35] (ECTL−X ), and in [32, 5] (ELTL−X ). However, to apply them to the DTPN
setting, we have changed the definition of the loop to the one presented above.
Definition of formula [M fc (N )ϕ,σ0 ]k . Let M
fc (N ) = (T ∪ CN , Σ, σ 0 , →r , Vc )
be a model of a given DTPN N = (P, T, F, m0 , Ef t, Lf t), ϕ an ECTL−X
or ELTL−X formula, and k ∈ IN a bound. In order to define the formula
fc (N )ϕ,σ0 ]k that constrains the fk (ϕ) symbolic k-paths to be valid k-paths
[M
of Mfc (N ), we proceed as follows. We assume that each state σ ∈ Σ is given
in a unique binary form, i.e., every state σ can be encoded as a bit vector
(σ[1], . . . , σ[lb ]) of length lb depending on the number of places P of N , the
bound k , the value cmax (N ) (i.e., the greatest finite value of Ef t and Lf t), and
the value fk (ϕ). Thus, each state σ can be represented by a valuation of a vector
w = (w[1], . . . , w[lb ]) (called a global state variable), where w[i], for i = 1, . . . , lb
is a propositional variable (called state variable)5 . A finite sequence (w0 , . . . , wk )
of global state variables is called a symbolic k-path. Since in the ECTL−X case
we shall need to consider not just one but a number of symbolic k-paths, we
use the notation of j-th symbolic k-path (w0,j , . . . , wk,j ), where wi,j are global
state variables for 0 ≤ j < fk (ϕ) and 0 ≤ i ≤ k; the number of symbolic k-paths
depends on the formula ϕ under investigation, and it is returned as the value
fk (ϕ) of the function fk ; note that if ϕ is an ELTL−X formulae then fk (ϕ) = 1.
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 M fc (N ), i.e., σ[i] = 1
is encoded by w[i], and σ[i] = 0 is encoded by ¬w[i].
• T S(w, w0 ) (T S 0 (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, w ) is a formula over w and w which is true for two valuations σw
0 0
t
of w and σw0 of w0 iff σw →r σw0 , for t ∈ T . It encodes the action-successor
fc (N ).
relation of M
The propositional formula [Mfcϕ,σ0 ]k is defined as follows:
fk (ϕ)−1 k−1
0 ^ ^
fcϕ,σ ]k := Iσ0 (w0,0 ) ∧
[M R(wi,j , wi+1,j )
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 S 0 (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].
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 81
Note that if ϕ is an ELTL−X formula, then fk (ϕ) = 1, and the above definition
fcϕ,σ0 ]k := Iσ0 (w0,0 ) ∧ Vk−1 R(wi,0 , wi+1,0 ).
is equivalent to the following one: [M i=0
5 BDD-based BMC for ELTL−X and ECTL−X
Binary decision diagrams (BDDs) [8, 17] are an efficient data structure widely
used for storing and manipulating boolean functions. In the paper we use Re-
duced Ordered Binary Decision Diagrams (ROBDDs) instead of the “pure” BDD
structures. The advantage of ROBDDs is that they are canonical for a particular
function and variable order.
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 for-
mula holds [17]. For this purpose we need the notion of a fixed point.
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 X 0 ⊆ S is a fixed point of τ if τ (X 0 ) = X 0 . 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
L) s → 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.
def
For ECTL−X formulae ϕ and ψ we define the following sets: [[true]] = SR ,
def def def def
[[℘]] = {s ∈ SR | ℘ ∈ V (s)}, [[¬ϕ]] = SR \ [[ϕ]], [[ϕ ∧ ψ]] = [[ϕ]] ∩ [[ψ]], [[ϕ ∨ ψ]] =
[[ϕ]]∪[[ψ]]. The remaining operators can be defined as fixed points in the following
def def
way: [[EGϕ]] = νX.[[ϕ]] ∩ pre∃ (X), [[E[ϕUψ]]] = µ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 [11], that is then combined
with the model M to obtain their product, which contains these paths of M
where the formula ϕ potentially holds. The product is then verified in terms of
CTL model checking of EGtrue formula under fairness constraints. The fairness
constraints, corresponding to sets of states, allow to choose only these paths
of the model, along which at least one state in each set representing fairness
constraints appears infinitely often. In the case of ELTL−X model checking,
fairness is applied to guarantee that E(ϕUψ) really holds, i.e., to eliminate paths
where ϕ holds continuously, but ψ never holds. Finally, we choose only these
reachable states of the product that belong to some particular set of states
computed for the formula. The corresponding states of the verified system that
are in this set, comprise the set [[M, ϕ]], i.e., the set of the reachable states
where the verified formula holds. As we are unable to include a more detailed
82 PNSE’11 – Petri Nets and Software Engineering
description of the method (due to the page limit), we refer the reader to [11] for
more details.
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 l
L | (∃s, s0 ∈ U ) s → s0 }, →0 = {s → 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
def l
successors of all the states in X by X; = {s0 ∈ S | (∃s ∈ X)(∃l ∈ L) s → 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 M cc (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 (σ[1], . . . , σ[lb ]) of length lb depending on the
number of places P of N , and the value cmax (N ). Thus, each state σ can be
represented by a valuation of a vector w = (w[1], . . . , w[lb ]) (called a global state
variable), where w[i], for i = 1, . . . , lb is a propositional variable (called state
variable).
Let w, w0 be two global state variables. We define the following boolean for-
mulae that are used in the encoding:
• Iσ (w) is a formula that encodes the state σ of the model M c(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
cc (N ).
relation of M
• ASt (w, w ), where t ∈ T , is a formula over w and w0 which is true for two
0
t
valuations σw of w and σw0 of w0 iff σw →s σw0 . It encodes the action-
cc (N ) for the transition t ∈ T .
successor relation of M
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 83
W
• T (w, w0 ) = t∈T ASt (w, w ) ∨ T S(w, w ) is a formula over w and w which
0 0 0
is true for two valuations σw of w and σw0 of w iff σw →s σw0 . It encodes
0
cc (N ).
the transition relation of M
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 [17] where
the variables encoding the states and their successors are interleaved. The expla-
nation of how we can compute the BDDs for the sets X; and pre∃ (X) (where
X ∈ Σs ) that are needed by the described fixed point methods can be found also
in [17]. Moreover, we encode each disjunct of the formula encoding the transition
relation, with separate BDDs.
6 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 con-
sumed 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 [25], which consists of Producer producing data (P rod-
Ready) or being inactive, Consumer receiving data (ConsReady) or being inac-
tive, and a chain of n intermediate Nodes which can be ready for receiving data
(N odei Ready), processing data (N odei P roc), or sending data (N odei Send). The
example can be scaled in the number of intermediate nodes. The intervals are
used to adjust the time properties of Producer, Consumer, and of the interme-
diate Nodes.
The second benchmark of our interest is the DTPN model for Fischer’s mu-
tual 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 [0, 2], was tested
with the ECTL−X formula ψ1 = EG(EF(¬ConsReady)), and the ELTL−X for-
mula ψ2 = EGF(¬ConsReady). The Mutex protocol, with ∆ = 1 and δ = 2,
was tested with the ECTL−X formulae: ψ1 = EGEF(critical1 ∨ . . . ∨ criticalN ),
ψ2 = EF(trying1 ∧ . . . ∧ tryingN ∧ EG(¬critical2 ∧ . . . ∧ ¬criticalN )), and the
ELTL−X formulae: ψ3 = EGF(critical1 ∨ . . . ∨ criticalN ), ψ4 = EF(trying1 ∧
. . . ∧ tryingN ∧ G(¬critical2 ∧ . . . ∧ ¬criticalN )).
84 PNSE’11 – Petri Nets and Software Engineering
The above systems have been carefully selected in order to reveal the advan-
tages and disadvantages of both SAT- and BDD-based BMC approaches.
Memory usage for GTPP, ECTLX formula ψ1 Total time for GTPP, ECTLX formula ψ1
1600
BDD, fixed order 3500
1400 BDD, reordered
BDD, partitioning, fixed order 3000
1200 BDD, partitioning, reordered
2500
Time in sec.
Memory in MB
SAT, alternating sem.
1000 SAT, non-alternating sem.
2000
800
1500
600
1000
400
500
200
0
0
0 5 10 15 20 25 30 35 40 0 5 10 15 20 25 30 35 40
Number of processes Number of processes
Memory usage for GTPP, ELTLX formula ψ2 Total time for GTPP, ELTLX formula ψ2
4000
BDD, fixed order 6000
3500 BDD, reordered
BDD, partitioning, fixed order 5000
3000 BDD, partitioning, reordered
Time in sec.
Memory in MB
SAT, alternating sem. 4000
2500 SAT, non-alternating sem.
Tina
2000 3000
1500 2000
1000
1000
500
0
0
0 5 10 15 20 25 0 5 10 15 20 25
Number of processes Number of processes
For the SAT-based BMC method two semantics are implemented: the alter-
nating 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 indepen-
dent 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 for-
mulae that are more complicated than in case of the alternating semantics. This
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 85
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 BDD-
based 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 [2].
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 [30], which is a general purpose BDD library, while the
SAT-based technique uses MiniSat2 [14] for testing satisfiability of the generated
propositional formulae.
7 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
86 PNSE’11 – Petri Nets and Software Engineering
Memory usage for Mutex, ECTLX formula ψ1 Total time for Mutex, ECTLX formula ψ1
5000
BDD, fixed order 4500
4500 BDD, reordered 4000
4000 BDD, partitioning, fixed order
BDD, partitioning, reordered 3500
3500
Time in sec.
Memory in MB
SAT, alternating sem. 3000
3000 SAT, non-alternating sem.
2500
2500
2000
2000
1500
1500
1000
1000
500
500
0
0
0 10 20 30 40 50 60 70 80 90 100 0 10 20 30 40 50 60 70 80 90 100
Number of processes Number of processes
Memory usage for Mutex, ECTLX formula ψ2 Total time for Mutex, ECTLX formula ψ2
1400
BDD, fixed order 4500
1200 BDD, reordered 4000
BDD, partitioning, fixed order
1000 BDD, partitioning, reordered 3500
Time in sec.
Memory in MB
SAT, alternating sem. 3000
SAT, non-alternating sem.
800 2500
600 2000
1500
400
1000
200 500
0
0
2 4 6 8 10 12 14 16 2 4 6 8 10 12 14 16
Number of processes Number of processes
Memory usage for Mutex, ELTLX formula ψ3 Total time for Mutex, ELTLX formula ψ3
3000
BDD, fixed order 4000
BDD, reordered 3500
2500 BDD, partitioning, fixed order
BDD, partitioning, reordered 3000
Time in sec.
Memory in MB
2000 SAT, alternating sem.
SAT, non-alternating sem. 2500
Tina
1500 2000
1500
1000
1000
500 500
0
0
0 10 20 30 40 50 60 70 0 10 20 30 40 50 60 70
Number of processes Number of processes
Memory usage for Mutex, ELTLX formula ψ4 Total time for Mutex, ELTLX formula ψ4
2000
BDD, fixed order 6000
1800 BDD, reordered
1600 BDD, partitioning, fixed order 5000
BDD, partitioning, reordered
1400
Time in sec.
Memory in MB
SAT, alternating sem. 4000
1200 SAT, non-alternating sem.
Tina
1000 3000
800
2000
600
400 1000
200
0
0
2 3 4 5 6 7 8 9 10 2 3 4 5 6 7 8 9 10
Number of processes Number of processes
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 87
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 consid-
ered 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.
References
1. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science,
126(2):183–235, 1994.
2. N. Amla, R. Kurshan, K. McMillan, and R. Medel. Experimental analysis of
different techniques for bounded model checking. In Proc. of TACAS’03, volume
2619 of LNCS, pp. 34–48. Springer-Verlag, 2003.
3. G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani. Bounded model
checking for timed systems. In Proc. of FORTE’02, volume 2529 of LNCS, pp.
243–259. Springer-Verlag, 2002.
4. M. Benedetti and A. Cimatti. Bounded model checking for Past LTL. In Proc. of
TACAS’03, volume 2619 of LNCS, pp. 18–33. Springer-Verlag, 2003.
5. A. Biere, A. Cimatti, E. Clarke, M.Fujita, and Y. Zhu. Symbolic model checking
using SAT procedures instead of BDDs. In Proc. of DAC’99, pp. 317–320, 1999.
88 PNSE’11 – Petri Nets and Software Engineering
6. H. Boucheneb, G. Gardey, and O. H. Roux. TCTL model checking of time Petri
nets. Journal of Logic and Computation, 19(6):1509–1540, 2009.
7. H. Boucheneb and R. Hadjidj. CTL∗ model checking for time Petri nets. Theoretical
Computer Science, 353(1):208–227, 2006.
8. R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE
Transaction on Computers, 35(8):677–691, 1986.
9. J. R. Burch, E. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic
model checking: 1020 states and beyond. Information and Computation, 98(2):142–
170, 1990.
10. G. Cabodi, P. Camurati, and S. Quer. Can BDD compete with SAT solvers on
bounded model checking? In Proc. of DAC’02, pp. 117–122, 2002.
11. E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking.
In Proc. of CAV’94, volume 818 of LNCS, pp. 415–427. Springer-Verlag, 1994.
12. E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
13. F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi.
Benefits of bounded model checking at an industrial setting. In Proc. of CAV’01,
volume 2102 of LNCS, pp. 436–453. Springer-Verlag, 2001.
14. N. Eén and N. Sörensson. MiniSat - A SAT Solver with Conflict-Clause Minimiza-
tion. In Proc. of SAT’05, LNCS. Springer-Verlag, 2005.
15. G. Luettgen G. Ciardo and A. S. Miner. Exploiting interleaving semantics in
symbolic state-space generation. Formal Methods in System Design, 31:63–100,
2007.
16. K. Heljanko and I. Niemelä. Bounded LTL model checking with stable models. In
Proc. of LPNMR’01, volume 2173 of LNCS, pp. 200–212. Springer-Verlag, 2001.
17. M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about
Systems. Cambridge University Press, 2004.
18. R. Janicki. Nets, sequential components and concurrency relations. Theoretical
Computer Science, 29:87–121, 1984.
19. A. Jones and A. Lomuscio. A BDD-based BMC approach for the verification
of multi-agent systems. In Proc. of CS&P’09, volume 1, pp. 253–264. Warsaw
University, 2009.
20. D. Lime and O. H. Roux. Model checking of time Petri nets using the state class
timed automaton. Discrete Event Dynamic Systems, 16(2):179–205, 2006.
21. K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
22. P. Merlin and D. J. Farber. Recoverability of communication protocols – impli-
cation of a theoretical study. IEEE Trans. on Communications, 24(9):1036–1043,
1976.
23. A. Mȩski, W. Penczek, and A. Półrola. BDD-based bounded model checking for el-
ementary net systems. In Proc. of CS&P’10, volume 237(1) of Informatik-Berichte,
pp. 219–230. Humboldt University, 2010.
24. A. Miner and G. Ciardo. Efficient reachability set generation and storage us-
ing decision diagrams. In Proc. of ICATPN’99, volume 1639 of LNCS, pp. 6–25.
Springer-Verlag, 1999.
25. D. Peled. All from one, one for all: On model checking using representatives. In
Proc. of CAV’93, volume 697 of LNCS, pp. 409–423. Springer-Verlag, 1993.
26. W. Penczek and A. Półrola. Advances in Verification of Time Petri Nets and Timed
Automata: A Temporal Logic Approach, volume 20 of Studies in Computational
Intelligence. Springer-Verlag, 2006.
27. W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal
fragment of CTL. Fundamenta Informaticae, 51(1-2):135–156, 2002.
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 89
28. Knot Pipatsrisawat and Adnan Darwiche. Rsat 2.0: Sat solver description. Techni-
cal Report D–153, Automated Reasoning Group, Computer Science Department,
UCLA, 2007.
29. A. Półrola and W. Penczek. Minimization algorithms for time Petri nets. Funda-
menta Informaticae, 60(1-4):307–331, 2004.
30. F. Somenzi. CUDD: CU decision diagram package - release 2.3.1. http://
vlsi.colorado.edu/∼fabio/CUDD/cuddIntro.html.
31. M. Wan and G. Ciardo. Symbolic reachability analysis of integer timed petri nets.
In Proc. of SOFSEM’2009, pp. 595–608, 2009.
32. B. Woźna. ACTL∗ properties and bounded model checking. Fundamenta Infor-
maticae, 63(1):65–87, 2004.
33. B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for
timed automata via SAT. Fundamenta Informaticae, 55(2):223–241, 2003.
34. A. J. Yu, G. Ciardo, and G. Luettgen. Decision-diagram-based techniques for
bounded reachability checking of asynchronous systems. Software Tools for Tech-
nology Transfer, 11(2):117–131, 2009.
35. A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Infor-
maticae, 85(1-4):513–531, 2008.
A Appendix: Models for DTPNs - Proofs
cc (N ) can replace Mc (N ) in CTL∗−X verification (i.e., to
In order to show that M
prove Lemma 1) we shall prove the following lemma:
Lemma 3. For a given distributed time Petri net N the models Mc (N ) =
fc (N ) = (T ∪ CN , Σ, σ 0 , →r , Vc ) are bisimulation
(T ∪ IN, Σ, σ 0 , →c ), Vc and M
equivalent.
Proof. We shall show that the relation R = {((m, clock), (m0 , clock 0 )) | m =
m0 ∧∀(i ∈ I s.t. clock(i) ≤ cmax (N )) clock(i) = clock 0 (i) ∧ ∀(i ∈ I s.t. clock(i) >
cmax (N )) clock 0 (i) > cmax (N )} is a bisimulation. It is easy to see that σ 0 Rσ 0 ,
and the valuations of the related states are equal (due to equality of their mark-
ings). Consider σ = (m, clock) ∈ Σ and σ 0 = (m, clock 0 ) ∈ Σ 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 clock 0 (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
90 PNSE’11 – Petri Nets and Software Engineering
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 M fc (N ) and M cc (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 σ 0 Rσ 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, clock 0 ) (σ, σ 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) clock 0 (i), and in turn
mini∈IV(t) clock 0 (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) clock 0 (i) ≤
cmax (N ) then mini∈IV(t) clock(i) + δ = mini∈IV(t) clock 0 (i) + δ which is not
A. Męski et al.: Bounded Model Checking Approaches for Verification of DTPN 91
greater than Lf t(t) in an obvious way, while if mini∈IV(t) clock(i) > cmax (N )
and mini∈IV(t) clock 0 (i) > cmax (N ) then both mini∈IV(t) clock(i) + δ and
mini∈IV(t) clock 0 (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) clock 0 (i), which implies that for each i ∈ IV(t) clock 0 (i) ≥
Ef t(t) and there is i ∈ IV(t) such that clock 0 (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) = clock 0 (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 clock 0 (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 '? σ10 .
• 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 clock 0 (i) ≥ Ef t(t), while for all i ∈ IV(t) clock 0 (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.