=Paper=
{{Paper
|id=None
|storemode=property
|title=Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-851/paper2.pdf
|volume=Vol-851
|dblpUrl=https://dblp.org/rec/conf/apn/JanowskaPPZ12
}}
==Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets==
https://ceur-ws.org/Vol-851/paper2.pdf
Using Integer Time Steps for Checking
Branching Time Properties of Time Petri Nets
Agata Janowska1 , Wojciech Penczek2 , Agata Półrola3 , and Andrzej Zbrzezny4
1
Institute of Informatics, University of Warsaw, Banacha 2, 02-097 Warsaw, Poland
janowska@mimuw.edu.pl
2
Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland
penczek@ipipan.waw.pl
3
University of Łódź, FMCS, Banacha 22, 90-238 Łódź, Poland
polrola@math.uni.lodz.pl
4
Jan Długosz University, IMCS, Armii Krajowej 13/15, 42-200 Czȩstochowa, Poland
a.zbrzezny@ajd.czest.pl
Abstract. Verification of timed systems is an important subject of re-
search, and one of its crucial aspects is the efficiency of the methods de-
veloped. Extending the result of Popova which states that integer time
steps are sufficient to test reachability properties of time Petri nets [5,
8], in our work we prove that the discrete-time semantics is also suffi-
cient to verify ECTL∗ and ACTL∗ properties of TPNs with the dense
semantics. To show that considering this semantics instead of the dense
one is profitable, we compare the results for SAT-based bounded model
checking of ACTL−X properties and the class of distributed time Petri
nets.
1 Introduction
Verification of time-dependent systems is an important subject of research. The
crucial problem to deal with is the state explosion: the state spaces of these
systems are usually very large due to infinity of the dense time domain, and
are likely to grow exponentially in the number of concurrent components of the
system. This influences strongly the efficiency of the model checking methods.
The papers of Popova [5, 8] show that in the case of checking reachability
for systems modelled by time Petri nets (i.e., while testing whether a marking
of a net is reachable) one can use discrete (integer) time steps instead of real-
valued ones. This reduces the state space to be searched. The aim of our work
is to investigate whether the result of Popova can be extended, i.e., whether
the discrete-time semantics can replace the dense-time one also while verifying
a wider class of properties of dense-time Petri net systems. In this paper we
present our preliminary result, i.e., prove that the discrete-time model can be
used instead of the dense-time one while verifying ECTL∗ and ACTL∗ properties.
To show that such an approach can be profitable we perform some experiments,
using an implementation for SAT-based bounded model checking of ACTL−X
16 PNSE’12 – Petri Nets and Software Engineering
and the class of distributed time Petri nets with the discrete-time semantics [4],
as well as its modification for the dense-time case.
The rest of the paper is organised as follows: Sec. 2 discusses the related
work. Sec. 3 introduces time Petri nets and their dense and discrete models.
Sec. 4 presents the logics ECTL∗ and ACTL∗ . Sec. 5 deals with the theoretical
considerations, while Sec. 6 presents the experimental results. Sec. 7 contains
final remarks and sketches directions of the further work.
2 Related Works
We would like to stress that in our work we are interested in branching time
properties. To our best knowledge the fact that the discrete-time semantics is
sufficient to verify ECTL∗ or ACTL∗ properties of time Petri nets (TPNs) with
the dense-time semantics has never been proven before.
The topic of verification of dense-time Petri nets using integer time steps has
been studied in several publications. In paper [5] it is shown how to construct a
reachability graph whose vertices are reachable integer states for time Petri nets
in which all the latest firing times are finite. The main theorem of [5] (Thm 3.2)
states that for each run of a TPN, starting at its initial state, it is possible to find
a corresponding run which starts at the initial state as well, and visits integer
states only. Due to this theorem a discrete analysis of boundedness and liveness
of a TPN is possible. The work [6] extends the results of [5] to arbitrary TPNs.
It uses the idea of “freezing” the clock values of transitions with infinite Lf t
just as their Ef t is reached. This way a reduced (finite) reachability graph of
“essential” (integer) states is obtained.
In [8] and [7] the state space of a TPN is characterised parametrically. The
main theorems (Thm 3.1 and Thm 3.2) of [8] state that for an arbitrary feasible
execution path where the clocks have real values it is possible to replace these
real values by integer ones and obtain another feasible path. The differences
between the clocks values of each enabled transition at a given marking in the
former and the latter path are always smaller than 1, and so are the differences
between total times of both the executions. The main idea of the proof is as
follows: the integer values are constructed out of the given assignments of real
values by successive transforming all the non-integer numbers to nearby integers
in n + 1 steps, where n is the length of the path. According to the theorems
the minimal and maximal time duration of a transition sequence are integer
values. In the paper [7] an enumerative procedure for reducing the state space
is introduced. The idea is to divide a problem into a finite number of smaller
problems, which can be solved recursively with a methodology inspired from
dynamic programming. Moreover, it extends the method of [8] to the nets with
real-valued time steps (in [8] rational time steps were allowed only) and infinite
latest firing times.
The authors of the above-mentioned papers claim that the knowledge of the
reachable integer states is sufficient to determine the entire behaviour of the
net at any point in time. However, all these papers show the trace equivalence
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 17
a a
a
b c b c
p1 p2 p1 p2
Fig. 1. Two trace equivalent models which are not (bi)similar. A formula distinguishing
them is e.g. ϕ = EF(EXp1 ∧ EXp2) which holds for the model on the right only
between a continuous model and a (restricted) discrete one. It is very well known
that trace equivalence preserves linear time properties, but it does not preserve
branching time properties (see Fig. 1 and [1]), so the word “behaviour” should
probably be understood in a way following from a fragment of [7]: “The properties
of a Petri net, both the classical one as well as the TPN, can be divided into two
parts: There are static properties, like being pure, ordinary, free choice, extended
simple, conservative, etc., and there are dynamic properties like being bounded,
live, reachable, and having place- or transitions invariants, deadlocks, etc. While
it is easy to prove the static behavior of a net using only the static definition, the
dynamic behavior depends on both the static and dynamic definitions and is quite
complicated to prove.”, so as the dynamic properties listed. Moreover, the result
of the papers [5, 6] does not imply bisimulation between both the models, as the
construction given in these papers cannot be used to prove it. We discuss this on
p. 27, showing that the relation R used in our proof and derived from the result
of [5, 6] cannot be used to prove bisimulation. This follows from the fact that
the integer run π 0 “justifying” σ 0 Rσ (generated according to the construction of
[5]) and the dense run π occurring in the relation do not need to “branch” in
the same way. Similarly, the result of [8, 7] does not imply (bi)simulation as well.
Although it is not stated directly, the construction given in these papers is based
on a parametric description of the classes of the forward-reachability graph for
a net considered (i.e., a structure in which the initial state class contains the
initial state of the net and all the time successors of this state, and given a
state class Cx corresponding to firing a sequence of transitions x, its successor
class on a transition t contains all the concrete states which can be obtained by
firing t at a concrete state σ ∈ Cx and then passing some time not disabling any
enabled transition). It is well known that such a structure preserves reachability
and linear time properties, but it does not preserve branching time properties.
The discrete runs constructed in both the papers are retrieved from the dense
ones to preserve nothing but visiting the same state classes as the runs they
correspond to.
The current paper is a modified and improved version of our work [3] (pub-
lished in the proceedings of a local workshop, and containing a completely dif-
ferent proof which does not define simulation explicitely).
18 PNSE’12 – Petri Nets and Software Engineering
3 Time Petri Nets
We start from introducing some basic definitions related to time Petri nets. For
simplicity of the presentation we focus on 1-safe time Petri nets only. However,
our result applies also to unbounded nets, which is explained in more details in
the final section.
Let IN be the set of natural numbers (including zero), and IR (IR+ ) be the
set of (nonnegative) reals. Time Petri nets are defined as follows:
Definition 1. A time Petri net (TPN, for short) is a six-element tuple N =
(P, T, F, Ef t, Lf t, m0 ), 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, Ef t : T → IN and 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), and m0 ⊆ P is the initial marking of N .
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 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};
– for t ∈ en(m), newly_en(m, t) = {u ∈ T | u ∈ en(m[ti) ∧ (t • ∩ • u 6=
∅ ∨ u • ∩ • t 6= ∅)}.
Concerning the behaviour of time Petri nets, it is possible to consider a dense-
time semantics, i.e. the one in which the time steps can be of an arbitrary
(nonnegative) real-valued length, and the discrete one which considers integer
time passings only. Below we define both of them.
3.1 Dense-Time Semantics
In the dense-time semantics (the dense semantics in short) a concrete state σ of a
net N is defined as a pair (m, clock), where m is a marking, and clock : T → IR+
is a function which for each transition t ∈ en(m) gives the time elapsed since
t became enabled most recently, and assigns zero to other transitions. Given
a state (m, clock) and δ ∈ IR+ , denote by clock + δ the function defined by
(clock + δ)(t) = clock(t) + δ for each t ∈ en(m), and (clock + δ)(t) = 0 otherwise.
By (m, clock) + δ we denote (m, clock + δ). The dense concrete state space of N
is a structure (T ∪ IR+ , Σ, σ 0 , →r ), where Σ is the set of all the concrete states
of N , σ 0 = (m0 , clock 0 ) with clock 0 (t) = 0 for each t ∈ T is the initial state of
N , and →r ⊆ Σ × (T ∪ IR+ ) × Σ is a timed consecution relation defined by:
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 19
δ
– for δ ∈ IR+ , (m, clock) →r (m, clock + δ) iff (clock + δ)(t) ≤ Lf t(t) for all
t ∈ en(m) (time successor),
t
– for t ∈ T , (m, clock) →r (m0 , clock 0 ) iff t ∈ en(m), Ef t(t) ≤ clock(t) ≤
Lf t(t), m = m[ti, and for all u ∈ T we have clock 0 (u) = 0 for u ∈
0
newly_en(m, t) and clock 0 (u) = clock(u) otherwise (action successor).
Notice that firing of a transition takes no time.
Given a set of propositional variables P V , we introduce a valuation function
V : Σ → 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 p ∈ P , and use the same names for the propositions and the places.
The function V is then defined by p ∈ V (σ) iff p ∈ m for each σ = (m, ·). The
structure Mr (N ) = (T ∪ IR+ , Σ, σ 0 , →r , V ) is a dense concrete model of N .
a a
A dense σ-run of TPN N is a (maximal) sequence of states: σ0 →0 r σ1 →1 r
a
σ2 →2 r . . ., where σ0 = σ ∈ Σ and ai ∈ T ∪ IR+ for each i ≥ 0. A state σ is
a a a
reachable in Mr (N ) if there is a dense σ 0 -run σ0 →0 r σ1 →1 r σ2 →2 r . . . such that
σ = σi for some i ∈ IN.
3.2 Discrete-Time Semantics
Alternatively, one can consider integer time passings only. In such a discrete-
time semantics (discrete semantics in short) a (discrete) concrete state σn of
a net N is a pair (m, clockn ), where m is a marking, and clockn : T → IN is
a function which for each transition t ∈ en(m) gives the time elapsed since t
became enabled most recently, and assigns zero to the other transitions. Given a
state (m, clockn ) and δ ∈ IN, we define clockn +δ and (m, clockn )+δ analogously
as in the dense-time case. The discrete concrete state space of N is a structure
(T ∪ IN, Σn , σn 0 , →n ), where Σn is the set of all the discrete concrete states of
N , σn 0 = (m0 , clockn 0 ) with clockn 0 (t) = 0 for each t ∈ T is the initial state of
N , and →n ⊆ Σn × (T ∪ IN) × Σn is a timed consecution relation defined by:
δ
– for δ ∈ IN, (m, clockn ) →n (m, clockn + δ) iff (clockn + δ)(t) ≤ Lf t(t) for all
t ∈ en(m) (time successor),
t
– for t ∈ T , (m, clockn ) →n (m0 , clockn 0 ) iff t ∈ en(m), Ef t(t) ≤ clockn (t) ≤
Lf t(t), m = m[ti, and for all u ∈ T we have clockn 0 (u) = 0 for u ∈
0
newly_en(m, t) and clockn 0 (u) = clockn (u) otherwise (action successor).
Again, firing of a transition takes no time.
Given a set of propositional variables P V , we introduce valuation function
Vn : Σn → 2P V which assigns the same propositions to the states with the same
markings. Similarly as in the dense case, we assume the set P V to be such that
each q ∈ P V corresponds to exactly one p ∈ P , and use the same names for the
propositions and the places. The function Vn is then defined by p ∈ Vn (σn ) iff
p ∈ m for each σn = (m, ·). The structure Mn (N ) = (T ∪ IN, Σn , σn 0 , →n , Vn ) is
a discrete concrete model of N .
20 PNSE’12 – Petri Nets and Software Engineering
a
A discrete σn -run of TPN N is a (maximal) sequence of states: σn0 →0 n
a a
σn1 →1 n σn2 →2 n . . ., where σn0 = σn ∈ Σn and ai ∈ T ∪IN for each i ≥ 0. A state
a a a
σn is reachable in Mn (N ) iff there is a σn 0 -run of N σn0 →0 n σn1 →1 n σn2 →2 n . . .
such that σn = σni for some i ∈ IN.
4 Temporal Logics ACTL∗ and ECTL∗
In our work we deal with verification of properties of time Petri nets expressed
in certain sublogics of the standard branching time logic CTL∗ . Below, we define
the logics of our interest.
4.1 Syntax and Sublogics of CTL∗
Let P V = {℘1 , ℘2 . . .} be a set of propositional variables. The language of CTL∗
is given as the set of all the state formulas ϕs (interpreted at states of a model),
defined using path formulas ϕp (interpreted along paths of a model), by the
following grammar:
ϕs := ℘ | ¬ϕs | ϕs ∧ ϕs | ϕs ∨ ϕs | Aϕp | Eϕp
ϕp := ϕs | ϕp ∧ ϕp | ϕp ∨ ϕp | Xϕp | U(ϕp , ϕp ) | R(ϕp , ϕp ).
In the above ℘ ∈ P V , A (’for All paths’) and E (’there Exists a path’) are path
quantifiers, whereas U (’Until’) and R (’Release’) are state operators. Intuitively,
the formula Xϕp specifies that ϕp holds in the next state of the path, whereas
U(ϕp , ψp ) expresses that ψp eventually occurs and that ϕp holds continuously
until then. The operator R is dual to U: the formula R(ϕp , ψp ) says that either
ψp holds always or it is released when ϕp eventually occurs. Derived operators
def def def
are defined as Gϕp = R(f alse, ϕp ) and Fϕp = U(true, ϕp ), where true =
def
℘ ∨ ¬℘, and f alse = ℘ ∧ ¬℘ for an arbitrary ℘ ∈ P V . Intuitively, the formula
Fϕp specifies that ϕp occurs in some state of the path (’Finally’), whereas Gϕp
expresses that ϕp holds in all the states of the path (’Globally’).
Next, we define some sublogics of CTL∗ :
ACTL∗ : the fragment of CTL∗ in which the state formulas are restricted such
that negation can be applied to propositions only, and the existential quan-
tifier E is not allowed,
ECTL∗ : the fragment of CTL∗ in which the state formulas are restricted such
that negation can be applied to propositions only, and the universal quanti-
fier A is not allowed,
ACTL : the fragment of ACTL∗ in which the temporal formulas are restricted
to positive boolean combinations of A(ϕUψ), A(ϕRψ), and AXϕ only.
ECTL : the fragment of ECTL∗ in which the temporal formulas are restricted
to positive boolean combinations of E(ϕUψ), E(ϕRψ) and EXϕ only.
L−X denotes the logic L without the next-step operator X.
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 21
4.2 Semantics of CTL∗
Let P V be a set of propositions. A model for CTL∗ is a tuple 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 relation5 , and V : S −→ 2P V is a valuation
function. For s, s0 ∈ S the notation s→s0 means that there is l ∈ L such that
l
s → s0 . Moreover, for s0 ∈ S a path π = (s0 , s1 , . . .) is an infinite sequence of
states in S starting at s0 , where si →si+1 for all i ≥ 0, πi = (si , si+1 , . . .) is the
i-th suffix of π, and π(i) = si .
Given a model M , a state s, and a path π of M , by M, s |= ϕ (M, π |= ϕ) we
mean that ϕ holds in the state s (along the path π, respectively) of the model
M . The model is sometimes omitted if it is clear from the context. The relation
|= is defined inductively as follows:
M, s |= ℘ iff ℘ ∈ V (s), for ℘ ∈ P V,
M, s |= ¬℘ iff M, s 6|= ℘, for ℘ ∈ P V,
M, x |= ϕ ∧ ψ iff M, x |= ϕ and M, x |= ψ, for x ∈ {s, π},
M, x |= ϕ ∨ ψ iff M, x |= ϕ or M, x |= ψ, for x ∈ {s, π},
M, s |= Aϕ iff M, π |= ϕ for each path π starting at s,
M, s |= Eϕ iff M, π |= ϕ for some path π starting at s,
M, π |= ϕ iff M, π(0) |= ϕ, for a state formula ϕ,
M, π |= Xϕ iff M, π1 |= ϕ,
M, π |= ϕUψ iff (∃j ≥ 0) M, πj |= ψ and (∀0 ≤ i < j) M, πi |= ϕ ,
M, π |= ϕRψ iff (∀j ≥ 0) M, πj |= ψ or (∃0 ≤ i < j) M, πi |= ϕ .
Moreover, we assume M |= ϕ iff M, s0 |= ϕ, where s0 is the initial state of M .
4.3 Equivalence Preserving ACTL∗ and ECTL∗
Let M = (L, S, s0 , →, V ) and M 0 = (L0 , S 0 , s00 , →0 , V 0 ) be two models.
Definition 2 ([2]). A relation ;sim ⊆ S 0 × S is a simulation from M 0 to M if
the following conditions hold:
• s00 ;sim s0 ,
• for each s ∈ S and s0 ∈ S 0 , if s0 ;sim s, then V (s) = V 0 (s0 ), and for every
0
l l0
s1 ∈ S such that s → s1 for some l ∈ L, there is s01 ∈ S 0 such that s0 → s01
for some l0 ∈ L0 and s01 ;sim s1 .
The model M 0 simulates M (M 0 ;sim M ) if there is a simulation from M 0 to M .
The models M , M 0 are simulation equivalent iff M ;1sim M 0 and M 0 ;2sim M
for some simulations ;1sim ⊆ S × S 0 and ;2sim ⊆ S 0 × S. Two models M and
M 0 are called bisimulation equivalent if M 0 ;sim M and M (;sim )−1 M 0 , where
(;sim )−1 is the inverse of ;sim .
5
Totality means that (∀s ∈ S)(∃s0 ∈ S) s→s0 .
22 PNSE’12 – Petri Nets and Software Engineering
The following theorem holds:
Theorem 1 ([2]). Let M , M 0 be two simulation equivalent models, where the
range of the valuation functions V, V 0 is 2P V . Then, M, s0 |= ϕ iff M 0 , s00 |= ϕ,
for any formula ϕ over P V such that ϕ ∈ ACTL∗ ∪ ECTL∗ .
5 Discrete- vs. Dense-Time Verification for ACTL∗ and
ECTL∗
It is easy to see that both the models Mr (N ) and Mn (N ) can be used in ACTL∗
and ECTL∗ verification for a net with the semantics a given model corresponds
to (as both meet the definition of the model for CTL∗ ). However, it is also
not difficult to see that the second model is smaller and less prone to the state
explosion problem. The aim of our work is then to show that both the models
are equivalent w.r.t. checking ACTL∗ and ECTL∗ properties of time Petri nets
with the dense-time semantics. In our proof we make use of the approach of
Popova presented in the paper [5].
Consider the dense concrete model Mr (N ) = (T ∪ IR+ , Σ, σ 0 , →r , V ) of a
TPN N . A state σ = (m, clock) ∈ Σ is called an integer-state if clock(t) ∈ IN for
a a a
all t ∈ T . A integer σ-run of N is a sequence of states σ0 →0 r σ1 →1 r σ2 →2 r . . .,
where σ0 = σ ∈ Σ and ai ∈ T ∪ IN for each i ≥ 0. Note that all the states of an
integer-run which starts at an integer-state are integer-states as well. Thus, it is
easy to see that the following holds:
Lemma 1. For a given time Petri net N the model Mr (N ) reduced to the
integer-states and the transition relation between them is equal to Mn (N ).
Given a number x ∈ IR+ , let bxc denote the floor of x, i.e., the greatest a ∈ IN
such that a ≤ x, and let dxe denote the ceiling of x, i.e. the smallest a ∈ IN such
that x ≤ a. Moreover, let f ire(σ) denote a set of transition that are ready to fire
in the state σ ∈ Σ, i.e., f ire(σ) = {t ∈ en(m) | clock(t) ∈ [Ef t(t), Lf t(t)]}. We
define the integer-states to be neighbour states of real-valued ones as follows:
Definition 3 (Neighbour states). Let σ = (m, clock) be a state of a TPN N .
An integer-state σ 0 = (m0 , clock 0 ) is a neighbour state of σ (denoted σ 0 ∼n σ) iff
– m0 = m,
– for each t ∈ en(m), bclock(t)c ≤ clock 0 (t) ≤ dclock(t)e.
Intuitively, a neighbour state of σ is an integer-state of the same marking, and
such that the values of its clocks, for all the enabled transitions, are “in a neigh-
bourhood” of these of σ. However, it is easy to see that these values can be such
that they make more transitions ready to fire than the corresponding values in σ
do: each transition t which can be fired at a given value of clock(t) can be fired
both at bclock(t)c and at dclock(t)e since all these three values are either equal
if clock(t) is a natural number, or belong to the same (integer-bounded) interval
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 23
[Ef t(t), Lf t(t)] if clock(t) 6∈ IN; on the other hand, a transition t0 which is not
ready to fire at clock(t0 ) can be firable at dclock(t0 )e if dclock(t0 )e = Ef t(t0 ).
This implies f ire(σ) ⊆ f ire(σ 0 ).
a a
Let π := σ0 →0 r σ1 →1 r . . . be a σ 0 -run in Mr (N ). By π[k] , for k ∈ IN, we
a a ak−1
denote the prefix σ0 →0 r σ1 →1 r . . . → r σk of π, and by π(k) - the k-th state
a
of π, i.e., σk . Moreover, we assign a time δi to each step σi →i r σi+1 in the run,
i.e., define δi = ai if ai ∈ IR, and δi = 0 otherwise. By ∆G (σi , π), for i ∈ IN,
i−1
we denote the value Σj=0 δi (i.e., the time passed along π before reaching σi ).
b b b
Moreover, given k ∈ IN and a π(k)-run ρ := σk →
0
r β1 →r β2 →r . . ., by π[k] · ρ
1 2
a a ak−1 b b b
we denote the run σ0 →0 r σ1 →1 r . . . → r σk →
0
r β1 →r β2 →r . . . (i.e, the run
1 2
obtained by “joining” π[k] and ρ). The above definitions apply to discrete runs in
an analogous way. Next, we introduce the following definition (see also Fig. 2):
σ0 a0 σ1 a1 σ2 σk−2 a σk−1 a σk
k−2 k−1
π:
a 0’ a1’ a’k−2 a’k−1
π ’:
σ0’ σ1’ σ2’ ’
σk−2 ’
σk−1 σ ’k
0
Fig. 2. Neighbour prefix of π[k] (denoted π[k] ). If ai ∈ T , then a0i = ai ; the states of
0
π[k] and π[k] related by ∼n are linked by dashed lines.
a a
Definition 4 (Neighbour prefix). Let π := σ0 →0 r σ1 →1 r . . . be a run in
a00 a01
Mr (N ), and let π 0 := σ00 →r σ10 →r . . . be an integer run. For k ∈ IN, the prefix
0
π[k] is a neighbour prefix of π[k] (denoted π[k]0
∼n π[k] ) iff for each i = 0, . . . , k
it holds
– σi0 ∼n σi ,
– ai ∈ T iff a0i ∈ T , and if ai , a0i ∈ T then a0i = ai .
Intuitively, a neighbour prefix “visits” neighbour states of these in π[k] , and the
corresponding steps of these prefixes are either both firings of the same transition,
or both passages of time (possibly of different lengths).
In order to show that Mn (N ) can replace Mr (N ) in ACTL∗ /ECTL∗ verifi-
cation we shall prove the following lemma:
Lemma 2. The models Mr (N ) and Mn (N ) are simulation equivalent.
Proof. It is obvious from Lemma 1 that Mr (N ) simulates Mn (N ), with the
relation R1 ⊆ Σ × Σn defined as R1 = {(σ, σ 0 ) | σ = σ 0 }.
24 PNSE’12 – Petri Nets and Software Engineering
Let Rr (N ) and Rn (N ) denote respectively the sets of all the dense σ 0 -runs
(discrete σn 0 -runs) of the net N . In order to prove that Mn (N ) ;sim Mr (N )
we shall show that the relation R ⊆ Σn × Σ given by
R = {(σ 0 , σ) | ∃π ∈ Rr (N ) ∃π 0 ∈ Rn (N ) ∃k ∈ IN s.t.
σ = π(k) ∧ σ 0 = π 0 (k) ∧ π[k]
0
∼n π[k] ∧ ∀j≤k ∆G (σj0 , π 0 ) = b∆G (σj , π)c}
is a simulation from Mn (N ) to Mr (N ). Intuitively, the states σ, σ 0 are related
by R if they both are reachable from the initial state of N in k steps for some
natural k, on runs π, π 0 such that π[k] 0
is a neighbour prefix of π[k] and for each
j ≤ k the total time passed along π[j] is the floor of that passed along π[j] .
0
It is obvious that (σn 0 , σ 0 ) ∈ R due to equality of these states. Next, consider
σ, σ 0 such that (σ 0 , σ) ∈ R. Assume that the runs “justifying” this relation (for
a a a0 a0
some k) are of the form π := σ0 →0 r σ1 →1 r . . . and π 0 := σn0 = σ00 →0 n σ10 →1 n . . .
respectively, and that σi = (mi , clock i ), σi0 = (m0i , clock 0i ) for each i ∈ IN (which
implies also the notation σ = (mk , clock k ) and σ 0 = (m0k , clock 0k ) used below).
t
– if σ →r γ for a transition t ∈ T and a state γ = (mγ , clock γ ), then from
σ 0 ∼n σ (and therefore f ire(σ) ⊆ f ire(σ 0 )) the transition t can be fired
at σ 0 as well, leading to a state ξ = (mξ , clock 0ξ ). Let ρ be a σ-run of the
t t
form σ →r γ →r . . . (i.e., a σ-run whose first step is σ →r γ), and let ρ0
t
be a σ 0 -run of the form σ 0 →n ξ →n . . . (i.e., a σ 0 -run whose first step is
t
σ 0 →n ξ; see Fig. 3). We shall show that (π[k]
0
· ρ0 )[k+1] ∼n (π[k] · ρ)[k+1] and
ρ
π [k]
γ
σ0 σ1 α = σh σ = σk
π:
ρ’
π’[k]
ξ
δ’
σ0’ σ1’ α’= σ h’ σ ’ = σ k’
π’:
Fig. 3. Relation between π, π 0 , ρ and ρ0 in the proof of Lemma 2.
that ∆G (ξ, π[k]
0
· ρ0 ) = b∆G (γ, π[k] · ρ)c.
• In order to prove (π[k] 0
· ρ0 )[k+1] ∼n (π[k] · ρ)[k+1] it is sufficient to show
that ξ ∼n γ. It is obvious that the markings mγ and mξ are equal, and
that newly_en(mk , t) = newly_en(m0k , t). Next, consider t0 ∈ en(mγ ).
If t0 6∈ newly_en(mk , t) then the value of its clock in γ is the same as in σ
(since firing of t does not influence the value of the clock of t0 ). In turn, if
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 25
t0 ∈ newly_en(mk , t) then the values of its clock in γ and in ξ are equal
to 0. Thus, from the fact that for σ, σ 0 we have bclock k (t)c ≤ clock 0k (t) ≤
dclock k (t)e we have also bclock γ (t)c ≤ clock 0ξ (t) ≤ dclock γ (t)e, which
implies ξ ∼n γ.
• the condition ∆G (ξ, π[k] 0
· ρ0 ) = b∆G (γ, π[k] · ρ)c holds in an obvious way
(∆G (ξ, π[k]
0
· ρ0 ) = ∆G (σ 0 , π 0 ) = b∆G (σ, π)c = b∆G (γ, π[k] · ρ)c as the step
consisting in firing a transition is assigned the time 0).
δ
– if σ →r γ for a time δ ∈ IR+ and a state γ = (mγ , clock γ ), then let ρ be a
δ · δ
σ-run σ →r γ →r . . . (i.e., a σ-run of the first step σ →r γ; see Fig. 3), and
a a ak−1 δ
let π[k] · ρ denote the run σ0 →0 r σ1 →1 r . . . → r σk →r γ →r . . . (i.e, the
run obtained by “joining” π[k] and ρ). Next, assume
δ 0 = b∆G (γ, π[k] · ρ)c − ∆G (σ 0 , π 0 )
(which is an integer value due to ∆G (σ 0 , π 0 ) ∈ IN). We shall show first that
the time δ 0 can pass at σ 0 , leading to a state ξ = (mξ , clock 0ξ ).
• To show that δ 0 can pass at σ 0 notice that
δ = ∆G (γ, π[k] · ρ) − ∆G (σ, π[k] · ρ),
and that
∆G (σi , π) = ∆G (σi , π[k] · ρ) for each i = 0, . . . , k.
Moreover, we have that clock γ (t) = clock k (t) + δ ≤ Lf t(t) for each
t ∈ en(mk ).
Consider a transition t ∈ en(m0k ) (where en(m0k ) = en(mk ) = en(mγ )).
Let h be an index along π[k] pointing to a state (denoted α) at which t
became enabled most recently, and let h0 be an index along π[k] 0
pointing
to a state (denoted α0 ) at which t became enabled most recently. From
the fact that π[k]
0
∼n π[k] we have h = h0 (for each j ≤ k − 1 the
corresponding j-th steps of π[k] and π[k] 0
are either both firings of the
same transition or both time passings, which implies that for each i ≤ k
a transition t becomes enabled in π(i) iff it becomes enabled in π 0 (i)).
From the definitions of clock, clock 0 it is easy to see that
clock k (t) = ∆G (σ, π) − ∆G (α, π),
clock γ (t) = ∆G (γ, π[k] · ρ) − ∆G (α, π)
and
clock 0k (t) = ∆G (σ 0 , π 0 ) − ∆G (α0 , π 0 )
Moreover, it holds
clock 0k (t) + δ 0 = ∆G (σ 0 , π 0 ) − ∆G (α0 , π 0 ) + δ 0 =
∆G (σ 0 , π 0 ) − ∆G (α0 , π 0 ) + b∆G (γ, π[k] · ρ)c − ∆G (σ 0 , π 0 ) =
def. of R and h=h0
b∆G (γ, π[k] ·ρ)c−∆G (α0 , π 0 ) = b∆G (γ, π[k] ·ρ)c−b∆G (α, π)c.
26 PNSE’12 – Petri Nets and Software Engineering
From clock γ (t) ≤ Lf t(t) we have dclock γ (t)e ≤ Lf t(t), and from the
property bac − bbc ≤ da − be we get
clock 0k (t) + δ 0 = b∆G (γ, π[k] · ρ)c − b∆G (α, π)c ≤ d∆G (γ, π[k] · ρ) −
∆G (α, π)e = dclock γ (t)e ≤ Lf t(t);
Thus, we have that clock 0k (t) + δ 0 ≤ Lf t(t) for each t ∈ en(m0k ), and
therefore the time δ 0 can pass at σ 0 .
δ0
Next, let ρ0 be a σ 0 -run of the form σ 0 →n ξ →n . . .. We shall show that
0
(π[k] · ρ0 )[k+1] ∼n (π[k] · ρ)[k+1] and that ∆G (ξ, π[k]
0
· ρ0 ) = b∆G (γ, π[k] · ρ)c.
• In order to prove (π[k]
0
· ρ0 )[k+1] ∼n (π[k] · ρ)[k+1] it is sufficient to show
that ξ ∼n γ. It is obvious that the markings of these states are equal.
Consider t ∈ en(m). We show that bclock γ (t)c ≤ clock 0ξ (t) ≤ dclockγ (t)e.
Let α, α0 , h, h0 be defined as in the previous part of the proof (see the
8th line of the previous item). Similarly as before, from the definitions
of clock, clock 0 we have that
clock γ (t) = ∆G (γ, π[k] · ρ) − ∆G (α, π),
and that
clock 0ξ (t) = ∆G (σ 0 , π 0 ) + δ 0 − ∆G (α0 , π 0 ).
∗ From the property ba − bc ≤ bac − bbc (for a, b ∈ IR+ with a ≥ b) we
have
bclock γ (t)c = b∆G (γ, π[k] · ρ) − ∆G (α, π)c ≤ b∆G (γ, π[k] · ρ)c −
h=h0 and def. of R
b∆G (α, π)c = b∆G (γ, π[k] ·ρ)−∆G (σ 0 , π 0 )+∆G (σ 0 , π 0 )c−
∆G (α0 , π 0 ) = b∆G (γ, π[k] ·ρ)c−∆G (σ 0 , π 0 )+∆G (σ 0 , π 0 )−∆G (α0 , π 0 ) =
δ 0 + ∆G (σ 0 , π 0 ) − ∆G (α0 , π 0 ) = clock 0ξ (t).
∗ From the property bac − bbc ≤ da − be we have
clock 0k (t) + δ 0 = b∆G (γ, π[k] · ρ)c − b∆G (α, π)c ≤ d∆G (γ, π[k] · ρ) −
∆G (α, π)e = dclock γ (t)e
• Next, we have ∆G (ξ, π[k] 0
·ρ0 ) = ∆G (σ 0 , π 0 )+δ 0 = ∆G (σ 0 , π 0 )+b∆G (γ, π[k] ·
ρ)c − ∆G (σ 0 , π 0 ) = b∆G (γ, π[k] · ρ)c, which ends the proof.
Therefore, we can formulate the following theorem:
Theorem 2. Let Mr (N ) and Mn (N ) be respectively a dense and a discrete
model for a time Petri net N , and let ϕ be an ACTL∗ (ECTL∗ ) formula. The
following condition holds:
Mr (N ) |= ϕ iff Mn (N ) |= ϕ.
Proof. Follows from Theorem 1 and Lemma 2 in a straightforward way.
It should also be explained that in the case of timed systems (and therefore
also TPNs) with the dense-time semantics, logics without the next-step operator
are usually used, due to problems with intepreting the “next” step in the case
of continuous time. However, Thm. 2 considers more general logics, in case one
would interpret the next-step operator over an arbitrary passage of time.
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 27
p1 p2
t1 [0,1] t2 [1,2]
Fig. 4. A net
It should be noticed that the relation R used in our proof cannot be used to
prove bisimulation between the models, i.e., their equivalence w.r.t. the CTL∗
properties, since the integer run π 0 “justifying” σ 0 Rσ and the dense run π oc-
curring in the relation do not need to “branch” in the same way. Thus, although
one can prove that each transition t which can be fired at σ can be fired at σ 0
as well, the reverse does not hold. To see an example of the above consider the
net shown in Fig. 4 and its runs:
– the dense one:
0.5 t1 0.6
π := (p1 , (0, 0)) →r (p1, (0.5, 0)) →r (p2, (0, 0)) →r (p2, (0, 0.6)) →r . . .
– and the discrete one (denoted π 0 ), built in the way shown in [5] and used in
our proof in the definition of R (i.e., satisfying π[3]
0
∼n π[3] and ∆G (σj0 , π 0 ) =
b∆G (σj , π)c for each j ≤ 3):
0 t1 1
π 0 := (p1 , (0, 0)) →n (p1, (0, 0)) →n (p2, (0, 0)) →n (p2, (0, 1)) →n . . ..
It is easy to see that in π(3) we have clock(t2) = 0.6, which means that t2 cannot
be fired at this state, while in π 0 (3) we have clock(t2) = 1, which means that
the transition t2 is firable.
6 Experimental Results
In order to show that using discrete-time models instead of the dense ones can
be profitable, we performed some tests, using as an example an implementation
of SAT-based bounded model checking (BMC) for a subclass of TPNs (i.e., dis-
tributed time Petri nets) with the discrete-time semantics and the logic ACTL−X
used in [4], and its modification for the dense-time case prepared for the current
paper. BMC is a technique applied mainly to searching for counterexamples for
universal properties, using a model truncated up to some specific depth k. The
formulas used by the method are then negations of these expressing properties
to be tested. So, in our case they are formulas of ECTL−X .
The first system we consider is the Generic Pipeline Paradigm Petri net
model (GTPP) shown in Fig. 5. It consists of three parts: Producer producing
data (P rodReady) or being inactive, Consumer receiving data (ConsReady) or
being inactive, 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 by adding more intermediate nodes.
The parameters a, b, c, d, e, f are used to adjust the time properties of Pro-
ducer, Consumer, and of the intermediate Nodes. The formulas considered are
EGEFConsReceived, EG(P rodReady ∨ ConsReady) and EFN ode1 Send.
28 PNSE’12 – Petri Nets and Software Engineering
ProdReady Node1Ready Node2Ready NodenReady ConsReady
[c, d] [c, d] [c, d] [c, d] [c, d]
[a, b] [a, b]
Node1Proc Node2Proc NodenProc
[e, f ] [e, f ] [e, f ]
Node1Send Node2Send NodenSend
Fig. 5. A net for Generic Timed Pipeline Paradigm
The next system tested is the standard Fischer’s mutual exclusion protocol
(Mutex). The system consists of n time Petri nets, each one modelling a process,
plus one additional net used to coordinate the access of the processes to the
critical sections. A TPN modelling the system for n = 2 is presented in Fig. 6
In this case we have tested the formula EGEF(crit1 ∨ . . . ∨ critn ).
setx0_1
[0, ∞)
setx1
[0, ∆]
critical1
idle1 start1 trying1 setx1−copy1
[0, ∆] enter1
[0, ∞) [δ, ∞)
waiting1
[0, ∆]
setx1−copy2
place 1
place 0
place 2
setx2−copy2
[0, ∆]
start2
[0, ∞) [0, ∆] enter2
idle2 trying2 setx2−copy1 waiting2 critical2
[δ, ∞)
[0, ∆]
setx2
setx0_2[0, ∞)
Fig. 6. A net for Fischer’s mutual exclusion protocol for n = 2
The results are presented in Fig. 7–9 for GTPP, and in Fig. 10 for Mutex. It
can be seen that in all the cases we are able to verify systems containing more
components (indicated in the column n) than when discrete models are used,
and the total time (bmcT +satT ) and the memory required (max(bmcM, satM ))
are usually smaller for the discrete-time case (the columns with “IN :”). In some
cases the differences are quite substantial, but there are also examples in which
the time and the memory used are similar for both the semantics. However, one
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 29
n k LL IR: bmcT+satT IR: max(bmcM,satM) IN: bmcT+satT IN: max(bmcM,satM)
1 5 7 1.41 12.00 0.20 8.00
2 7 9 9.94 25.00 1.15 12.00
3 9 11 49.45 60.00 3.55 21.00
4 11 13 154.70 146.00 9.94 38.00
5 13 15 310.18 243.00 20.90 61.00
6 15 17 708.66 313.00 41.43 94.00
7 17 19 1934.63 818.00 76.81 145.00
8 19 21 4121.60 1071.00 131.98 215.00
9 21 23 6819.25 1640.00 237.21 314.00
10 23 25 20519.20 3455.00 361.03 377.00
11 25 27 - - 562.15 552.00
Fig. 7. Comparison of the results for GTPP and the formula EGEFConsReceived
n k LL IR: bmcT+satT IR: max(bmcM,satM) IN: bmcT+satT IN: max(bmcM,satM)
1 5 1 0.41 7.00 0.17 7.00
2 7 1 4.14 12.00 0.76 8.00
3 9 1 32.27 29.00 2.20 9.00
4 11 1 63.28 52.00 8.57 12.00
5 13 1 200.14 151.00 21.14 17.00
6 15 1 488.59 165.00 43.18 24.00
7 17 1 870.21 342.00 105.18 38.00
8 19 1 1870.65 415.00 234.00 54.00
9 21 1 3745.33 658.00 763.84 139.00
10 23 1 7097.01 1364.00 1696.58 283.00
11 25 1 - - 3013.98 306.00
Fig. 8. Comparison of the results: GTPP, the formula EG(P rodReady ∨ ConsReady)
can see that the noticeable differences occur in the cases in which the length of
the witness for the formula (k) or the number of paths required to check this
formula (LL) grow together with the size of the system, making the verification
more expensive.
7 Conclusions and Further Work
We have shown that the result of Popova, stating that integer time steps are
sufficient to test reachability of markings in time Petri nets, can be extended
to testing ECTL∗ and ACTL∗ properties. We have focused on 1-safe TPNs for
simplicity of the presentation, but it is easy to see that the result applies also to
“general” time Petri nets: neither the definitions of a marking and of enabledness
of a transition, nor the way multiple enabledness of transitions is handled do
influence the proof.
30 PNSE’12 – Petri Nets and Software Engineering
n k LL IR: bmcT+satT IR: max(bmcM,satM) IN: bmcT+satT IN: max(bmcM,satM)
100 2 1 2.02 23.00 1.60 19.00
200 2 1 7.04 76.00 5.74 51.00
300 2 1 15.03 153.00 12.15 102.00
400 2 1 26.30 270.00 18.59 179.00
500 2 1 40.50 412.00 28.47 273.00
600 2 1 58.71 563.00 40.45 397.00
700 2 1 79.71 738.00 54.69 537.00
800 2 1 104.84 992.00 72.06 654.00
900 2 1 133.78 1173.00 90.48 854.00
1000 2 1 169.19 1528.00 114.86 1005.00
1100 2 1 211.16 1772.00 140.22 1168.00
1200 2 1 - - 168.86 1506.00
1300 2 1 - - 203.24 1604.00
Fig. 9. Comparison of the results: GTPP, the formula EFN ode1Send
n k LL IR: bmcT+satT IR: max(bmcM,satM) IN: bmcT+satT IN: max(bmcM,satM)
24 5 1.04 11.00 0.74 10.00
34 5 1.77 13.00 1.10 12.00
44 5 1.83 15.00 1.63 14.00
54 5 3.18 17.00 2.41 16.00
10 4 5 9.15 40.00 7.20 31.00
20 4 5 26.14 90.00 18.76 86.00
30 4 5 74.70 177.00 58.56 161.00
40 4 5 258.34 330.00 108.34 320.00
50 4 5 265.06 419.00 170.93 358.00
60 4 5 710.11 732.00 442.42 713.00
70 4 5 701.81 1092.00 728.20 1073.00
80 4 5 919.34 1001.00 2288.34 1349.00
90 4 5 780.89 1161.00 934.72 1140.00
100 4 5 4566.16 3181.00 4230.64 4549.00
110 4 5 4260.76 3414.00 4956.38 3237.00
120 4 5 - - 4217.44 3238.00
130 4 5 - - 2155.04 2571.00
140 4 5 - - 5087.76 3603.00
Fig. 10. Comparison of the results: mutex, the formula EGEF(crit1 ∨ . . . ∨ critn )
Our experimental results show that considering the discrete semantics while
verifying properties of dense-time nets can be profitable. Due to this, in our
further work we are going to check whether discrete-time semantics can be used
when testing other classes of properties of the dense-time Petri net systems (e.g.,
CTL∗−X ).
A. Janowska et al.: Checking Branching Time Properties of Time Petri Nets 31
References
1. U. Goltz, R. Kuiper, and W. Penczek. Propositional temporal logics and equiv-
alences. In Proc. of the 3rd Int. Conf. on Concurrency Theory (CONCUR’92),
volume 630 of LNCS, pages 222–236. Springer-Verlag, 1992.
2. O. Grumberg and D. E. Long. Model checking and modular verification. In Proc.
of the 2nd Int. Conf. on Concurrency Theory (CONCUR’91), volume 527 of LNCS,
pages 250–265. Springer-Verlag, 1991.
3. A. Janowska, W. Penczek, A. Półrola, and A. Zbrzezny. Towards discrete-time
verification of time Petri nets with dense-time semantics. In Proc. of the Int. Work-
shop on Concurrency, Specification and Programming (CS&P’11), pages 215–228.
Bialystok University of Technology, 2011.
4. A. Mȩski, W. Penczek, A. Półrola, B. Woźna-Szcześniak, and A. Zbrzezny. Bounded
model checking approaches for verificaton of distributed time Petri nets. In Proc. of
the Int. Workshop on Petri Nets and Software Engineering (PNSE’11), pages 72–91.
University of Hamburg, 2011.
5. L. Popova. On time Petri nets. Elektronische Informationsverarbeitung und Kyber-
netik, 27(4):227–244, 1991.
6. L. Popova-Zeugmann. Essential states in time Petri nets. Informatik-Bericht 96,
Humboldt University, 1998.
7. L. Popova-Zeugmann. Time Petri nets state space reduction using dynamic pro-
gramming. Journal of Control and Cybernetics, 35(3):721–748, 2006.
8. L. Popova-Zeugmann and D. Schlatter. Analyzing paths in time Petri nets. Funda-
menta Informaticae, 37(3):311–327, 1999.