=Paper=
{{Paper
|id=Vol-2951/paper6
|storemode=property
|title=On Semantics for Testing in Time Petri Nets
|pdfUrl=https://ceur-ws.org/Vol-2951/paper6.pdf
|volume=Vol-2951
|authors=Elena Bozhenkova,Irina Virbitskaite
|dblpUrl=https://dblp.org/rec/conf/csp/BozhenkovaV21
}}
==On Semantics for Testing in Time Petri Nets==
https://ceur-ws.org/Vol-2951/paper6.pdf
On Semantics for Testing in Time Petri Nets
Elena Bozhenkova1 , Irina Virbitskaite1
1
A.P. Ershov Institute of Informatics Systems, SB RAS; 6, Lavrentiev av., Novosibirsk, 630090, Russian Federation
Abstract
Dense-Time Petri Nets (TPNs) are now a well-established model to describe and study real time (quanti-
tative) and functional (qualitative) properties of safety-critical, computer-controlled systems. Testing
equivalences, used to compare systems’ behaviors (processes) and reduce the structure of systems, are
defined in terms of tests that processes may or must pass. The intention of the paper is to establish
the interrelations between various semantics for must-testing equivalences with extended tests, in the
framework of TPNs. This allows for studying in detail the timing behavior in addition to the degree of
relative concurrency of processes generated when systems are functioning.
1. Introduction
Dense-Time Petri Nets (TPNs) are suitable for qualitative and quantitative modelling and verify-
ing of safety-critical, computer-controlled, real-time systems. Several semantics (behaviors) are
explored in the literature for TPNs, that can be classified according to interleaving – partial order
dichotomy. The classical interleaving behavior of the TPN is described by runs — sequences of
changes in states by time elapsings and/or transition firings. The semantics allows for analyzing
some safety and liveness properties of systems, however concurrency between net transitions
is reduced to non-deterministic choice between sequences of transitions firings in any possible
order. Step semantics of TPNs generalizes the interleaving approach by allowing several con-
current transitions (forming a step) to fire simultaneously. Partial order semantics of TPNs is
most often represented by means of the so-called causal net processes which include events
and conditions related by causal dependence (the absence of causality means concurrency)
and equipped with timing information. Causal tree semantics summarizes the interleaving
and partial order approaches by representing the behavior of the TPN in the form of a tree
with nodes corresponding to runs, and edges labeled by actions with their times and causal
predecessors.
Testing equivalences [1] are explicitly based on a framework of extracting information about
the systems’ behaviors (processes) by testing them. Two processes are considered equivalent if
there is no test that can distinguish them. In the realm of untimed models, interleaving testing
was thoroughly investigated and well-understood in the setting of models of transition systems
(see [2, 3] among many others). Interleaving, step and partial order testing equivalences for
elementary net systems (safe Petri nets without loops) were studied in [4]. There, the authors
29th International Workshop on Concurrency, Specification and Programming (CS&P’21)
$ bozhenko@iis.nsk.su (E. Bozhenkova); virb@iis.nsk.su (I. Virbitskaite)
https://pdb.iis.nsk.su/en/person/220 (E. Bozhenkova); https://persons.iis.nsk.su/en/virbitskaite (I. Virbitskaite)
0000-0002-9291-7451 (E. Bozhenkova); 0000-0002-4475-3480 (I. Virbitskaite)
© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
indicated the location of the testings among other behavioral equivalences from linear time –
branching time spectrum, providing their hierarchies for the model under consideration with
and without invisible actions. Partial order and non-deterministic semantics for different classes
of Petri nets are often represented by means of various models of event structures. In the
framework of the models, testing equivalences within interleaving – partial order dichotomy
were developed and compared in the papers [5, 6, 7]. Moreover, in [7] special attention was paid
to the relationships between partial order and causal tree semantics in the context of testing
equivalences. To the best of authors’ knowledge, causal tree semantics in the framework of
Petri nets has not been studied yet.
As safety-critical applications often require verification of real time characteristics, testing
equivalences are expanded in concurrent models with time. In the papers [8, 9, 10, 11], alternative
characterizations of timed testing are provided for timed generalizations of interleaving models.
In [12], the testing relations along with their alternative characterization and discretization
were proposed in the framework of Petri nets with time intervals associated to arcs from places
to transitions. At the same time, to the best of our knowledge, there are only few mentions
of a fusion of timing and partial order semantics, in testing scenario. In this regard, the work
[13] is a welcome exception, where time-sensitive testing is investigated within linear time –
branching time spectrum, in the setting of event structure models with time characteristics.
Also, our origin is the paper [14] the main result of which is the coincidence of poset and causal
tree testing equivalences, with the tests as direct extensions of the experiments, in the setting
of TPNs. In this paper, we expand the results of [14] to step, poset and causal tree semantics
with extended tests1 , and demonstrate the discriminating/matching power of the semantics in
the framework of testing equivalences on contact-free TPNs. The results obtained can be useful
in formal verification of systems since partial order semantics allows for reducing the number
of systems’ states to be analyzed.
2. Syntax and Different Semantics of TPNs
In this section, some terminology concerning the model of Petri nets with timing constraints
(time intervals on the firings of transitions) and its concurrent semantics in terms of interleav-
ing/step firing sequences, causal net processes and causal trees are defined.
2.1. Syntax and Interleaving/Step Semantics of TPNs
We start with recalling the definitions of the structure and interleaving/step behavior of time
Petri nets [15, 16]. We use 𝐴𝑐𝑡 as an alphabet of actions and 𝐴𝑐𝑡N as a set of multisets over
𝐴𝑐𝑡. Let the domain T of time values be the set of rational numbers. We denote by [𝜏1 , 𝜏2 ] the
closed interval between two time values 𝜏1 , 𝜏2 ∈ T. Infinity is allowed at the upper bounds of
intervals. Let 𝐼𝑛𝑡𝑒𝑟𝑣 be the set of all such intervals.
Definition 1. • A (labeled over 𝐴𝑐𝑡) time Petri net is a pair 𝒯 𝒩 = (𝒩 , 𝐷), where 𝒩 = (𝑃 ,
𝑇 , 𝐹 , 𝑀0 , 𝐿) is a (labeled over 𝐴𝑐𝑡) underlying Petri net (with a finite set 𝑃 of places, a
1
Testing equivalence with extended tests checks, after the executions of the experiments, the tests that are
continuations of the experiments with steps/posets of actions, not with single actions.
finite set 𝑇 of transitions such that 𝑃 ∩ 𝑇 = ∅ and 𝑃 ∪ 𝑇 ̸= ∅, a flow relation 𝐹 ⊆
(𝑃 × 𝑇 ) ∪ (𝑇 × 𝑃 ), an initial marking ∅ =
̸ 𝑀0 ⊆ 𝑃 , a labeling function 𝐿 : 𝑇 → 𝐴𝑐𝑡) and
𝐷 : 𝑇 → 𝐼𝑛𝑡𝑒𝑟𝑣 is a static timing function associating with each transition a time interval.
For a transition 𝑡 ∈ 𝑇 , the boundaries of the interval 𝐷(𝑡) ∈ 𝐼𝑛𝑡𝑒𝑟𝑣 are called the earliest
firing time 𝐸𝑓 𝑡 and latest firing time 𝐿𝑓 𝑡 of 𝑡. For 𝑥 ∈ 𝑃 ∪ 𝑇 , let ∙ 𝑥 = {𝑦 | (𝑦, 𝑥) ∈ 𝐹 }
and 𝑥∙ = {𝑦 ⋃︀ preset and postset of 𝑥, respectively. For 𝑋 ⊆ 𝑃 ∪ 𝑇 ,
| (𝑥, 𝑦) ∈ 𝐹 } be the⋃︀
define 𝑋 = 𝑥∈𝑋 𝑥 and 𝑋 = 𝑥∈𝑋 𝑥∙ .
∙ ∙ ∙
• A marking 𝑀 of 𝒯 𝒩 is any subset of 𝑃 . A transition 𝑡 ∈ 𝑇 is enabled at a marking
𝑀 if ∙ 𝑡 ⊆ 𝑀 . Let 𝐸𝑛(𝑀 ) be the set of transitions enabled at 𝑀 . A non-empty subset
∅ ̸= 𝑈 ⊆ 𝑇 is a step enabled at a marking 𝑀 , if (∀𝑡 ∈ 𝑈 ◇ 𝑡 ∈ 𝐸𝑛(𝑀 )) and (∀𝑡 ̸= 𝑡′ ∈
𝑈 : (∙ 𝑡 ∪ 𝑡∙ ) ∩ (∙ 𝑡′ ∪ 𝑡′∙ ) = ∅).
A state of 𝒯 𝒩 is a pair (𝑀, 𝐼), where 𝑀 is a marking and 𝐼 : 𝐸𝑛(𝑀 ) −→ T is a dynamic
timing function. The initial state of 𝒯 𝒩 is a pair 𝑆0 = (𝑀0 , 𝐼0 ), where 𝑀0 is the initial
marking and 𝐼0 (𝑡) = 0, for all 𝑡 ∈ 𝐸𝑛(𝑀0 ).
A step 𝑈 enabled at a marking 𝑀 can fire from a state 𝑆 = (𝑀, 𝐼) after a delay time
𝜃 ∈ T if (𝐸𝑓 𝑡(𝑡) ≤ 𝐼(𝑡) + 𝜃), for all 𝑡 ∈ 𝑈 , and (𝐼(𝑡′ ) + 𝜃 ≤ 𝐿𝑓 𝑡(𝑡′ )), for all 𝑡′ ∈ 𝐸𝑛(𝑀 ).
The firing of a step 𝑈 that can fire from a state 𝑆 = (𝑀, 𝐼) after a delay time 𝜃 leads to the
(𝑈,𝜃)
new state 𝑆 ′ = (𝑀 ′ , 𝐼 ′ ) (denoted 𝑆 −→ 𝑆 ′ ) given by:
𝑈
(𝑎) 𝑀 −→ 𝑀 ′ ,
⎨ 𝐼(𝑡′ ) + 𝜃, if 𝑡′ ∈ 𝐸𝑛(𝑀 ∖ ∙ 𝑡),
⎧
(𝑏) ∀𝑡′ ∈ 𝑇 ◇ 𝐼 ′ (𝑡′ ) = 0, if 𝑡′ ∈ 𝐸𝑛(𝑀 ′ ) ∖ 𝐸𝑛(𝑀 ∖ ∙ 𝑡),
undefined, otherwise.
⎩
(𝐴,𝜃)
Then, we write 𝑆 −→ 𝑆 ′ , if 𝐴 = 𝐿(𝑈 ) = Σ𝑡∈𝑈 𝐿(𝑡) ∈ 𝐴𝑐𝑡N , i.e. 𝐴 is a multiset
𝜎
over the set {𝑎 ∈ 𝐴𝑐𝑡 | 𝑎 = 𝐿(𝑡) and 𝑡 ∈ 𝑈 }. We use the notation 𝑆 −→ 𝑆 ′ iff
(𝑈1 ,𝜃1 ) (𝑈𝑘 ,𝜃𝑘 )
𝜎 = (𝑈1 , 𝜃1 ) . . . (𝑈𝑘 , 𝜃𝑘 ) and 𝑆 = 𝑆 0 −→ 𝑆 1 . . . 𝑆 𝑘−1 −→ 𝑆 𝑘 = 𝑆 ′ (𝑘 ≥ 0). In this
case, 𝜎 is a step firing sequence of 𝒯 𝒩 from 𝑆 (to 𝑆 ′ ), and 𝑆 ′ is a reachable state of 𝒯 𝒩
from 𝑆. Whenever | 𝑈𝑖 |= 1 for all 1 ≤ 𝑖 ≤ 𝑘, we call 𝜎 an interleaving firing sequence
of 𝒯 𝒩 . Let ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 ) be the set of all step (interleaving) firing sequences of 𝒯 𝒩 from
𝑆0 , and 𝑅𝑆(𝒯 𝒩 ) be the set of all reachable states of 𝒯 𝒩 from 𝑆0 . For 𝜎 = (𝑈1 , 𝜃1 ) . . .
(𝑈𝑘 , 𝜃𝑘 ) ∈ ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 ), 𝐿(𝜎) = (𝐴1 , 𝜃1 ) . . . (𝐴𝑘 , 𝜃𝑘 ) iff 𝐴𝑖 = 𝐿(𝑈𝑖 ) for all 1 ≤ 𝑖 ≤ 𝑘.
We call 𝒯 𝒩 𝑇 -restricted iff ∙ 𝑡 ̸= ∅ =
̸ 𝑡∙ , for all transitions 𝑡 ∈ 𝑇 ; contact-free iff whenever
a step 𝑈 can fire from the state 𝑆 = (𝑀, 𝐼) after some delay time 𝜃, then (𝑀 ∖ ∙ 𝑈 )∩𝑈 ∙ = ∅,
for all 𝑆 ∈ 𝑅𝑆(𝒯 𝒩 ). In what follows, we shall consider only 𝑇 -restricted and contact-free
time Petri nets.
Example 1. A (labeled over 𝐴𝑐𝑡 = {𝑎, 𝑏, 𝑐}) time Petri net 𝒯̃︂ 𝒩 is shown in Figure 1. Here,
the places are represented by circles, and transitions — by bars; the names are depicted near the
net elements, the flow relation is drawn by the arcs, the initial marking is represented as the set
of the places with tokens (bold points), and the values of the labeling and timing functions are
𝑏, 𝑡3 [1, 3] 𝑝1 𝑎, 𝑡2 [1, 3]
𝑝2
𝑝3 𝑎, 𝑡4 [0, 2]
𝑎, 𝑡1 [0, 1] 𝑐, 𝑡5 [0, 2]
𝑝4 𝑝5
Figure 1: The TPN 𝒯̃︂
𝒩.
printed next to the transitions. It is not difficult to check that 𝑡1 , 𝑡2 and 𝑡4 are transitions enabled
at the initial marking 𝑀0 = {𝑝1 , 𝑝2 }, and, moreover, {𝑡1 , 𝑡4 } and {𝑡2 , 𝑡4 } are steps enabled
at 𝑀0 . The {︂ steps can fire from the initial state 𝑆0 = (𝑀0 , 𝐼0 ) after time delay 𝜃1 = 1, where
0, if 𝑡 ∈ {𝑡1 , 𝑡2 , 𝑡4 },
𝐼0 (𝑡) = The sequence 𝜎 = ({𝑡1 , 𝑡4 }, 0.5) (𝑡3 , 1) (𝑡2 , 2)
𝑢𝑛𝑑𝑒𝑓 𝑖𝑛𝑒𝑑, otherwise.
(𝑡5 , 2) is a step firing sequence of 𝒯̃︂ 𝒩 from 𝑆0 . Also, we have 𝐿(𝜎) = (2′ 𝑎, 0.5) (𝑏, 1) (𝑎, 2)
(𝑐, 2). Furthermore, it is easy to see that 𝒯̃︂ 𝒩 is really 𝑇 -restricted and contact-free.
2.2. Causal Net Process Semantics of TPNs
In this subsection, the concept of causality-based net processes is presented in the context of
TPNs.
We start with the definition of time causal nets, whose events and conditions are related by
causal dependence and concurrency (absence of causality), and whose timing function associates
with the events their occurrence times.
Definition 2. A (labeled over 𝐴𝑐𝑡) time causal net is a finite, acyclic net 𝑇 𝑁 = (𝐵, 𝐸, 𝐺, 𝑙, 𝜏 )
with a set 𝐵 of conditions; a set 𝐸 of events; a flow relation 𝐺 ⊆ (𝐵 × 𝐸) ∪ (𝐸 × 𝐵) such that
| ∙ 𝑏 |≤ 1 ≥| 𝑏∙ |, for all 𝑏 ∈ 𝐵, and ∙ 𝐵 = 𝐸 = 𝐵 ∙ ; a labeling function 𝑙 : 𝐸 → 𝐴𝑐𝑡, and a
timing function 𝜏 : 𝐸 → T such that 𝑒 𝐺+ 𝑒′ ⇒ 𝜏 (𝑒) ≤ 𝜏 (𝑒′ ).
For a time causal net 𝑇 𝑁 = (𝐵, 𝐸, 𝐺, 𝑙, 𝜏 ) and 𝑒, 𝑒′ ∈ 𝐸, define:
• 𝑇 𝑁 ∙ = {𝑏 ∈ 𝐵 | 𝑏∙ = ∅};
• ≺= 𝐺+ , ⪯= 𝐺* (causality);
• 𝑃 𝑟𝑒𝑑𝑒𝑐(𝑒) = {𝑒′ ∈ 𝐸 | 𝑒′ ≺ 𝑒} (causal predecessors of 𝑒), 𝐸𝑎𝑟𝑙𝑖𝑒𝑟(𝑒) = {𝑒′ ∈
𝐸 | 𝜏 (𝑒′ ) < 𝜏 (𝑒)} (time predecessors of 𝑒), and 𝐶𝑢𝑡(𝑒) = (𝐸𝑎𝑟𝑙𝑖𝑒𝑟(𝑒)∙ ∪ ∙ 𝑇 𝑁 ) ∖
∙ 𝐸𝑎𝑟𝑙𝑖𝑒𝑟(𝑒);
• 𝐸 ′ is a downward-closed subset of 𝐸 iff 𝐸 ′ ⊂ 𝐸 and 𝑃 𝑟𝑒𝑑𝑒𝑐(𝑒′ ) ⊆ 𝐸 ′ , for all 𝑒′ ∈ 𝐸 ′ ; a
timely sound subset of 𝐸 iff 𝐸 ′ ⊂ 𝐸 and 𝐸𝑎𝑟𝑙𝑖𝑒𝑟(𝑒′ ) ⊆ 𝐸 ′ , for all 𝑒′ ∈ 𝐸 ′ ;
• 𝑒 ⌣ 𝑒′ ⇐⇒ ¬((𝑒 ≺ 𝑒′ ) ∨ (𝑒′ ≺ 𝑒)) (concurrency); ∅ = ̸ 𝑉 ⊆ 𝐸 is a step iff 𝑒 ⌣ 𝑒′
and 𝜏 (𝑒) = 𝜏 (𝑒 ) for all 𝑒 ̸= 𝑒 ∈ 𝑉 . Let 𝜏 (𝑉 ) = 𝜏 (𝑒) for some 𝑒 ∈ 𝑉 (time of 𝑉 );
′ ′
• a sequence (𝑘 of steps of is an iff
⋃︀
𝜌 = 𝑉 1 . . . 𝑉𝑘 ≥ 0) 𝑇 𝑁 s-linearization of 𝑇 𝑁 1≤𝑖≤𝑘 𝑉𝑖 =
𝐸 and 1≤𝑖≤𝑘>1 𝑉𝑖 = ∅ (i.e. every⋃︀event of 𝑇 𝑁 appears in the sequence exactly once),
⋂︀
and for⋃︀all 1 ≤ 𝑖 < 𝑗 ≤ 𝑘 it holds: 1≤𝑙≤𝑖 𝑉𝑙 is a downward-closed and timely sound sub-
set of 1≤𝑚≤𝑗 𝑉𝑚 (i.e. both causal and time order are preserved: for all 1 ≤ 𝑖 < 𝑗 ≤ 𝑘,
¬((𝑒′ ≺ 𝑒) ∨ (𝜏 (𝑒′ ) < 𝜏 (𝑒))), for all 𝑒 ∈ 𝑉𝑖 , 𝑒′ ∈ 𝑉𝑗 ). Whenever | 𝑉𝑖 | = 1 for all
1 ≤ 𝑖 ≤ 𝑘, 𝜌 is an 𝑖-linearization;
• 𝜂(𝑇 𝑁 ) = (𝐸𝑇 𝑁 , ⪯𝑇 𝑁 ∩(𝐸𝑇 𝑁 × 𝐸𝑇 𝑁 ), 𝑙𝑇 𝑁 , 𝜏𝑇 𝑁 ) is a time poset2 . For time posets
𝜂 = (𝐸, ⪯, 𝑙, 𝜏 ) and 𝜂 ′ = (𝐸 ′ , ⪯′ , 𝑙′ , 𝜏 ′ ), 𝜂 is a pos-extension of 𝜂 ′ iff 𝐸 ′ is a downward-
closed and timely sound subset of 𝐸, ⪯′ =⪯ ∩𝐸 ′ × 𝐸 ′ , 𝑙′ = 𝑙 |𝐸 ′ , and 𝜏 ′ = 𝜏 |𝐸 ′ .
We are now ready to define the concept of causal net based processes of TPNs, proposed in
[15].
Definition 3. Given a time Petri net 𝒯 𝒩 = ((𝑃 , 𝑇 , 𝐹 , 𝑀0 , 𝐿), 𝐷) and a time causal net
𝑇 𝑁 = (𝐵, 𝐸, 𝐺, 𝑙, 𝜏 ),
• a mapping 𝜙 : 𝐵 ∪ 𝐸 → 𝑃 ∪ 𝑇 is a homomorphism from 𝑇 𝑁 to 𝒯 𝒩 iff the following
hold:
– 𝜙(𝐵) ⊆ 𝑃 , 𝜙(𝐸) ⊆ 𝑇 ;
– the restriction of 𝜙 to ∙ 𝑒 is a bijection between ∙ 𝑒 and ∙ 𝜙(𝑒), and the restriction of 𝜙
to 𝑒∙ is a bijection between 𝑒∙ and 𝜙(𝑒)∙ , for all 𝑒 ∈ 𝐸;
– the restriction of 𝜙 to ∙ 𝑇 𝑁 is a bijection between ∙ 𝑇 𝑁 and 𝑀0 ;
– 𝑙(𝑒) = 𝐿(𝜙(𝑒)), for all 𝑒 ∈ 𝐸.
• a pair 𝜋 = (𝑇 𝑁, 𝜙) is a time process of a time Petri net 𝒯 𝒩 iff 𝑇 𝑁 is a time causal net
and 𝜙 is a homomorphism from 𝑇 𝑁 to 𝒯 𝒩 ;
• a time process 𝜋 = (𝑇 𝑁, 𝜙) of 𝒯 𝒩 is correct iff for all 𝑒 ∈ 𝐸 it holds:
(a) 𝜏 (𝑒) ≥ TOE𝜋 (∙ 𝑒, 𝜙(𝑒)) + 𝐸𝑓 𝑡(𝜙(𝑒)),
(b) ∀𝑡 ∈ 𝐸𝑛(𝜙(𝐶𝑢𝑡(𝑒))) ◇ 𝜏 (𝑒) ≤ TOE𝜋 (𝐶𝑢𝑡(𝑒), 𝑡) + 𝐿𝑓 𝑡(𝑡).
Here, for a subset 𝐵 ′ ⊆ 𝐵𝑇 𝑁 and a transition 𝑡 ∈ 𝐸𝑛(𝜙(𝐵 ′ )), the time of enabling (TOE)
of 𝑡, i.e. the latest global time moment when
(︁ tokens appear in all input places)︁ of 𝑡, is
defined as follows: TOE𝜋 (𝐵 , 𝑡) = max {𝜏𝑇 𝑁 (∙ 𝑏) | 𝑏 ∈ 𝐵[𝑡]
′ ′ ∖ ∙ 𝑇 𝑁 } ∪ {0} , where
′ = {𝑏 ∈ 𝐵 ′ | 𝜙 ∙
𝐵[𝑡] 𝑇 𝑁 (𝑏) ∈ 𝑡}.
Let 𝒞𝒫(𝒯 𝒩 ) denote the set of correct time processes of 𝒯 𝒩 .
We now present for the time Petri net the relationships between its correct time processes
and its interleaving/step firing sequences from the initial state.
Proposition 1. [15, 16] Let 𝒯 𝒩 be a time Petri net. Then,
2
A (labeled over 𝐴𝑐𝑡) time poset (partially ordered set) is a tuple 𝜂 = (𝑋, ⪯, 𝜆, 𝜏 ) consisting of a finite set 𝑋
of elements; a reflexive, antisymmetric and transitive relation ⪯; a labeling function 𝑙 : 𝑋 → 𝐴𝑐𝑡; and a timing
function 𝜏 : 𝑋 → T such that 𝑥 ⪯ 𝑥′ ⇒ 𝜏 (𝑥) ≤ 𝜏 (𝑥′ ).
(i) for any 𝜋 = (𝑇 𝑁, 𝜙) ∈ 𝒞𝒫(𝒯 𝒩 ) with an 𝑠(𝑖)-linearization 𝜌 = 𝑉1 . . . 𝑉𝑘 of 𝑇 𝑁 , there
is a unique step (interleaving) firing sequence 𝐹 𝑆𝜋 (𝜌) = (𝜙(𝑉1 ), 𝜏 (𝑉1 ) − 0) . . . (𝜙(𝑉𝑘 ),
𝜏 (𝑉𝑘 ) − 𝜏 (𝑉𝑘−1 )) ∈ ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 );
(ii) for any step (interleaving) firing sequence 𝜎 ∈ ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 ), there is a unique (up to
an isomorphism3 ) correct time process 𝜋𝜎 = (𝑇 𝑁, 𝜙) ∈ 𝒞𝒫(𝒯 𝒩 ) with a unique 𝑠(𝑖)-
linearization 𝜌𝜎 of 𝑇 𝑁 such that 𝐹 𝑆𝜋𝜎 (𝜌𝜎 ) = 𝜎.
For correct time processes 𝜋 = (𝑇 𝑁, 𝜙), 𝜋 ′ = (𝑇 𝑁 ′ , 𝜙′ ) ∈ 𝒞𝒫(𝒯 𝒩 ), we say that 𝜋 is a
𝑝𝑜𝑠-extension of 𝜋 ′ in 𝒯 𝒩 iff 𝜂(𝑇 𝑁 ) is 𝑝𝑜𝑠-extension of 𝜂(𝑇 𝑁 ′ ), 𝐵 ′ ⊂ 𝐵, 𝐺′ = 𝐺 ∩ (𝐵 ′ ×
𝐸 ′ ∪ 𝐸 ′ × 𝐵 ′ ), and 𝜙′ = 𝜙 |𝐵 ′ ∪𝐸 ′ .
We expand the above results to 𝑝𝑜𝑠-extensions of correct time processes of TPNs.
Lemma 1. Given a time Petri net 𝒯 𝒩 , 𝜎 ∈ ℱ 𝒮 𝑠(𝑖) (𝒯 𝒩 ), and 𝜋 ∈ 𝒞𝒫(𝒯 𝒩 ) such that 𝜎 =
𝐹 𝑆𝜋 (𝜌), where 𝜌 is an 𝑠(𝑖)-linearization of 𝑇 𝑁𝜋 ,
̃︀ is a 𝑝𝑜𝑠-extension of 𝜋 in 𝒯 𝒩 , then there is 𝜎𝜎 ′ ∈ ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 ) such that 𝜎𝜎 ′ =
(i) if 𝜋
𝐹 𝑆𝜋̃︀ (𝜌𝜌′ ), where 𝜌𝜌′ is an 𝑠(𝑖)-linearization of 𝑇 𝑁𝜋̃︀ ;
(ii) if 𝜎𝜎 ′ ∈ ℱ𝒮 𝑠(𝑖) (𝒯 𝒩 ), there is 𝜋
̃︀ ∈ 𝒞𝒫(𝒯 𝒩 ) such that 𝜋 ̃︀ is a 𝑝𝑜𝑠-extension of 𝜋 in 𝒯 𝒩
and 𝜎𝜎 ′ = 𝐹 𝑆𝜋̃︀ (𝜌𝜌′ ), where 𝜌𝜌′ is an 𝑠(𝑖)-linearization of 𝑇 𝑁𝜋̃︀ .
2.3. Causal Tree Semantics of TPNs
Causal trees [17] are synchronisation trees which carry in their labels additional information
about causes of actions thus providing us with an interleaving description of concurrent pro-
cesses, which faithfully expresses causality. Time causal trees are generalizations of causal
trees by adding timing. In the time causal tree of the TPN, the nodes are the interleaving firing
sequences of the TPN, and an edge exists between two nodes if the second one is a direct
extension of the first one. The causes in the edge labels are calculated based on the causality
relations in the correct time processes of the TPN corresponding to the nodes (the interleaving
firing sequences).
Definition 4. The time causal tree of the TPN 𝒯 𝒩 , 𝑇 𝐶𝑇 (𝒯 𝒩 ), is a tree (ℱ𝒮 𝑖 (𝒯 𝒩 ), 𝐸𝑑, 𝜑),
where ℱ𝒮 𝑖 (𝒯 𝒩 ) is the set of nodes with the root 𝜖; 𝐸𝑑 = {(𝜎, 𝜎(𝑡, 𝜃)) | 𝜎, 𝜎(𝑡, 𝜃) ∈ ℱ𝒮(𝒯 𝒩 )}
is the set of edges; 𝜑 is the labeling function such that 𝜑(𝜖) = 𝜖 and 𝜑(𝜎, 𝜎(𝑡, 𝜃)) = (𝐿𝒯 𝒩 (𝑡), 𝜃,
𝐾), with 𝜎 = 𝐹 𝑆𝜋𝜎 (𝜌𝜎 = 𝑒1 . . . 𝑒𝑛 ), 𝜎(𝑡, 𝜃) = 𝐹 𝑆𝜋𝜎(𝑡,𝜃) (𝜌𝜎(𝑡,𝜃) = 𝑒1 . . . 𝑒𝑛 𝑒), 𝐾 = {𝑛−𝑙 +1 |
𝑒𝑙 ≺𝑇 𝑁𝜋𝜎(𝑡,𝜃) 𝑒}. Let 𝑝𝑎𝑡ℎ(𝜎) be the path starting from the root and finishing in the node 𝜎 of
𝑇 𝐶𝑇 (𝒯 𝒩 )4 .
3
Time processes 𝜋 = (𝑇 𝑁, 𝜙) and 𝜋 ′ = (𝑇 𝑁 ′ , 𝜙′ ) ∈ 𝒞𝒫(𝒯 𝒩 ) are isomorphic (denoted 𝜋 ≃ 𝜋 ′ ) iff there exists
a bijective mapping 𝛽 : 𝐵 ∪ 𝐸 → 𝐵 ′ ∪ 𝐸 ′ such that (i) 𝛽(𝐵) = 𝐵 ′ and 𝛽(𝐸) = 𝐸 ′ ; (ii) 𝑥 𝐺 𝑦 ⇐⇒ 𝛽(𝑥) 𝐺′ 𝛽(𝑦),
for all 𝑥, 𝑦 ∈ 𝐵 ∪ 𝐸; (iii) 𝑙(𝑒) = 𝑙′ (𝛽(𝑒)), for all 𝑒 ∈ 𝐸; (iv) 𝜏 (𝑒) = 𝜏 ′ (𝛽(𝑒)), for all 𝑒 ∈ 𝐸; (v) 𝜙(𝑥) = 𝜙′ (𝛽(𝑥)),
for all 𝑥 ∈ 𝐵 ∪ 𝐸.
4
We assume 𝑝𝑎𝑡ℎ(𝜖) = 𝜖. Notice that in 𝑇 𝐶𝑇 (𝒯 𝒩 ), for any node 𝜎 ∈ ℱ𝒮 𝑖 (𝒯 𝒩 ), there is a path starting
from the root and finishing in 𝜎.
Example 2. Consider the time Petri net 𝒯̃︂ 𝒩 (see Figure 1) and its interleaving firing sequence
𝜎 = (𝑡1 , 0.5) (𝑡4 , 0) (𝑡3 , 1) (𝑡2 , 2) (𝑡5 , 2) ∈ ℱ 𝒮 𝑖 (𝒯̃︂
𝒩 ). It is easy to get that 𝜑(𝑝𝑎𝑡ℎ(𝜎)) =
(𝑎, 0.5, ∅) (𝑎, 0.5, ∅) (𝑏, 1, {2}) (𝑎, 2, {1}) (𝑐, 2, {1, 3}).
We finally establish some relationships between correct time processes and labeled paths in
the time causal trees of two time Petri nets.
Proposition 2. Let 𝒯 𝒩 , 𝒯 𝒩 ′ be time Petri nets. Then,
(i) for any 𝜋 ∈ 𝒞𝒫(𝒯 𝒩 ) and 𝜋 ′ ∈ 𝒞𝒫(𝒯 𝒩 ′ ) with an isomorphism 𝑓 : 𝜂(𝑇 𝑁𝜋 ) → 𝜂(𝑇 𝑁𝜋′ ),
𝜑(𝑝𝑎𝑡ℎ(𝐹 𝑆𝜋 (𝜌))) = 𝜑′ (𝑝𝑎𝑡ℎ(𝐹 𝑆𝜋′ (𝑓 (𝜌)))), for any 𝑖-linearization 𝜌 of 𝑇 𝑁𝜋 ;
(ii) for any 𝜎 ∈ ℱ𝒮 𝑖 (𝒯 𝒩 ) and 𝜎 ′ ∈ ℱ𝒮 𝑖 (𝒯 𝒩 ′ ) such that 𝜑(𝑝𝑎𝑡ℎ(𝜎)) = 𝜑′ (𝑝𝑎𝑡ℎ(𝜎 ′ )), there
is an isomorphism 𝑓 : 𝜂(𝑇 𝑁𝜋𝜎 ) → 𝜂(𝑇 𝑁𝜋𝜎′ ) such that 𝑓 (𝜌𝜎 ) = 𝜌𝜎′ .
3. Testing Equivalences
Interleaving testing equivalence deals with the experiments on the TPN — sequences of actions
with their times — and the behaviors which are tested for after the experiments — sets of actions
with their times. So, it checks whether actions with times, given as a test, can be executed after
a sequence of actions with times, specified as an experiment. Here, both the experiments and
tests represent interleaving semantics.
Definition 5. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ ,
• for a sequence 𝑤 ∈ (𝐴𝑐𝑡 × T)* and a set 𝑊 ⊆ (𝐴𝑐𝑡 × T), 𝒯 𝒩 after 𝑤 MUST𝑖𝑛𝑡 𝑖𝑛𝑡 𝑊
iff for all firing sequences 𝜎 ∈ ℱ𝒮 𝑖 (𝒯 𝒩 ) such that 𝐿(𝜎) = 𝑤, there exists an element
(𝑎, 𝜃) ∈ 𝑊 and a firing sequence 𝜎(𝑡, 𝜃) ∈ ℱ𝒮 𝑖 (𝒯 𝒩 ) such that 𝐿(𝜎(𝑡, 𝜃)) = 𝑤(𝑎, 𝜃);
• 𝒯 𝒩 and 𝒯 𝒩 ′ are interleaving testing equivalent (denoted 𝒯 𝒩 ∼𝑖𝑛𝑡 ′
𝑖𝑛𝑡 𝒯 𝒩 ) iff for all
*
sequences 𝑤 ∈ (𝐴𝑐𝑡 × T) and for all sets 𝑊 ⊆ (𝐴𝑐𝑡 × T), it holds:
′
𝒯 𝒩 after 𝑤 MUST𝑖𝑛𝑡 𝑖𝑛𝑡
𝑖𝑛𝑡 𝑊 ⇐⇒ 𝒯 𝒩 after 𝑤 MUST𝑖𝑛𝑡 𝑊.
In step testing, the experiments on the TPN are sequences of multisets over sets of actions
with their times and the tests checked after the experiments are sets of multisets over sets of
actions with their times. So, it checks whether multisets over sets of actions with times, given
as a test, can be executed after a sequence of multisets over sets of actions with times, specified
as an experiment. Thereby, both the experiments and tests respect step semantics.
Definition 6. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ ,
• for a sequence 𝑤 ∈ (𝐴𝑐𝑡N × T)* and a set 𝑊 ⊆ (𝐴𝑐𝑡N × T), 𝒯 𝒩 after 𝑤 MUST𝑠𝑡𝑒𝑝 𝑠𝑡𝑒𝑝
𝑊 iff for all firing sequences 𝜎 ∈ ℱ𝒮 𝑠 (𝒯 𝒩 ) such that 𝐿(𝜎) = 𝑤, there exists an element
(𝐴, 𝜃) ∈ 𝑊 and a firing sequence 𝜎(𝑈, 𝜃) ∈ ℱ𝒮 𝑠 (𝒯 𝒩 ) such that 𝐿(𝜎(𝑈, 𝜃)) = 𝑤(𝐴, 𝜃);
𝒯 𝒩1 :
𝑎[1, 1] 𝑏[1, 2] 𝒯 𝒩2 :
𝑏[0, 0] 𝑏[0, 1] 𝑎[0, 0] 𝑎[1, 1] 𝑏[1, 1]
𝑠𝑡𝑒𝑝
Figure 2: The ∼𝑖𝑛𝑡 𝑝𝑜𝑠
𝑖𝑛𝑡 –equivalent but neither ∼𝑠𝑡𝑒𝑝 – nor ∼𝑝𝑜𝑠 –equivalent TPNs 𝒯 𝒩 1 and 𝒯 𝒩 2 .
𝒯 𝒩3 : 𝒯 𝒩4 :
𝑏[0, 0] 𝑏[0, 0] 𝑏[0, 0] 𝑏[0, 0]
𝑎[2, 3] 𝑎[2, 3] 𝑎[2, 3] 𝑎[2, 3] 𝑎[2, 3]
Figure 3: The ∼𝑠𝑡𝑒𝑝 𝑝𝑜𝑠
𝑠𝑡𝑒𝑝 –equivalent but not ∼𝑝𝑜𝑠 –equivalent TPNs 𝒯 𝒩 3 and 𝒯 𝒩 4 .
• 𝒯 𝒩 and 𝒯 𝒩 ′ are step testing equivalent (denoted 𝒯 𝒩 ∼𝑠𝑡𝑒𝑝 ′
𝑠𝑡𝑒𝑝 𝒯 𝒩 ) iff for all sequences
𝑤 ∈ (𝐴𝑐𝑡N × T)* and for all sets 𝑊 ⊆ (𝐴𝑐𝑡N × T), it holds:
𝒯 𝒩 after 𝑤 MUST𝑠𝑡𝑒𝑝 ′ 𝑠𝑡𝑒𝑝
𝑠𝑡𝑒𝑝 𝑊 ⇐⇒ 𝒯 𝒩 after 𝑤 MUST𝑠𝑡𝑒𝑝 𝑊.
The idea of partial order testing is that the experiments on the TPN are time posets and the
tests, that are examined after the experiments, are sets of 𝑝𝑜𝑠-extensions of the experiments.
This contrasts with partial order based testing investigated in the paper in [14], where the tests
contain sets of time posets extending the experiments by single actions with their times. From
now on, we denote 𝑝𝑜𝑠-extensions of a time poset 𝑇 𝑃 by TP𝑇 𝑃 .
Definition 7. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ ,
• for a time poset 𝑇 𝑃 and a set TP ⊆ TP𝑇 𝑃 , 𝒯 𝒩 after 𝑇 𝑃 MUST𝑝𝑜𝑠 𝑝𝑜𝑠 TP iff for all
time processes 𝜋 = (𝑇 𝑁, 𝜙) ∈ 𝒞𝒫(𝒯 𝒩 ) and for all isomorphisms 𝑓 : 𝜂(𝑇 𝑁 ) −→ 𝑇 𝑃 ,
𝒯 𝒩5 : 𝒯 𝒩6 :
𝑏[0, 0] 𝑏[0, 0] 𝑏[0, 0] 𝑏[0, 0]
𝑐[1, 4] 𝑎[1, 4] 𝑎[1, 4] 𝑐[1, 4] 𝑎[1, 4] 𝑎[1, 4] 𝑎[4, 4]
Figure 4: The ∼⋆⋆ –equivalent TPNs 𝒯 𝒩 5 and 𝒯 𝒩 6 , for ⋆ ∈ {𝑖𝑛𝑡, 𝑠𝑡𝑒𝑝, 𝑝𝑜𝑠}.
there exists a time poset 𝑇 𝑃 ′ ∈ TP, a time process 𝜋 ′ = (𝑇 𝑁 ′ , 𝜙′ ) ∈ 𝒞𝒫(𝒯 𝒩 ), and an
isomorphism 𝑓 ′ : 𝜂(𝑇 𝑁 ′ ) −→ 𝑇 𝑃 ′ , such that 𝜋 ′ is a 𝑝𝑜𝑠-extension of 𝜋 and 𝑓 ⊂ 𝑓 ′ ;
• 𝒯 𝒩 and 𝒯 𝒩 ′ are poset testing equivalent (denoted 𝒯 𝒩 ∼𝑝𝑜𝑠 ′
𝑝𝑜𝑠 𝒯 𝒩 ) iff for all time posets
𝑇 𝑃 and for all sets TP ⊆ TP𝑇 𝑃 , it holds:
′
𝒯 𝒩 after 𝑇 𝑃 MUST𝑝𝑜𝑠 𝑝𝑜𝑠
𝑝𝑜𝑠 TP ⇐⇒ 𝒯 𝒩 after 𝑇 𝑃 MUST𝑝𝑜𝑠 TP.
Theorem 1. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ ,
′ 𝑠𝑡𝑒𝑝 ′
𝒯 𝒩 ∼𝑝𝑜𝑠 𝑖𝑛𝑡
𝑝𝑜𝑠 𝒯 𝒩 =⇒ 𝒯 𝒩 ∼𝑠𝑡𝑒𝑝 𝑇 𝑁 =⇒ 𝒯 𝒩 ∼𝑖𝑛𝑡 𝒯 𝒩 .
The implications in the theorem above do not hold in the opposite directions, as demonstrated
in the example below.
Example 3. The time Petri nets 𝒯 𝒩 1 and 𝒯 𝒩 2 , shown in Figure 2, are ∼𝑖𝑛𝑡 𝑖𝑛𝑡 –equivalent but
they are neither ∼𝑠𝑡𝑒𝑝
𝑠𝑡𝑒𝑝 – nor ∼ 𝑝𝑜𝑠
𝑝𝑜𝑠 –equivalent. First, check that 𝒯 𝒩 1 and 𝒯 𝒩 𝑠𝑡𝑒𝑝
2 are not ∼𝑠𝑡𝑒𝑝 –
equivalent. It is easy to see that 𝒯 𝒩 1 after 𝑤 = (1′ 𝑎 + 1′ 𝑏, 1) MUST𝑠𝑡𝑒𝑝 𝑠𝑡𝑒𝑝 𝑊 = ∅, because
in ℱ𝒮 𝑠 (𝒯 𝒩 1 ) there is no firing sequence 𝜎 such that 𝐿(𝜎) = 𝑤. However, this is not the
case in 𝒯 𝒩 2 , since in ℱ𝒮 𝑠 (𝒯 𝒩 2 ) there exists a firing sequence 𝜎 such that 𝐿(𝜎) = 𝑤 and it
is impossible to find any element (𝐴, 𝜃) of 𝑊 so as to locate in ℱ𝒮 𝑠 (𝒯 𝒩 2 ) a firing sequence
𝜎(𝑈, 𝜃) such that 𝐿(𝜎(𝑈, 𝜃)) = 𝑤(𝐴, 𝜃). Hence, it hods that ¬(𝒯 𝒩 2 after 𝑤 = (1′ 𝑎 + 1′ 𝑏, 1)
MUST𝑠𝑡𝑒𝑝 𝑝𝑜𝑠
𝑠𝑡𝑒𝑝 𝑊 = ∅). Second, verify that 𝒯 𝒩 1 and 𝒯 𝒩 2 are not ∼𝑝𝑜𝑠 –equivalent. Define
a poset 𝑇 𝑃 = ({𝑥1 , 𝑥2 }, ⪯, 𝜆, 𝜏 ) (with ⪯= {(𝑥1 , 𝑥1 ), (𝑥2 , 𝑥2 )}, 𝜆(𝑥1 ) = 𝑎, 𝜆(𝑥2 ) = 𝑏,
𝜏 (𝑥1 ) = 𝜏 (𝑥2 ) = 1). For any time process 𝜋1 = (𝑇 𝑁1 , 𝜙1 ) ∈ 𝒞𝒫(𝒯 𝒩 1 ), there is no isomorphism
𝑓1 : 𝜂(𝑇 𝑁1 ) −→ 𝑇 𝑃 . So, it is true that 𝒯 𝒩 1 after 𝑇 𝑃 MUST𝑝𝑜𝑠 𝑝𝑜𝑠 TP = ∅. However, this is
not the case in 𝒯 𝒩 2 because there is a time process 𝜋2 = (𝑇 𝑁2 , 𝜙2 ) ∈ 𝒞𝒫(𝒯 𝒩 2 ), with 𝐸𝑇 𝑁2
containing two concurrent events labeled by 𝑎 and 𝑏, both with time value 1, and an isomorphism
𝑓2 : 𝜂(𝑇 𝑁2 ) −→ 𝑇 𝑃 , and we cannot find any 𝑝𝑜𝑠-extension of 𝑇 𝑃 in TP. Hence, it hods that
¬(𝒯 𝒩 2 after 𝑇 𝑃 MUST𝑝𝑜𝑠 𝑝𝑜𝑠 TP = ∅).
The time Petri nets 𝒯 𝒩 3 and 𝒯 𝒩 4 , shown in Figure 3, are ∼𝑠𝑡𝑒𝑝 𝑝𝑜𝑠
𝑠𝑡𝑒𝑝 –equivalent but not ∼𝑝𝑜𝑠 –
equivalent. Let’s make sure of the latter. Define posets 𝑇 𝑃 = ({𝑥1 }, ⪯, 𝜆, 𝜏 ) (with ⪯= {(𝑥1 , 𝑥1 )},
𝜆(𝑥1 ) = 𝑏, 𝜏 (𝑥1 ) = 0) and 𝑇 𝑃 ′ = ({𝑥1 , 𝑥2 , 𝑥3 , 𝑥4 }, ⪯′ , 𝜆′ , 𝜏 ′ ) (with ⪯′ = {(𝑥𝑖 , 𝑥𝑖 ) | 1 ≤
𝑖 ≤ 4} ∪ {(𝑥2 , 𝑥3 )}, 𝜆′ (𝑥1 ) = 𝜆′ (𝑥2 ) = 𝑏, 𝜆′ (𝑥3 ) = 𝜆′ (𝑥4 ) = 𝑎, 𝜏 ′ (𝑥1 ) = 𝜏 ′ (𝑥2 ) = 0,
and 𝜏 ′ (𝑥3 ) = 𝜏 ′ (𝑥4 ) = 2.9. It is easy to see that 𝑇 𝑃 ′ is a 𝑝𝑜𝑠-extension of 𝑇 𝑃 . For any
time process 𝜋1 = (𝑇 𝑁1 , 𝜙1 ) ∈ 𝒞𝒫(𝒯 𝒩 3 ), with 𝐸𝑇 𝑁1 consisting of an event with label 𝑏
and time value 0, and any isomorphism 𝑓1 : 𝜂(𝑇 𝑁1 ) −→ 𝑇 𝑃 , we can find a 𝑝𝑜𝑠-extension
𝜋1′ = (𝑇 𝑁1′ , 𝜙′1 ) ∈ 𝒞𝒫(𝒯 𝒩 1 ), with 𝐸𝑇 𝑁1′ consisting of two concurrent events, both with label 𝑏
and time value 0, and two concurrent events, both with label 𝑎 and time value 2.9, and, moreover,
one of the two events labeled by 𝑎 is causally preceded by the added event labeled by 𝑏, and an
isomorphism 𝑓1′ : 𝜂(𝑇 𝑁1′ ) −→ 𝑇 𝑃 ′ such that 𝑓1 ⊂ 𝑓1′ . But this is not the case in 𝒯 𝒩 4 .
The time Petri nets 𝒯 𝒩 5 and 𝒯 𝒩 6 , depicted in Figure 4, are ∼⋆⋆ –equivalent, for ⋆ ∈ {𝑖𝑛𝑡, 𝑠𝑡𝑒𝑝,
𝑝𝑜𝑠}. □
At last, the definition of testing equivalence based on the causal trees of TPNs is developed.
In doing so the experiments are considered as sequences over the alphabet (𝐴𝑐𝑡 × T × 2N )
(corresponding to labeled paths from the roots in the causal trees) and the tests are specified as
sets of non-empty sequences over the same alphabet (corresponding to sets of extensions of the
labeled paths in the causal trees). In the paper [14], the tests directly extend the experiments by
single elements, not by sequences of elements, from the set (𝐴𝑐𝑡 × T × 2N ).
Definition 8. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ with their time causal trees 𝑇 𝐶𝑇 (𝒯 𝒩 ) and
𝑇 𝐶𝑇 (𝒯 𝒩 ′ ), respectively,
• for a sequence 𝑤 ∈ (𝐴𝑐𝑡 × T × 2N )* and a set W ⊆ (𝐴𝑐𝑡 × T × 2N )+ , we say 𝑇 𝐶𝑇 (𝒯 𝒩 )
after 𝑤 MUST𝑒𝑥𝑡 𝑐𝑡 W iff for all paths 𝑢 in 𝑇 𝐶𝑇 (𝒯 𝒩 ) from its root to a node 𝑛 such
that 𝜑(𝑢) = 𝑤, there exists 𝑤′ ∈ W and a path 𝑢′ starting from the node 𝑛, such that
𝜑(𝑢′ ) = 𝑤′ ;
• 𝒯 𝒩 and 𝒯 𝒩 ′ are causal tree testing equivalent (𝒯 𝒩 ∼𝑒𝑥𝑡 ′
𝑐𝑡 𝒯 𝒩 ) iff for all sequences
* +
𝑤 ∈ (𝐴𝑐𝑡 × T × 2 ) and sets W ⊆ (𝐴𝑐𝑡 × T × 2 ) , it holds:
N N
′
𝑇 𝐶𝑇 (𝒯 𝒩 ) after 𝑤 MUST𝑒𝑥𝑡 𝑒𝑥𝑡
𝑐𝑡 W ⇐⇒ 𝑇 𝐶𝑇 (𝒯 𝒩 ) after 𝑤 MUST𝑐𝑡 W.
We finally expand the main result of [14] by establishing the coincidence of poset and causal
tree testing equivalences with extended tests, in the setting of TPNs.
Theorem 2. Given time Petri nets 𝒯 𝒩 and 𝒯 𝒩 ′ ,
′ ′
𝒯 𝒩 ∼𝑝𝑜𝑠 𝑒𝑥𝑡
𝑝𝑜𝑠 𝒯 𝒩 ⇐⇒ 𝒯 𝒩 ∼𝑐𝑡 𝒯 𝒩 .
4. Concluding Remarks
We have specified and studied several testing equivalences based on concurrent semantics, in
the setting of contact-free time Petri nets. In doing so, we dealt with various conceptions of the
behavior of the time Petri net: interleaving/step firing sequences, time processes, from causal
nets of which partial orders are derived, and time causal tree, constructed from interleaving
firing sequences and partial orders. We have demonstrated that interleaving testing equivalence
(with the experiments as labeled interleaving firing sequences and with the tests as experiments
extensions by single actions with their times) is coarser than step testing (with the experiments
as labeled step firing sequences and the tests as sequences extensions by steps of concurrent
actions with their times), which, in turn, is coarser than poset testing (with time posets as
experiments and their 𝑝𝑜𝑠-extensions as tests). As the main result, the latter equivalence has
been established to coincide with causal tree testing (based on labeled paths and their extensions
in time causal trees of TPNs).
As for future work, we plan to investigate the equivalences and semantics under consideration
in the framework of Petri nets with weak timing policy [18]. Also, it would be interesting to
see whether open intervals in the specification of TPNs influence the results obtained here.
References
[1] R. de Nicola, M. Hennessy, Testing equivalence for processes, in: J. Díaz (Ed.), Automata,
Languages and Programming, 10th Colloquium, Barcelona, Spain, July 18-22, 1983, Pro-
ceedings, volume 154 of Lecture Notes in Computer Science, Springer, 1983, pp. 548–560.
URL: https://doi.org/10.1007/BFb0036936. doi:10.1007/BFb0036936.
[2] R. de Nicola, Extensional equivalences for transition systems, Acta Informatica 24 (1987)
211–237. URL: https://doi.org/10.1007/BF00264365. doi:10.1007/BF00264365.
[3] R. Cleaveland, M. Hennessy, Testing equivalence as a bisimulation equivalence, Formal
Aspects Comput. 5 (1993) 1–20. URL: https://doi.org/10.1007/BF01211314. doi:10.1007/
BF01211314.
[4] L. Pomello, G. Rozenberg, C. Simone, A survey of equivalence notions for net based
systems, in: G. Rozenberg (Ed.), Advances in Petri Nets 1992, The DEMON Project,
volume 609 of Lecture Notes in Computer Science, Springer, 1992, pp. 410–472. URL: https:
//doi.org/10.1007/3-540-55610-9_180. doi:10.1007/3-540-55610-9\_180.
[5] L. Aceto, History preserving, causal and mixed-ordering equivalence over stable event
structures, Fundam. Informaticae 17 (1992) 319–331.
[6] L. Aceto, R. de Nicola, A. Fantechi, Testing equivalences for event structures, in: M. V. Zilli
(Ed.), Mathematical Models for the Semantics of Parallelism, Advanced School, Rome, Italy,
September 24 - October 1, 1986, Proceedings, volume 280 of Lecture Notes in Computer
Science, Springer, 1986, pp. 1–20. URL: https://doi.org/10.1007/3-540-18419-8_9. doi:10.
1007/3-540-18419-8\_9.
[7] U. Goltz, H. Wehrheim, Causal testing, in: W. Penczek, A. Szalas (Eds.), Mathemat-
ical Foundations of Computer Science 1996, 21st International Symposium, MFCS’96,
Cracow, Poland, September 2-6, 1996, Proceedings, volume 1113 of Lecture Notes in Com-
puter Science, Springer, 1996, pp. 394–406. URL: https://doi.org/10.1007/3-540-61550-4_165.
doi:10.1007/3-540-61550-4\_165.
[8] R. Cleaveland, A. E. Zwarico, A theory of testing for real-time, in: Proceedings of the
Sixth Annual Symposium on Logic in Computer Science (LICS ’91), Amsterdam, The
Netherlands, July 15-18, 1991, IEEE Computer Society, 1991, pp. 110–119. URL: https:
//doi.org/10.1109/LICS.1991.151635. doi:10.1109/LICS.1991.151635.
[9] M. Hennessy, T. Regan, A process algebra for timed systems, Inf. Comput. 117 (1995)
221–239. URL: https://doi.org/10.1006/inco.1995.1041. doi:10.1006/inco.1995.1041.
[10] F. Corradini, W. Vogler, L. Jenner, Comparing the worst-case efficiency of asynchronous
systems with PAFAS, Acta Informatica 38 (2002) 735–792. URL: https://doi.org/10.1007/
s00236-002-0094-3. doi:10.1007/s00236-002-0094-3.
[11] L. F. L. Díaz, D. de Frutos-Escrig, Denotational semantics for timed testing, in: M. Bertran,
T. Rus (Eds.), Transformation-Based Reactive Systems Development, 4th International
AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software,
ARTS’97, Palma, Mallorca, Spain, May 21-23, 1997, Proceedings, volume 1231 of Lec-
ture Notes in Computer Science, Springer, 1997, pp. 368–382. URL: https://doi.org/10.1007/
3-540-63010-4_25. doi:10.1007/3-540-63010-4\_25.
[12] E. Bihler, W. Vogler, Timed Petri nets: Efficiency of asynchronous systems, in: M. Bernardo,
F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems, International
School on Formal Methods for the Design of Computer, Communication and Software
Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004, Revised Lectures, volume
3185 of Lecture Notes in Computer Science, Springer, 2004, pp. 25–58. URL: https://doi.org/
10.1007/978-3-540-30080-9_2. doi:10.1007/978-3-540-30080-9\_2.
[13] M. V. Andreeva, I. B. Virbitskaite, Observational equivalences for timed stable event
structures, Fundam. Informaticae 72 (2006) 1–19. URL: http://content.iospress.com/articles/
fundamenta-informaticae/fi72-1-3-02.
[14] E. N. Bozhenkova, I. B. Virbitskaite, Testing equivalences of time Petri nets, Program.
Comput. Softw. 46 (2020) 251–260. URL: https://doi.org/10.1134/S0361768820040040. doi:10.
1134/S0361768820040040.
[15] T. Aura, J. Lilius, A causal semantics for time Petri nets, Theor. Comput. Sci. 243 (2000) 409–
447. URL: https://doi.org/10.1016/S0304-3975(99)00114-0. doi:10.1016/S0304-3975(99)
00114-0.
[16] I. B. Virbitskaite, D. Bushin, E. Best, True concurrent equivalences in time Petri nets,
Fundam. Informaticae 149 (2016) 401–418. URL: https://doi.org/10.3233/FI-2016-1454.
doi:10.3233/FI-2016-1454.
[17] P. Darondeau, P. Degano, Refinement of actions in event structures and causal trees,
Theor. Comput. Sci. 118 (1993) 21–48. URL: https://doi.org/10.1016/0304-3975(93)90361-V.
doi:10.1016/0304-3975(93)90361-V.
[18] P. Reynier, A. Sangnier, Weak time Petri nets strike back!, in: M. Bravetti, G. Zavattaro
(Eds.), CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009,
Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer
Science, Springer, 2009, pp. 557–571. URL: https://doi.org/10.1007/978-3-642-04081-8_37.
doi:10.1007/978-3-642-04081-8\_37.