=Paper=
{{Paper
|id=Vol-1269/paper257
|storemode=property
|title=Time Process Equivalences for Time Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-1269/paper257.pdf
|volume=Vol-1269
|dblpUrl=https://dblp.org/rec/conf/csp/BushinV14
}}
==Time Process Equivalences for Time Petri Nets==
https://ceur-ws.org/Vol-1269/paper257.pdf
Time Process Equivalences for Time Petri Nets⋆
Dmitry Bushin1 and Irina Virbitskaite1,2
1
A.P. Ershov Institute of Informatics Systems, SB RAS
6, Acad. Lavrentiev avenue, 630090, Novosibirsk, Russia
2
Novosibirsk State University
2, Pirogov avenue, 630090, Novosibirsk, Russia
1 Introduction
In the core of every theory of systems lies a notion of equivalence between
systems: it indicates which particular aspects of systems behaviors are considered
to be observable. In concurrency theory, a variety of observational equivalences
has been promoted, and the relationships between them have been quite well-
understood.
In order to investigate the performance of systems (e.g. the maximal time
used for the execution of certain activities and average waiting time for certain
requests), many time extensions have been de ned for a non-interleaving model
of Petri nets. On the other hand, there are few mentions of a fusion of timing
and partial order semantics, in the Petri net literature. In [9], processes of timed
Petri nets (under the asap hypothesis) have been de ned by an algebra of the
so-called weighted pomsets. The paper [8] has provided and compared timed
step sequence and timed process semantics for timed Petri nets. A method to
compute all valid timings for a causal net process of a time Petri net has been
put forward in [3]. Branching processes (unfoldings) of time Petri nets have been
constructed in [7].
To the best of our knowledge, the incorporation of timing into equivalence
notions on Petri nets is even less advanced. In this regard, the paper [4] is a wel-
come exception, where the testing approach has been extended to Petri nets with
associating clocks to tokens and time intervals to arcs from places to transitions.
A comparison of dierent subclasses of time Petri nets has been made in [5],
on the base of timed interleaving language and bisimulation equivalences. The
papers [1,2] contributed to the classi cation of the wealth of observational equiv-
alences of linear time branching time spectrum, based on interleaving, causal
tree and partial order semantics, for dense time extensions of event structures
with/without internal actions.
The intention of the note is towards developing, studying and comparing
trace and bisimulation equivalences based on interleaving, step, partial order, and
net-process semantics in the setting of time Petri nets (elementary net systems
enriched with the time static intervals on transitions, and with some niteness
⋆
This work is supported in part by DFG-RFBR (project CAVER, grants BE 1267/14-
1 and 14-01-91334)
requirements). This is an extension of the paper [6] to (causal and occurrence)
net-process and event structure semantics of the equivalences.
2 Time Petri Nets
In this section, we de ne some terminology concerning time Petri nets [3].
The domain T of time values is the set of natural numbers. We denote by
[τ1 , τ2 ] the closed interval between two time values τ1 , τ2 ∈ T, and by Interv the
set of all such intervals. In nity is allowed at the upper bound. An interval can
be of zero length, i.e. τ1 = τ2 , containing only a single time value. We use Act
to denote an alphabet of actions.
De nition 1. A (labeled over Act) time Petri net is a tuple T N = ((P , T , F ,
M0 , L), D), where (P, T, F, M0 , L) is a Petri net with a set P of places, a set
T of transitions (P ∩ T = ∅), a ow relation F ⊆ (P × T ) ∪ (T × P ), an initial
marking M0 ⊆ P , a labeling function L : T → Act, and D : T → Interv is a
static timing function associating with each transition a time interval.
For x ∈ P ∪ T , let • x = {y | (y, x) ∈ F } and x• = {y | (x, y) ∈ ∪ F } •be
the preset and
∪ postset of x , respectively. For X ⊆ P ∪ T , de ne •
X = x∈X x
and X • = x∈X x• . For a transition t ∈ T , the boundaries of the interval
D(t) ∈ Interv are called earliest ring time Ef t and latest ring time Lf t of t.
A marking M of T N is any subset of P . A transition t is enabled at a marking
M if • t ⊆ M (all its input places have tokens in M ), otherwise the transition is
disabled. Let En(M ) be the set of transitions enabled at M .
Consider the behavior of a time Petri net T N . A state of T N is a triple
(M, I, GT ), where M is a marking, I : En(M ) −→ T is a dynamic timing
function, and GT ∈ T is a global time moment. The initial state of T N is a
triple S0 = (M0 , I0 , GT0 ), where I0 (t) = 0, for all t ∈ En(M0 ), and GT0 = 0.
We call a non-empty subset U ⊆ T a step enabled at a state S = (M, I, GT ),
if (∀t ∈ U ⋄ t ∈ En(M )) and (∀t ̸= t′ ∈ U ⋄ • t ∩ • t′ = ∅). A step U ⊆ T
enabled at a state S = (M, I, GT ) is reable from S after a delay time θ ∈ T
if (∀t ∈ U ⋄ Ef t(t) ≤ I(t) + θ) and (∀t′ ∈ En(M ) ⋄ I(t′ ) + θ ≤ Lf t(t′ )). Let
Contact(S) = {t ∈ U | U is a step reable from a state S = (M, I, GT ) after
some delay time θ ∈ T and (M \ • t) ∩ t• ̸= ∅)}.
The ring of a step U reable from a state S = (M, I, GT ) after a delay time
θ leads to the new state S ′ = (M ′ , I ′ , GT ′ ) given as follows:
(i) M ′ = (M \ • U ) ∪
U •,
I(t′ ) + θ, if t′ ∈ En(M \ • U ),
′ ′ ′
(ii) ∀t ∈ T ⋄ I (t ) = 0, if t′ ∈ En(M ′ ) \ En(M \ • U ),
unde ned, otherwise,
(iii) GT ′ = GT + θ.
(U,θ) (A,θ)
In this case, we write S −→ S ′ , and, moreover, S −→ S ′ , if A = L(U ) =
∑ 0 (U1 ,θ1 ) 1 (U2 ,θ2 ) 2
t∈U L(t). A nite or in nite sequence of the form: S = S −→ S −→ S
?
p1 t p2 t
@
@
[0, 3] b @
R [1, 3] c ?[2, 3]
a
TN : t1 t3 t4
? ? ?
p3 p4 p5
Z
ZfZ
d ?[1, 1] ~= [0, 5]
t2 t5
?
p6
Figure 1.
({t1 },θ1 ) ({t2 },θ2 )
. . . (S = S 0 −→ S 1 −→ S 2 . . .,), is a step (interleaving) ring sequence
of T N from a state S . Then, σ = (U1 , θ1 ) (U2 , θ2 ) . . . (σ = ({t1 }, θ1 ) ({t2 }, θ2 )
. . .) is called a step (interleaving) ring schedule of T N from S . De ne the step
(interleaving) language of T N , Ls(i) (T N ) = {(A1 , θ1 ) . . . (Ak , θk ) | σ = (U1 , θ1 )
. . . (Uk , θk ) is a step (interleaving) ring schedule of T N from the initial state
S0 , and Ak = L(Uk ) (k ≥ 0)}.
A state S of T N is reachable if it appears in some step ring sequence of T N
from the initial state S0 . Let RS(T N ) denote the set of all reachable states of
T N . We call T N T -restricted if • t ̸= ∅ ̸= t• for all transition t ∈ T ; contact-free
if Contact(S) = ∅ for all S ∈ RS(T N ); time-progressive if for every in nite
step ring schedule (U1 , θ1 ) (U2 , θ2 ) (U3 , θ3 ) . . ., the series θ1 + θ2 + θ3 + . . .
diverges. In what follows, we will consider only T -restricted, contact-free and
time-progressive time Petri nets.
Example 1. Figure 1 shows a time Petri net T N . Both σ = ({t1 , t4 }, 3) and σ′ =
({t1 , t4 }, 3)({t2 }, 1)({t3 }, 1)({t5 }, 2) . . . are step
{ ring schedules of T N from S0 =
0, if t ∈ {t1 , t3 , t4 },
(M0 , I0 , GT0 ), where M0 = {p1 , p2 }, I0 (t) = and
undef ined, otherwise,
GT0 = 0. Furthermore, σ b = ({t2 }, 1)({t3 }, 1)({t5 }, 2) . . . {
is a step ring schedule
0, if t = t2 ,
of T N from S = (M, I, GT ), where M = {p3 , p5 }, I(t) =
undef ined, otherwise,
and GT = 3. It is easy to see that T N is really T -restricted, contact-free and
time-progressive.
3 Auxiliary Models
First, consider de nitions related to time partial orders.
De nition 2. A (labeled over Act) time partial order is a tuple η = (X, ≺, λ, τ )
consisting of a set X ; a transitive, irre exive relation ≺; a labeling function
λ : X → Act; and a timing function τ : X → T such that e ≺ e′ ⇒ τ (e) ≤ τ (e′ ).
As usual, we write x ≼ y for x ≺ y or x = y. Often ≺ is called a strict partial
order, while ≼ is a partial order, i.e. a re exive, antisymmetric and transitive
relation.
Time partial order sets over Act, η = (X, ≺, λ, τ ) and η ′ = (X ′ , ≺′ , λ′ , τ ′ ),
are isomorphic (denoted η ∼ η ′ ) i there is a bijective mapping β : X → X ′
such that (i) x ≺ x e ⇐⇒ β(x) ≺′ β(e e ∈ X ; (ii) λ(x) = λ′ (β(x))
x), for all x, x
′
and τ (x) = τ (β(x)), for all x ∈ X . The isomorphic class of a time partial order
over Act, η , is called a time pomset over Act and denoted as pom(η).
Second, we aim at de ning notions pertaining to time event structures.
De nition 3. A (labeled over Act) time event structure is a tuple ξ = (E ,
≺, #, l, τ ) with a set E of events; a strict partial order ≺⊆ E × E such that
| ↓ e = {e′ ∈ E | e′ ≺ e}| < ∞, for all e ∈ E ; an irre exive symmetric
con ict relation # ⊆ E × E such that (e # e′ ≺ e′′ ) ⇒ (e # e′′ ), for all
e, e′ , e′′ ∈ E ; a labeling function l : E → Act; a timing function τ : E → T such
that e ≺ e′ ⇒ τ (e) ≤ τ (e′ ).
Time event structures over Act, ξ = (E, ≺, # , l, τ ) and ξ ′ = (E ′ , ≺′ , # ′ , l′ , τ ′ ),
are isomorphic (denoted ξ ∼ ξ ′ ) i there is a bijective mapping β : E → E ′ such
that (i) e ≺ e′ ⇔ β(e) ≺′ β(e′ ) and e # e′ ⇔ β(e) #′ β(e′ ), for all e, e′ ∈ E ; (ii)
l(e) = l′ (β(e)) and τ (e) = τ ′ (β(e)), for all e ∈ E . The isomorphic class of a time
event structure over Act, ξ , is denoted as les(ξ).
Third, consider de nitions associated with (labeled) time nets.
De nition 4. A (labeled over Act) time net is a nitary, acyclic net T N =
(B, E, G, l, τ ) with a set B of conditions, a set E of events, a ow relation
G ⊆ (B × E) ∪ (E × B) such that {e | (e, b) ∈ G} = {e | (b, e) ∈ G} = E ,
a labeling function l : E → Act, and a time function τ : E → T such that
e G+ e′ ⇒ τ (e) ≤ τ (e′ ).
Time nets over Act, T N = (B , E , G, l, τ ) and T N ′ = (B ′ , E ′ , G′ , l′ , τ ′ ), are
isomorphic (denoted T N ≃ T N ′ ) i there exists a bijective mapping β : B ∪E →
B ′ ∪ E ′ such that (i) β(B) = B ′ and β(E) = E ′ ; (ii) x G y ⇐⇒ β(x) G′ β(y),
for all x, y ∈ B ∪ E ; (iii) l(e) = l′ (β(e)) and τ (e) = τ ′ (β(e)), for all e ∈ E .
Consider additional notions and notations for a time net T N . Let ≺= G+ ,
≼= G∗ , and τ (T N ) = sup{τ (e) | e ∈ E}. Specify • x = {y∪| (y, x) ∈ G} and
x• = {y | (x, y) ∈ G}, for x ∈ B ∪ E , and, moreover, • X = x∈X • x and X • =
∪ • • •
x∈X x , for X ⊆ B ∪ E . Furthermore, de ne the sets T N = {b ∈ B | b = ∅},
• • ′ ′ ′
T N = {b ∈ B | b = ∅}. Given e, e ∈ E , x, x ∈ (B ∪ E), and E ⊆ E ,
↓ e = {x | x ≼ e} (predecessors),
E ′ is a downward-closed subset of E if ↓ e′ ∩ (E × E) ⊆ E ′ , for all e′ ∈ E ′ .
In this case, E ′ is called timely sound if τ (e′ ) ≤ τ (e), for all e′ ∈ E ′ and
e ∈ E \ E ′ , and de ne the set Cut(E ′ ) = (E ′• ∪ • T N ) \ • E ′ ,
x # x′ ⇐⇒ ∃e ̸= e′ ⋄ e ≼ x, ∧ e′ ≼ x′ ∧ • e ∩ • e′ ̸= ∅ (con ict),
E ′ is a con ict-free subset of E , if ¬(e′ # e′′ ), for all e′ , e′′ ∈ E ′ ,
E ′ is a con guration of T N if E ′ is a nite, downward-closed, con ict-free
subset of E ,
x ⌣ x′ ⇐⇒ ¬((x ≺ x′ ) ∨ (x′ ≺ x) ∨ (x # x′ )) (concurrency).
∅ ̸= E ′ is a step of T N i e ⌣ e′ and τ (e) = τ (e′ ), for all e, e′ ∈ E ′ . In this
case, let τ (E ′ ) = τ (e) for some e ∈ E ′ .
Given time nets T N = (B, E, G, l, τ ), Td N = (B, b E, b b
b G, l, τb) and T N ′ =
(B ′ , E ′ , G′ , l′ , τ ′ ), T N is a pre x of T N ′ (denoted T N −→ T N ′ ) if B ′ ⊆ B , E is a
nite, downward-closed and timely sound subset of E ′ , G = G′ ∩(B ×E ∪E ×B),
l = l′ |E , and τ = τ ′ |E ; Td N is a su x of T N ′ w.r.t. T N if E b = E′ \ E,
Bb = B \B ∪TN , G
′ • b = G ∩ (B
′ b×E b∪E b × B) b
b , l = l | b , and τb = τ | b . We write
′ ′
E E
d
T N −→ T N ′ i T N −→ T N ′ and Td
T N
N is a su x of T N ′ w.r.t. T N .
d
Lemma 1. Given T N −→
TN b , the following holds:
T N ′ and eb ∈ E
(i) • T N = • T N ′ and • Td N = T N •,
(ii) (• eb \ • Td
N ) ⊆ (• eb \ • T N ′ ),
(iii) if eb ⊆ B ′ ⊆ Be , then {b ∈ Be ′ | φ(b)
• e b e)} = • eb in Tg
e ∈ • φ(b N ∈ {T N, Td
N , T N ′ }.
An s-linearization of a time net T N is a nite or in nite sequence ρ =
V1 V2 . . . of steps of T N , such that every event of T N is included in the sequence
exactly once, and both causal and time orders are preserved: (ei ≺ ej ∨ τ (ei ) <
τ (ej )) ⇒ i < j , for all ei ∈ Vi and ej ∈ Vj (i, j ≥ 1). An s-linearization of
T N of the form: ρ = {e1 }{e2 } . . ., is called an ∪i-linearization of T N . For an
s-linearization ρ = V1 V2 . . . of T N , de ne Eρk = 1≤i≤k Vi (k ≥ 0). Clearly, Eρk
is a downward-closed subset of E .
A (labeled over Act) time net T N = (B, E, G, l, τ ) is called a time causal
net, if |• b| ≤ 1 ∧ |b• | ≤ 1, for all b ∈ B ; a time occurrence net, if |• b| ≤ 1,
and ¬(x #T N x), for all x ∈ B ∪ E . Clearly, η(T N ) = (E, ≺ ∩(E × E), l, τ )
is a time partial order, if T N is a time causal net, and ξ(T N ) = (ET N , ≺T N
∩(ET N × ET N ), #T N ∩ (ET N × ET N ), lT N , τT N ) is a (labeled over Act) time
event structure, if T N is a time occurrence net.
Lemma 2. Every time causal( net T N has an s-linearization
) ( V1 V2 . . .. More-
ρ= )
over, it holds: Cut(Eρk+1 ) = Cut(Eρk ) \ • V k+1 ∪ V • k+1 , and Cut(Eρk ) \ • e ∩
e• = ∅, for all e ∈ Vk+1 (k ≥ 0).
Example 2. The time causal net T N ′ = (B ′ , E ′ , G′ , l′ , τ ′ ) is depicted in
Figure 2(a), where the net elements are accompanied by their names, and the
values of the functions l′ and τ ′ are indicated nearby the events. De ne the
time causal nets T N = (B, E, G, l, τ ), with B = {b1 , b2 , b3 , b4 }, E = {e1 , e4 },
G = G′ ∩ (B × E ∪ E × B)}, l = l′ |E , τ = τ ′ |E , and Td b E,
N = (B, b G, b b
l, τb), with
b ′ b ′ b ′ b b b b b
B = B \ B ∪ {b3 , b4 }, E = E \ E , G = G ∩ (B × E ∪ E × B), l = l |Eb , τb = τ ′ |Eb .
′
It is easy to see that T N is a pre x of T N ′ , Td N is a su x of T N ′ w.r.t. T N ,
d
T N
and, moreover, T N −→ T N ′ . Notice that ρT N ′ = {e1 , e4 }{e2 }{e3 }{e5 } . . . is an
s-linearization of T N ′ . The time occurrence net Tg
N is depicted in Figure 2(b).
(a) b1 g b2 g (b) b1 g b2 g
Z
Z
Z
a ?3 c ?
e4 3
a ?3 bZ
~ 1 c ?
e1 e1 e6 e4 3
T N′ : ? ? g ? ? ?
b3 g b4 g T N: b3 g b8 g b4 g
d ?4 d ?4 f ?
=3
e2 e2 e7
? ? ?
b5 g b5 g b9 g
Z
Z
Z
b ?
e3 5
a ?5 bZ
~
e8 e3 5
? ? ?
b6 g b10 g b6 g
Z
Z
Z
fZ
~ ?7 d ?6 f ?7
e5 e9 e5
? ? ?
b7 g b11 g b7 g
Figure 2.
4 Time Process Semantics
We start with de ning a special mapping from a time net T N to a time
Petri net T N w.r.t. its marking. Given a time Petri net T N = ((P , T , F ,
M0 , L), D) with a marking M and a time net T N = (B, E, G, l, τ ), a mapping
φ : B ∪E → P ∪T is a homomorphism from T N to T N w.r.t. M i the following
conditions hold:
φ(B) ⊆ P , φ(E) ⊆ T ,
the restriction of φ to • e is a bijection between • e and • φ(e) and the restric-
(tion of φ to e• is a bijection
) between e• and φ(e)• , for all e ∈ E ,
e = e ∧ φ(e) = φ(e ) ⇒ e = e′ ,
• • ′ ′
the restriction of φ to • T N is a bijection between • T N and M ,
l(e) = L(φ(e)), for all e ∈ E .
4.1 Time C -Processes
First, introduce the notion of a time C -process of T N w.r.t. its marking.
De nition 5. Given a time Petri net T N with its marking M , a time C -process
of T N w.r.t. M is a pair π = (T N, φ) with a time causal net T N and a homo-
morphism φ from T N to T N w.r.t. M . Let τ (π) = τ (T N ).
We use CP(T N , M0 ) (CP(T N , M )) to denote the set of time C -processes
of T N w.r.t. the initial marking M0 (a marking M ). Let π = (T N, φ), π ′ =
π d
b=(T b
N ,φ) d
T N
(T N ′ , φ′ ) ∈ CP(T N , M0 ). Then, π −→ π ′ i T N −→ T N ′ , φ = φ′ |B∪E ,
b
π (a,θ)
and φ b = φ′ |B∪
b E
′
b . From now on, whenever π −→ π , we shall write π −→ π
′
if Eb = {e}, τb(e) = τ (π) + θ, b (A,θ)
b × E)
b ∩ (E
l(e) = a; and π −→ π ′ if ≼ b = ∅,
b b ∑ b b
l(E) = e∈E b(e) = τ (π) + θ, for all e ∈ E .
b l(e) = A, τ
Given π = (T N, φ) ∈ CP(T N , M ), a state S = (M, I, GT ) of T N , and
B ′ ⊆ BT N , the latest global time moment when tokens appear in all input
places of the transition t ∈ En(φ(B ′ )) is de ned as follows:
( )
TOEπ,S (B ′ , t) = max {τT N (• b) | b ∈ B[t]
′
\ • T N } ∪ {GT } ,
′
where B[t] = {b ∈ B ′ | φT N (b) ∈ • t}, GT = GT − I(t), if B[t] ′
⊆ • T N , and
GT = GT , otherwise. Notice that the above is an extension of the de nition of
TOE(·, ·) from [3] to the case of the time C -processes of T N w.r.t. an arbitrary
one and not only the initial marking.
De nition 6. A time C -process π = (T N, φ) of T N w.r.t. M is a time C -
process of T N w.r.t. S = (M, I, GT ) ∈ RS(T N ) i for all e ∈ E it holds:
(i) τ (e) ≥ GT ,
(ii) τ (e) ≥ TOEπ,S (• e, φ(e)) + Ef t(φ(e)),
(iii) ∀t ∈ En(φ(Ce )) ⋄ τ (e) ≤ TOEπ,S (Ce , t) + Lf t(t),
where Ce = Cut(Earlier(e)) with Earlier(e) = {e′ ∈ E | τ (e′ ) < τ (e)}.
The time C -process π0 = (T N0 = (B0 , ∅, ∅, ∅, ∅), φ0 ) of T N w.r.t. the
initial state is called the initial time C -process of T N . We use CP(T N , S0 )
(CP(T N , S)) to denote the set of time C -processes of T N w.r.t. the initial state
S0 (a state S ∈ RS(T N )).
Theorem 1. Given π = (T N, φ), π ′ = (T N ′ , φ′ ) ∈ CP(T N , S0 ) such that
b
b = (Td
π −→ {π ′ , π b ∈ CP(T N , Sb = (Mc, I,
b GT
d )), where M
c = φ(T N • ),
π
N , φ)
b = τ (T N ) − TOEπ,S0 (T N , t), if t ∈ En(M ), and GT
• c
I(t) d = τ (T N ).
unde ned, otherwise,
Finally, we intend to realize for a time Petri net the relationships between its
ring schedules from reachable states and its time C -processes w.r.t. the states.
Lemma 3. Given π =( (T N, φ) ∈ CP(T
) ′ N , S)(, an s-linearization
) ρ(= V1 V2 . . . of )
T N , e ∈ Vk+1 , t ∈ En φ(Cut(Eρ )) , t ∈ En φ(Ce ) , and t ∈ En φ(Cut(Eρ ))
k ′′ k+1
(k ≥ 0), the following holds:
(i) TOEπ,S (Cut(Eρk ), φ(e)) = TOEπ,S (• e, φ(e)), ( )
(ii) TOEπ,S (Cut(Eρk ), t) = TOEπ,S (Ce , t), if (t ∈ En)φ(Ce ) ,
(iii) TOEπ,S (Cut(Eρk ), t) = τ (Vk+1 ), if t ̸∈ En φ(Ce ) ,
( )
(iv) TOEπ,S (Cut(Eρk ), t) = TOEπ,S (Cut(Eρk+1 ), t)(, if t ∈ En φ(Cut(Eρk+1) )) ,
(vi) TOEπ,S (Cut(Eρk+1 ), t′′ ) = τ (Vk+1 ), if t′′ ̸∈ En (φ(Cut(Eρk ))) \ • Vk+1 .
For π = (T N, φ) ∈ CP(T N , S), de ne the function F Sπ,S which maps any
s-linearization ρ = V1 V2 . . . of T N to the sequence of the form: F Sπ,S (ρ) =
(φ(V1 ), τ (V1 ) − GT ) (φ(V2 ), τ (V2 ) − τ (V1 )) . . ..
Proposition 1. Given π = (T N, φ) ∈ CP(T N , S = (M, I, GT )) and an
s(i)-linearization ρ = V1 V2 . . . of T N , F Sπ,S (ρ) is a step (interleaving)
ring schedule of T N from the state S , (with intermediate
) states S k =
(M , I , GT ) (k ≥ 0), where M = φ Cut(Eρ ) , GT = τ (Vk ), and
k k k k k k
{ ( )
τ (Vk ) − TOEπ,S Cut(Eρk ), t , if t ∈ En(M k ),
k
I (t) =
unde ned, otherwise, Here, τ (V0 ) = GT .
For any step (interleaving) ring schedule σ of T N from a state S ∈ RS(T N ),
there is a unique (up to an isomorphism) time process π ∈ CP(T N , S) such
that F Sπ,S (ρ) = σ, where ρ is an s(i)-linearization of T N .
Notice that the above Proposition is an extension of Theorems 19 and 21
from [3] to the cases of s-linearizations of time C -processes of T N w.r.t. arbitrary
reachable states and step ring schedules of T N from the states.
Example 3. De ne a mapping φ′ from the time causal net T N ′ (see Fig. 2(a))
to the time Petri net T N (see Fig. 1), as follows: φ′ (bi ) = pi (1 ≤ i ≤ 3),
φ′ (b4 ) = p5 , φ′ (b5 ) = p1 , φ′ (b6 ) = p4 , φ′ (b7 ) = p6 , and φ′ (ei ) = ti (1 ≤
i ≤ 5). Next, for the time causal nets T N and Td N speci ed in Example 1,
set φ = φ′ |E∪B and φ b = φ′ |E∪ ′ ′
b , respectively. Clearly, π = (T N , φ )
b B
′
d
T N
and π = (T N, φ) are time C -process of T N w.r.t. M0 . As T N −→ T N ′ ,
d
b=(T b
we get π
π
−→
N ,φ)
π ′ . Further, take B e = {b1 , b2 }, S ′ = (M ′ , I ′ , GT ′ ), where
{
0, if t ∈ {t1 , t4 },
M ′ = {p1 , p2 }, I ′ (t) = and GT ′ = 3, and t1 ∈
undef ined, otherwise,(
e . Calculate TOEπ′ ,S ′ (B,
En(φ′ (B)) e t1 ) = max {τT N ′ (• b) | b ∈ B e[t ] \ • T N ′ } ∪
) ( )
1
{GT } = max ∅ ∪ {3 − 0} = 3. It is not di cult to check that π ′ = (T N ′ , φ′ ),
π = (T{ N, φ) ∈ CP(T N , S0 ). Then, π b ∈ CP (T N , S), where M = {p3 , p5 },
0, if t = t2 ,
I(t) = and GT = 3, due to Theorem 1. For the s-
undef ined, otherwise,
linearization ρT N ′ = {e1 , e4 }{e2 }{e3 }{e5 } . . . of T N ′ from Example 2, we can
get F Sπ′ ,S0 (ρT N ′ ) = σ ′ , by using Proposition 1.
4.2 Time O-Processes
De ne the notion of a time O-process of T N w.r.t. its marking.
De nition 7. Given a time Petri net T N with its marking M , a time O-process
of T N w.r.t. M is a pair ν = (T N, ψ) with a time occurrence net T N and a
homomorphism ψ from T N to T N w.r.t. M .
A computation of a time O-process ν = (T N = (B , E , G, l, τ ), ψ) of T N
w.r.t. M is a nite time C -process π = (T N ′ = (B ′ , E ′ , G′ , l′ , τ ′ ), ψ|B ′ ∪E ′ )
of T N w.r.t. M such that E ′ ⊆ E is a con guration of T N . A time O-process
ν = (T N, ψ) of T N w.r.t. M is a time O-process of T N w.r.t. S = (M, I, GT ) ∈
RS(T N ) i all computations of ν belong to the set CP(T N , S). We use OP(T N , S0 )
to denote the set of all time O-processes of T N w.r.t. S0 .
Example 4. To illustrate the notions above, rst de ne a mapping ψ from the
time O-net Tg N (see Fig. 2(b)) to the time Petri net T N (see Fig. 1) as follows:
ψ(b1 ) = ψ(b5 ) = ψ(b11 ) = p1 , ψ(b2 ) = p2 , ψ(b3 ) = ψ(b10 ) = p3 , ψ(b4 ) = p5 ,
ψ(b6 ) = ψ(b8 ) = p4 , ψ(b7 ) = ψ(b9 ) = p6 and ψ(e1 ) = ψ(e8 ) = t1 , ψ(e2 ) =
ψ(e9 ) = t2 , ψ(e3 ) = ψ(e6 ) = t3 , ψ(e4 ) = t4 , ψ(e5 ) = ψ(e7 ) = t5 . Clearly, both
π and π ′ , speci ed in Example 3, are time C -processes of of T N w.r.t. S0 , and,
moreover, are computations of ν . It is easy to see that all computations of ν
belong to the set CP(T N , S ′ ). Then, ν is a time O-process of T N w.r.t. S0 .
5 Hierarchy of Behavioral Equivalences
First, consider equivalence notions rested on classical state-based behaviors
of time Petri nets.
De nition 8. Time Petri nets T N and T N ′ labeled over Act are:
step (interleaving) trace equivalent (denoted T N ≡s(i) T N ′ ) i Ls(i) (T N ) =
Ls(i) (T N ′ ),
step (interleaving) bisimilar (denoted T N -s(i) T N ′ ) i there is a relation
R ⊆ RS(T N ) × RS(T N ′ ) such that (S0 , S0′ ) ∈ R (S0 and S0′ are the initial
states of T N and T N ′ , respectively) and for all (S, S ′ ) ∈ R it holds:
• if S −→ S1 (S −→ S1 ) in T N , then S ′ −→ S1′ (S ′ −→ S1′ ) in T N ′
(A,θ) ({a},θ) (A,θ) ({a},θ)
and (S1 , S1′ ) ∈ R,
• and vice versa.
Before de ning behavioral equivalences on time processes of time Petri nets,
we need auxiliary notions. Given a time Petri net T N , de ne the following sets:
(a ,θ )
T racei−pr (T N ) = {({a1 }, θ1 ) . . . ({an }, θn ) ∈ (2Act × T)∗ | π0 −→
1 1
π1 . . .
(an ,θn )
πn−1 −→ πn (n ≥ 0) in T N },
(A ,θ )
T races−pr (T N ) = {(A1 , θ1 ) . . . (An , θn ) ∈ (NAct × T)∗ | π0 −→
1 1
π1 . . .
(An ,θn )
πn−1 −→ πn (n ≥ 0) in T N },
T racepom−pr (T N ) = {pom(η(T N )) | π = (T N, φ) ∈ CP(T N , S0 )},
T racec−pr (T N ) = {[T N ]≃ | π = (T N, φ) ∈ CP(T N , S0 )},
T raceles−pr (T N ) = {les(ξ(T N )) | ν = (T N, ψ) ∈ OP(T N , S0 )},
T raceo−pr (T N ) = {[T N ]≃ | ν = (T N, ψ) ∈ OP(T N , S0 )}.
De nition 9. Let ∗ ∈ {i − pr, s − pr, pom − pr, c − pr, les − pr, o − pr} and ⋆ ∈
{i−pr, s−pr, pom−pr, c−pr}. Then,
T N and T N ′ ∗-trace equivalent (denoted T N ≡∗ T N ′ ) i T race∗ (T N ) =
T race∗ (T N ′ ),
a relation R ⊆ CP(T N , S0 ) × CP(T N ′ , S0′ ) is ⋆-bisimulation between T N
and T N ′ (denoted R : T N -⋆ T N ′ ) i (π0 , π0′ ) ∈ R, and for all (π, π) ∈ R,
the following holds:
b
1. whenever π −→ π
e in T N and
π
b = 1, if ⋆ = i−pr,
* |E|
* ≼b ∩ (Eb × E)
b = ∅, if ⋆ = s−pr,
′
b
then π′ −→ πe′ in T N ′ , (eπ, πe′ ) ∈ R, and
π
′
* η(TdN ) ≃ η(Td N ), if ⋆ ∈ {i−pr, s−pr, pom−pr},
′
* TdN ≃ Td N , if ⋆ = c−pr,
2. Symmetric to item 1.
T N and T N ′ are ⋆-bisimilar (denoted T N -⋆ T N ′ ) i there is ⋆-bisimulation
R : T N -⋆ T N ′ .
Proposition 2. Let ↔∈ {≡, -} and ∗ ∈ {i, s}. Then, T N ↔∗ T N ′ ⇐⇒
T N ↔∗−pr T N ′ .
Finally, we state the relationships between the time process equivalences of
time Petri nets.
Theorem 2. Let ↔, ∈ {≡, -} and ⋆, ∗ ∈ {i−pr, s−pr, pom−pr, c−pr, les−
pr, o−pr}. Then,
T N ↔⋆ T N ′ ⇒ T N ∗ TN
′
i there is a directed path from ↔⋆ to ∗ in Fig. 3.
≡les−pr ≡o−pr
? ?
-i−pr -s−pr -pom−pr -c−pr
? ? ? ?
≡i−pr ≡s−pr ≡pom−pr ≡c−pr
Figure 3.
Proof. (⇐) All the implications in Fig. 1 follow from the De nitions, Theorems
and Lemmas considered prior to that.
(⇒) We now demonstrate that it is impossible to draw any arrow from one equiv-
alence to the other such that there is no directed path from the rst equivalence
to the second one in the graph in Fig. 1.
For this purpose, we consider the time Petri nets depicted in Fig. 2. It is
easy to see that T N 1 and T N 2 are ≡c−pr equivalent but not -i−pr equivalent
because, for example, any time C -process π of T N 2 w.r.t. the initial state,
containing one event (with its input and output conditions) labeled by an action
b and time moment 0, can be extended up to a time C -process π ′ of T N 2 w.r.t.
the initial state, containing two events (with their input and output conditions)
labeled by actions b and a and time moments 0 and 5, respectively, by the time
C -process πb of T N 2 w.r.t. its state corresponding to the nishing of π , but it is
not the case in T N 1 .
Second, T N 2 and T N 3 are -i−pr equivalent but not ≡s−pr equivalent be-
cause, for example, there is a time C -process of T N 3 w.r.t. the initial state,
containing two concurrent events (with their input and output conditions) la-
beled by actions a and b and time moments 0, but it is not the case in T N 2 .
Third, T N 3 and T N 4 are -s−pr equivalent but not ≡pom−pr equivalent be-
cause, for example, there is a time C -process of T N 3 w.r.t. the initial state,
containing two events (with their input and output conditions) labeled by ac-
tions b and a and time moments 0 and 5, respectively, such that an action b
causally precedes an action a, but it is not the case in T N 4 .
Fourth, T N 4 and T N 5 are ≡les−pr equivalent but not ≡c−pr equivalent be-
cause, for example, the time C -processes of T N 4 and T N 5 w.r.t. their initial
states, containing events (with its input and output conditions) labeled by ac-
tions a and time moments 0, are not isomorphic.
Finally, T N 5 and T N 6 are -c−pr equivalent but not ≡les−pr equivalent be-
cause it is easy to see that the time event structure, corresponding to any max-
imal time O-processes of T N 6 w.r.t. its initial states, contains two con icting
events labeled by actions b and time moments 0, but it is not the case in T N 5 .
References
1. Andreeva M.V., Virbitskaite I.B.: Timed equivalences for Timed Event Struc-
tures. Lecture Notes in Computer Science 3606 (2005) 1626.
2. Andreeva M.V., Virbitskaite I.B.: Observational equivalences for timed stable
event structures. Fundamenta Informaticae 72(4), 2006, 119.
3. Aura, T., Lilius, J.: Time Processes for Time Petri Nets. Lecture Notes in
Computer Science 1248 (1997) 136155.
4. Bihler, E., Vogler, W.: Timed Petri Nets: E ciency of asynchronous systems.
Lecture Notes in Computer Science 3185 (2004) 2558.
5. Boyer, M., Vernadat, R.: Language and bisimulation relations between sub-
classes of timed Petri nets with strong timing semantics. Thechnical Report No.
146, LAAS (2000).
6. Bushin, D., Virbitskaite, I.: Comparing Semantics under Strong Timing of
Petri Nets. In: Proc. PSI'14, Saint-Petersburg, 24-27 June, 2014, to appear in
LNCS.
7. Chatain, T., Jard, C.: Time supervision of concurrent systems using symbolic
unfoldings of time Petri nets. Lecture Notes in Computer Science 3829 (2005)
196210.
8. Valero, V., de Frutos, D., Cuartero, F.: Timed processes of timed Petri
nets. Lecture Notes in Computer Science 935 (1995) 490509.
9. Winkowski, J.: Algebras of Processes of Timed Petri Nets. Lecture Notes in
Computer Science 480 (1994) 309-321.
T N1 T N2 :
h h
Z Z
= ? Z
~
a [0, 0]
= Z
Z
~ b [0, 0]
a [0, 0] b [0, 0]
b [0, 5]
? ? ? ?
h ?
h
h h h
b [0, 0] ? ? a [0, 5]
b [0, 0] ? ? a [0, 5]
?
h ?
h
? ?
h h
T N3 : T N4 :
h h
HH
HH h h
a [0, 5] ? j
? b [0, 0]
b [0, 5]
?
h ?
h ?
h a [0, 5] ? ?b [0, 0]
?
h ?
h
?
a [0, 5]
?
h
T N5 : T N6 :
h h h h
@
a [0, 5] ? ? b [0, 0] a [0, 5] ? b [0, 0] ? @R b [0, 5]
@ @
@ @
h@
? Rh ?
h h@
? Rh ?
h ?
h
Figure 4.