Verification of timed systems is an important subject of research, and one of its crucial aspects is the efficiency of the methods developed. 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 sufficient 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.
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 [
using an implementation for SAT-based bounded model checking of ACTL−X
and the class of distributed time Petri nets with the discrete-time semantics [
work. Sec. 3 introduces time Petri nets and their dense and discrete models.
2
Related Works
The topic of verification of dense-time Petri nets using integer time steps has
been studied in several publications. In paper [
just as their Ef t is reached. This way a reduced (finite) reachability graph of “essential” (integer) states is obtained.
In [
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 [
Time Petri Nets
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
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= ∅)}.
3.1
Dense-Time Semantics
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, clock0) with clock0(t) = 0 for each t ∈ T is the initial state of N , and →r⊆ Σ × (T ∪ IR+) × Σ is a timed consecution relation defined by: – for δ ∈ IR+, (m, clock) →δr (m, clock + δ) iff (clock + δ)(t) ≤ Lf t(t) for all t ∈ en(m) (time successor), – for t ∈ T , (m, clock) →tr (m0, clock0) iff t ∈ en(m), Ef t(t) ≤ clock(t) ≤ Lf t(t), m0 = m[ti, and for all u ∈ T we have clock0(u) = 0 for u ∈ newly_en(m, t) and clock0(u) = clock(u) otherwise (action successor).
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 . a0 a1 A dense σ-run of TPN N is a (maximal) sequence of states: σ0 →r σ1 →r a2 σ2 →r . . ., where σ0 = σ ∈ Σ and ai ∈ T ∪ IR+ for each i ≥ 0. A state σ is reachable in Mr(N ) if there is a dense σ0-run σ0 →a0 r σ1 →a1 r σ2 →a2 r . . . such that σ = σi for some i ∈ IN. 3.2
Discrete-Time Semantics Alternatively, one can consider integer time passings only. In such a discretetime 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, σn0, →n), where Σn is the set of all the discrete concrete states of N , σn0 = (m0, clockn0) with clockn0(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), – for t ∈ T , (m, clockn) →tn (m0, clockn0) iff t ∈ en(m), Ef t(t) ≤ clockn(t) ≤ Lf t(t), m0 = m[ti, and for all u ∈ T we have clockn0(u) = 0 for u ∈ newly_en(m, t) and clockn0(u) = clockn(u) otherwise (action successor).
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, σn0, →n, Vn) is a discrete concrete model of N .
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
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 are defined as Gϕp d=ef R(f alse, ϕp ) and Fϕp d=ef U(true, ϕp ), where true d=ef def ℘ ∨ ¬℘, and f alse = ℘ ∧ ¬℘ for an arbitrary ℘ ∈ P V . Intuitively, the formula
expresses that ϕp holds in all the states of the path (’Globally’).
to positive boolean combinations of A(ϕUψ), A(ϕRψ), and AXϕ only.
to positive boolean combinations of E(ϕUψ), E(ϕRψ) and EXϕ only. L−X denotes the logic L without the next-step operator X.
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 s →l 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
|= 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 .
Equivalence Preserving ACTL∗ and ECTL∗
Let M = (L, S, s0, →, V ) and M 0 = (L0, S0, s00, →0, V 0) be two models.
Definition 2 ([
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 ;s1im M 0 and M 0 ;s2im M for some simulations ;s1im⊆ S × S0 and ;s2im⊆ S0 × S. Two models M and M 0 are called bisimulation equivalent if M 0 ;sim M and M (;sim)−1M 0, where (;sim)−1 is the inverse of ;sim. 5 Totality means that (∀s ∈ S)(∃s0 ∈ S) s→s0.
Theorem 1 ([
Discrete- vs. Dense-Time Verification for ECTL∗ ACTL∗ and 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
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 a0 a1 a2 all t ∈ T . A integer σ-run of N is a sequence of states σ0 →r σ1 →r σ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, clock0) is a neighbour state of σ (denoted σ0 ∼n σ) iff – m0 = m, – for each t ∈ en(m), bclock(t)c ≤ clock0(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 neighbourhood” 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 [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).
Let π := σ0 →r σ1 →a1 r . . . be a σ0-run in Mr(N ). By π[k], for k ∈ IN, we a0 denote the prefix σ0 →r σ1 →a1 r . . . ak−1 a0 → r σk of π, and by π(k) - the k-th state ai of π, i.e., σk. Moreover, we assign a time δi to each step σ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, we denote the value Σji−=10δi (i.e., the time passed along π before reaching σi). Moreover, given k ∈ IN and a π(k)-run ρ := σk →r β1 →r β2 →b2 r . . ., by π[k] · ρ b0 b1 we denote the run σ0 →r σ1 →a1 r . . . a→k−1r σk →r β1 →r β2 →b2 r . . . (i.e, the run a0 b0 b1 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 σ’ 0 a0 a’ 0 σ1 a1 a’ 1 σ’ 1 σ2 σ’ 2 σk−2 ak−2 σk−1 ak−1 σk σk’−2 a’k−2
a’k−1 σk’−1 σ’ k – σi0 ∼n σi, – ai ∈ T iff a0i ∈ T , and if ai, a0i ∈ T then a0i = ai.
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∗ verification 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}.
(discrete σn0-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) ∧ π[0k] ∼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 π[0k] is a neighbour prefix of π[k] and for each j ≤ k the total time passed along π[0j] is the floor of that passed along π[j].
It is obvious that (σn0, σ0) ∈ R due to equality of these states. Next, consider σ, σ0 such that (σ0, σ) ∈ R. Assume that the runs “justifying” this relation (for a0 a0 some k) are of the form π := σ0 →a0 r σ1 →a1 r . . . and π0 := σn0 = σ00 →0 n σ10 →1 n . . . respectively, and that σi = (mi, clocki), σi0 = (m0i, clock0i) for each i ∈ IN (which implies also the notation σ = (mk, clockk) and σ0 = (m0k, clock0k) used below). – if σ →tr γ 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ξ, clock0ξ). Let ρ be a σ-run of the form σ →tr γ →r . . . (i.e., a σ-run whose first step is σ →tr γ), and let ρ0 be a σ0-run of the form σ0 →tn ξ →n . . . (i.e., a σ0-run whose first step is σ0 →tn ξ; see Fig. 3). We shall show that (π[0k] · ρ0)[k+1] ∼n (π[k] · ρ)[k+1] and π : σ0 π[k] α = σh π’[k] α’= σh’ σ = σk σ’= σk’ ρ ρ’ δ’ γ ξ that ΔG(ξ, π[0k] · ρ0) = bΔG(γ, π[k] · ρ)c.
• In order to prove (π[0k] · ρ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 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 bclockk(t)c ≤ clock0k(t) ≤ dclockk(t)e we have also bclockγ (t)c ≤ clock0ξ(t) ≤ dclockγ (t)e, which implies ξ ∼n γ. • the condition ΔG(ξ, π[0k] · ρ0) = bΔG(γ, π[k] · ρ)c holds in an obvious way (ΔG(ξ, π[0k] · ρ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 let π[k] · ρ denote the run σ0 →a0 r σ1 →a1 r . . . a→k−1r σ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ξ, clock0ξ).
• 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) = clockk(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 π[0k] pointing to a state (denoted α0) at which t became enabled most recently. From the fact that π[0k] ∼n π[k] we have h = h0 (for each j ≤ k − 1 the corresponding j-th steps of π[k] and π[0k] 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)).
clockk(t) = ΔG(σ, π) − ΔG(α, π), clockγ (t) = ΔG(γ, π[k] · ρ) − ΔG(α, π) clock0k(t) = ΔG(σ0, π0) − ΔG(α0, π0) and
clock0k(t) + δ0 = ΔG(σ0, π0) − ΔG(α0, π0) + δ0 = ΔG(σ0, π0) − ΔG(α0, π0) + bΔG(γ, π[k] · ρ)c − ΔG(σ0, π0) = bΔG(γ, π[k]·ρ)c−ΔG(α0, π0) def. of R=and h=h0 bΔG(γ, π[k]·ρ)c−bΔG(α, π)c. From clockγ(t) ≤ Lf t(t) we have dclockγ(t)e ≤ Lf t(t), and from the property bac − bbc ≤ da − be we get clock0k(t) + δ0 = bΔG(γ, π[k] · ρ)c − bΔG(α, π)c ≤ dΔG(γ, π[k] · ρ) − ΔG(α, π)e = dclockγ(t)e ≤ Lf t(t); Thus, we have that clock0k(t) + δ0 ≤ Lf t(t) for each t ∈ en(m0k), and therefore the time δ0 can pass at σ0.
Next, let ρ0 be a σ0-run of the form σ0 →δ0 n ξ →n . . .. We shall show that (π[0k] · ρ0)[k+1] ∼n (π[k] · ρ)[k+1] and that ΔG(ξ, π[0k] · ρ0) = bΔG(γ, π[k] · ρ)c. • In order to prove (π[0k] · ρ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 ≤ clock0ξ(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, clock0 we have that and that clockγ(t) = ΔG(γ, π[k] · ρ) − ΔG(α, π), clock0ξ(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 − bΔG(α, π)c h=h0and=def. of R 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) = clock0ξ(t). ∗ From the property bac − bbc ≤ da − be we have clock0k(t) + δ0 = bΔG(γ, π[k] · ρ)c − bΔG(α, π)c ≤ dΔG(γ, π[k] · ρ) − ΔG(α, π)e = dclockγ(t)e • Next, we have ΔG(ξ, π[0k]·ρ0) = ΔG(σ0, π0)+δ0 = ΔG(σ0, π0)+bΔG(γ, π[k]· ρ)c − ΔG(σ0, π0) = bΔG(γ, π[k] · ρ)c, which ends the proof.
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 ) |= ϕ.
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.
t2 [
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” σ0Rσ and the dense run π occurring 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:
π := (p1, (0, 0)) 0→.5r (p1, (0.5, 0)) →t1 r (p2, (0, 0)) 0→.6r (p2, (0, 0.6)) →r . . .
– and the discrete one (denoted π0), built in the way shown in [
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.,
distributed time Petri nets) with the discrete-time semantics and the logic ACTL−X
used in [
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 odeiReady), processing data (N odeiP roc), or sending data (N odeiSend). The example can be scaled by adding more intermediate nodes.
EGEFConsReceived, EG(P rodReady ∨ ConsReady) and EFN ode1Send.
ProdReady
Node1Ready
Node2Ready
NodenReady
ConsReady [a,b] [c,d] [c,d] [c,d] [c,d] [c,d] [a,b] Node1Proc [e,f] Node1Send
Node2Proc [e,f] Node2Send
NodenProc [e,f] NodenSend
(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). idle1
trying1 start1 [0,∞) place 0 idle2
start2 [0,∞) trying2 setx0_1 setx1 [0,∞) [0,Δ] setx1−copy1
[0,Δ] [0,Δ] setx1−copy2 setx2−copy2 [0,Δ] [0,Δ] setx2−copy1 waiting2 [0,Δ]setx2 setx0_2[0,∞) waiting1 place 1 place 2 enter1 [δ,∞)
critical1 enter2 [δ,∞) critical2
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 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. n k LL IR: bmcT+satT IR: max(bmcM,satM) IN: bmcT+satT IN: max(bmcM,satM)
CTL∗−X).