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 wellunderstood.
used for the execution of certain activities and average waiting time for certain
requests), many time extensions have been dened 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 [
so-called weighted pomsets. The paper [
notions on Petri nets is even less advanced. In this regard, the paper [
on the base of timed interleaving language and bisimulation equivalences. The
papers [
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/141 and 14-01-91334)
requirements). This is an extension of the paper [
[ 1; 2] the closed interval between two time values 1; 2 2 T, and by Interv the set of all such intervals. Innity 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.
Denition 1. A (labeled over Act) time Petri net is a tuple T N = ((P , T , F ,
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 2 P [ T , let x = fy j (y; x) 2 F g and x = fy j (x; y) 2 F g be the preset and postset of x, respectively. For X P [ T , dene X = ∪ x and X = ∪x2X x . For a transition t 2 T , the boundaries of the inxt2eXrval
disabled. Let En(M ) be the set of transitions enabled at M .
(M; I; GT ), where M is a marking, I : En(M ) ! T is a dynamic timing function, and GT 2 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 2 En(M0), and GT0 = 0.
We call a non-empty subset U T a step enabled at a state S = (M; I; GT ), if (8t 2 U ⋄ t 2 En(M )) and (8t ̸= t′ 2 U ⋄ t \ t′ = ∅). A step U T enabled at a state S = (M; I; GT ) is reable from S after a delay time 2 T if (8t 2 U ⋄ Ef t(t) I(t) + ) and (8t′ 2 En(M ) ⋄ I(t′) + Lf t(t′)). Let Contact(S) = ft 2 U j U is a step reable from a state S = (M; I; GT ) after some delay time 2 T and (M n t) \ t ̸= ∅)g.
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: (ii) 8t′ 2 T ⋄ I′(t′) = (i) M ′ = (M n U ) [ U , 8 I(t′) + ; if t′ 2 En(M n U ); < 0; if t′ 2 En(M ′) n En(M n U ); : undened ; otherwise, (iii) GT ′ = GT + .
In this case, we write S (U!;) S′, and, moreover, S (A!;) S′, if A = L(U ) = ∑t2U L(t). A nite or innite sequence of the form: S = S0 (U1!;1) S1 (U2!;2) S2 T N : p3 ?[1; 1] ? Z : : : (S = S0 (ft1g; 1) S1 (ft2g; 2) S2 : : :,), is a step (interleaving) ring sequence ! ! of T N from a state S. Then, = (U1; 1) (U2; 2) : : : ( = (ft1g; 1) (ft2g; 2) : : :) is called a step (interleaving) ring schedule of T N from S. Dene the step (interleaving) language of T N , Ls(i)(T N ) = f(A1; 1) : : : (Ak; k) j = (U1; 1) : : : (Uk; k) is a step (interleaving) ring schedule of T N from the initial state S0, and Ak = L(Uk) (k 0)}.
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 2 T ; contact-free if Contact(S) = ∅ for all S 2 RS(T N ); time-progressive if for every innite 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 = (ft1; t4g; 3) and ′ = (ft1; t4g; 3)(ft2g; 1)(ft3g; 1)(ft5g; 2) : : : are step ring schedules of T N from S0 = (M0; I0; GT0), where M0 = fp1; p2g, I0(t) = { 0u;ndef ined; iofthte2rwfits1e;,t3; t4g; and GT0 = 0. Furthermore, b = (ft2g; 1)(ft3g; 1)(ft5g; 2) : : : is a step ring schedule of T N from S = (M; I; GT ), where M = fp3; p5g, I(t) = { 0u;ndef ined; iofthte=rwti2s;e, and GT = 3. It is easy to see that T N is really T -restricted, contact-free and time-progressive. 3
Denition 2. A (labeled over Act) time partial order is a tuple = (X; ≺; ; ) consisting of a set X; a transitive, irreexive 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 reexive, antisymmetric and transitive relation.
Time partial order sets over Act, = (X; ≺; ; ) and ′ = (X′; ≺′; ′; ′), are isomorphic (denoted ′) i there is a bijective mapping : X ! X′ sauncdh t(hxa)t=(i) ′x( ≺(xxe)), f(or)all x (2x)X≺. ′Th(exei)s,ofmororapllhixc; cxela2ssXof; a(iit)ime(xp)a=rtial′(or(dxe)r) over Act, , is called a time pomset over Act and denoted as pom( ).
Denition 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 j # e = fe′ 2 E j e′ ≺ egj < 1, for all e 2 E; an irreexive symmetric conict relation # E E such that (e # e′ ≺ e′′) ) (e # e′′), for all e; e′; e′′ 2 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′ 2 E; (ii) l(e) = l′( (e)) and (e) = ′( (e)), for all e 2 E. The isomorphic class of a time event structure over Act, , is denoted as les( ).
Denition 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 fe j (e; b) 2 Gg = fe j (b; e) 2 Gg = 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 2 B [ E; (iii) l(e) = l′( (e)) and (e) = ′( (e)), for all e 2 E.
Consider additional notions and notations for a time net T N . Let ≺= G+, ≼= G , and (T N ) = supf (e) j e 2 Eg. Specify x = fy j (y; x) 2 Gg and x∪x2=Xfxy j, (foxr; yX) 2 GBg[,fEor. xFu2rtBhe[rmEo,rea,ndde,nmeothreeosveetrs, XT=N ∪=xf2bX2 xBajndb X= ∅g=, T N = fb 2 B j b = ∅g. Given e; e′ 2 E, x; x′ 2 (B [ E), and E′ E, # e = fx j x ≼ eg (predecessors),
e 2 E n E′, and dene the set Cut(E′) = (E′ [ T N ) n E′, x # x′ () 9e ̸= e′ ⋄ e ≼ x; ^ e′ ≼ x′ ^ e \ e′ ̸= ∅ (conict),
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′ 2 E′. In this case, let (E′) = (e) for some e 2 E′.
Given time nets T N = (B; E; G; l; ), TdN = (Bb; Eb; Gb; bl; b) and T N ′ = (B′; E′; G′; l′; ′), T N is a prex 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′ jE, and = ′ jE; TdN is a sux of T N ′ w.r.t. T N if Eb = E′ n E, Bb = B′ n B [ T N , Gb = G′ \ (Bb Eb [ Eb Bb), bl= l′ jEb, and b = ′ jEb. We write T N Td!N T N ′ i T N ! T N ′ and TdN is a sux of T N ′ w.r.t. T N . Lemma 1. Given T N Td!N T N ′ and eb 2 Eb, the following holds: (i) T N = T N ′ and TdN = T N , (ii) ( eb n TdN ) (iii) if eb Be′ ( eb n T N ′), Be, then fb 2 Be′ j φe(b) 2 φb(eb)g = e in TgN 2 fT N; TdN ; T N ′g.
b
An s-linearization of a time net T N is a nite or innite sequence =
exactly once, and both causal and time orders are preserved: (ei ≺ ej _ (ei) < (ej)) ) i < j, for all ei 2 Vi and ej 2 Vj (i; j 1). An s-linearization of T N of the form: = fe1gfe2g : : :, is called an i-linearization of T N . For an s-linearization = V1V2 : : : of T N , dene Ek = ∪1 i k Vi (k 0). Clearly, Ek 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 j bj 1 ^ jb j 1, for all b 2 B; a time occurrence net, if j bj 1, and :(x #T N x), for all x 2 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 = V1V2 : : :. Moreover, it holds: Cut(Ek+1) = (Cut(Ek) n V k+1)[ V k+1, and (Cut(Ek) n e)\ e = ∅, for all e 2 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. Dene the time causal nets T N = (B; E; G; l; ), with B = fb1; b2; b3; b4g, E = fe1; e4g, G = G′ \ (B E [ E B)g, l = l′ jE, = ′ jE, and TdN = (Bb; Eb; Gb; bl; b), with Bb = B′ n B [ fb3; b4g, Eb = E′ n E, Gb = G′ \ (Bb Eb [ Eb Bb), bl= l′ jEb; b = ′ jEb.
and, moreover, T N Td!N T N ′. Notice that T N′ = fe1; e4gfe2gfe3gfe5g : : : is an s-linearization of T N ′. The time occurrence net TgN is depicted in Figure 2(b).
(a) T N ′ :
TgN :
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 restriction of φ to e is a bijection between e and φ(e) , for all e 2 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 2 E. 4.1
of T N w.r.t. M is a pair = (T N; φ) with a time causal net T N and a homomorphism φ 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; φ), ′ = (T N ′; φ′) 2 CP(T N ; M0). Then, b=(Td!N;φb) ′ i T N and φb = φ′jBb[Eb. From now on, whenever b! ′, we shall write if Eb = feg, b(e) = ( ) + , bl(e) = a; and (A!;) ′ if ≼b \ (Eb Eb) = ∅, bl(Eb) = ∑e2Eb bl(e) = A, b(e) = ( ) + , for all e 2 Eb.
Given = (T N; φ) 2 CP(T N ; M ), a state S = (M; I; GT ) of T N , and
places of the transition t 2 En(φ(B′)) is dened as follows: Td!N T N ′, φ = φ′jB[E , (a!;) ′ ( )
TOE ;S (B′; t) = max f T N ( b) j b 2 B[′t] n T N g [ fGT g ; where B[′t] = fb 2 B′ j φT N (b) 2 tg, GT = GT I(t), if B[′t] T N , and GT = GT , otherwise. Notice that the above is an extension of the denition of
one and not only the initial marking.
Denition 6. A time C-process = (T N; φ) of T N w.r.t. M is a time Cprocess of T N w.r.t. S = (M; I; GT ) 2 RS(T N ) i for all e 2 E it holds: (i) (e) GT , (ii) (e) TOE ;S ( e; φ(e)) + Ef t(φ(e)), (iii) 8t 2 En(φ(Ce)) ⋄ (e) TOE ;S (Ce; t) + Lf t(t), where Ce = Cut(Earlier(e)) with Earlier(e) = fe′ 2 E j (e′) < (e)g.
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 2 RS(T N )).
= (T N; φ), ′ = (T N ′; φ′) 2 CP(T N ; S0) such that b ! Ib(t) =
′, b = (TdN ; φb) 2 CP(T N ; Sb = (Mc; Ib; GdT )), where Mc = φ(T N ), { (T N ) TOE ;S0 (T N ; t); if t 2 En(Mc); and GT = (T N ).
undened ; otherwise, d
ring schedules from reachable states and its time C-processes w.r.t. the states. Lemma 3. Given = (T N; φ) 2 CP(T N ; S), an s-linearization = V1V2 : : : of T N , e 2 Vk+1, t 2 En(φ(Cut(Ek))), t′ 2 En(φ(Ce)), and t′′ 2 En(φ(Cut(Ek+1))) (k 0), the following holds: (i) TOE ;S (Cut(Ek); φ(e)) = TOE ;S ( e; φ(e)), (ii) TOE ;S (Cut(Ek); t) = TOE ;S (Ce; t), if t 2 En(φ(Ce)), (iii) TOE ;S (Cut(Ek); t) = (Vk+1), if t ̸2 En(φ(Ce)), (iv) TOE ;S (Cut(Ek); t) = TOE ;S (Cut(Ek+1); t), if t 2 En(φ(Cut(Ek+1))), (vi) TOE ;S (Cut(Ek+1); t′′) = (Vk+1), if t′′ ̸2 En((φ(Cut(Ek))) n Vk+1).
For = (T N; φ) 2 CP(T N ; S), dene the function F S ;S which maps any s-linearization = V1V2 : : : of T N to the sequence of the form: F S ;S ( ) = (φ(V1); (V1) GT ) (φ(V2); (V2) (V1)) : : :.
Proposition 1. Given = (T N; φ) 2 CP(T N , S = (M; I; GT )) and an s(i)-linearization = V1V2 : : : of T N , F S ;S ( ) is a step (interleaving) ring schedule of T N from the state S, with intermediate states Sk = (M k; Ik; GT k) (k 0), where M k = φ(Cut(Ek)), GT k = (Vk), and Ik(t) = { un(Vdke)ned T;OE ;S (Cut(Ek); t); iofthte2rwEisne(,M k); Here, (V0) = GT .
there is a unique (up to an isomorphism) time process 2 CP(T N ; S) such that F S ;S ( ) = , where is an s(i)-linearization of T N .
from [
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′, ′); jB′[E′ ) of T N w.r.t. M such that E′ E is a conguration 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 ) 2
Example 4. To illustrate the notions above, rst dene a mapping from the time O-net TgN (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 ′, specied 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
Ls(i)(T N ) = Ls(i)(T N ′), step (interleaving) bisimilar (denoted T N -s(i) T N ′) i there is a relation
states of T N and T N ′, respectively) and for all (S; S′) 2 R it holds: if S (A!;) S1 (S (fa!g; ) S1) in T N , then S′ (A!;) S1′ (S′ (fa!g; ) S1′) in T N ′ and (S1; S′ ) 2 R,
1 and vice versa.
we need auxiliary notions. Given a time Petri net T N , dene the following sets: T racei pr(T N ) = f(fa1g; 1) : : : (fang; n) 2 (2Act T) j 0
n 1 (an!;n) n (n 0) in T N g, T races pr(T N ) = f(A1; 1) : : : (An; n) 2 (NAct T) j 0
n 1 (An!;n) n (n 0) in T N g, T racepom pr(T N ) = fpom( (T N )) j = (T N; φ) 2 CP(T N ; S0)g, T racec pr(T N ) = f[T N ]≃ j = (T N; φ) 2 CP(T N ; S0)g, T raceles pr(T N ) = fles( (T N )) j = (T N; ) 2 OP(T N ; S0)g, T raceo pr(T N ) = f[T N ]≃ j = (T N; ) 2 OP(T N ; S0)g. 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′) 2 R, and for all ( ; ) 2 R, the following holds: 1. whenever b! e in T N and * jEbj = 1, if ⋆ = i pr, * ≼b \ (Eb Eb) = ∅, if ⋆ = s pr, th*en (Td′Nb!)′≃e′ (inTdNT ′N),′,if(⋆e;2e′f)i2 pRr,; sandpr; pom prg,
* TdN ≃ TdN ′, if ⋆ = c pr,
T N and T N ′ are ⋆-bisimilar (denoted T N -⋆ T N ′) i there is ⋆-bisimulation R : T N -⋆ T N ′.
Proposition 2. Let $2 f ; -g and T N $ pr T N ′: 2 fi; sg. Then, T N $
T N ′ ()
T N $⋆ T N ′ i there is a directed path from ) T N T N ′
in Fig. 3.
$⋆ to 2 f ; -g and ⋆; 2 fi pr; s pr; pom pr; c pr; les -i pr ? i pr -s pr ? s pr
and Lemmas considered prior to that. ()) We now demonstrate that it is impossible to draw any arrow from one equivalence 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 prequivalent but not -i prequivalent 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 prequivalent but not s prequivalent because, 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) labeled 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 prequivalent but not pom prequivalent because, 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 actions 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.
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 actions a and time moments 0, are not isomorphic.
Finally, T N 5 and T N 6 are -c prequivalent but not les prequivalent because it is easy to see that the time event structure, corresponding to any maximal time O-processes of T N 6 w.r.t. its initial states, contains two conicting events labeled by actions b and time moments 0, but it is not the case in T N 5. b [0; 0]
T N 3 : H
H
Hj b [0; 5] a [0; 5] ? h ? ? h
T N 5 : h h
Z
T N 4 : h
Z Z~
T N 6 : a [0; 5]