Testing Equivalences of Time Petri Nets

Abstract

In the paper, we study a family of testing equivalences in interleaving, partial-order semantics, and combined semantics in the context of safe time Petri nets (elementary net systems whose transitions are labeled with time firing intervals, can fire only if their lower time bounds are attained, and are forced to fire when their upper time bounds are reached). For this purpose, the following three representations of behavior of safe time Petri nets are developed: sequences of firings of net transitions, which represent interleaving semantics; time causal processes, from which partial orders are derived; and time causal tree, whose nodes are sequences of transition firings and arcs are labeled by information about partial orders. We establish relationships between these equivalences and show that semantics of time causal processes and time causal trees coincide.

1 INTRODUCTION

Testing equivalences are used for comparing behavior of systems and checking whether the specification and the implementation obtained correspond to one another, as well as for establishing satisfiability of logical formulas. The concept of testing equivalence was put forward by Hennessy and de Nicola in [1]. A test is a special process that is executed in parallel with the process being tested. Such an execution is considered to be successful if the test reaches a designated successful state, and the process passes the test if every computation is successful. Two processes are said to be test equivalent if they pass the same sets of tests. To facilitate the study and the use of testing equivalencies, alternative characterizations for them have been found. For instance, comparison is performed based on all tests, which are computations of processes and sets of their possible continuations. The notion of testing equivalence is intuitively appealing and has led to a well-developed mathematical theory of equivalences and preorders on the processes.

Originally, testing equivalences were thoroughly investigated in the context of models of transition systems (see, for instance, [2, 3]), which are based on the interleaving semantics, where the concurrency relation between system actions is represented as nondeterministic choice between executions of linearly ordered atomic actions rather than directly. Interleaving testing equivalences for elementary net systems were studied in [4]. To overcome limitations of the interleaving approach, the concurrency relation is modeled often as a lack of causality dependence between system actions, which is presented, as a rule, by a partial order. In [5, 6]), testing equivalences were considered in partial order semantics in the framework of event structure models. Moreover, testing equivalences were actively studied in the context of event structures models for the causal tree semantics (the behavior of the system is represented as a tree in which the arcs are labeled by actions and information about their predecessors; i.e., information about causal dependence is preserved). Relationships between partial order and causal tree semantics for event structure models have been thoroughly studied in [6–8]. Partial order semantics of Petri nets is most often represented by means of the so-called causal net processes, which include events and conditions related by causal dependence and concurrency (see [9–11] and references therein). Comparison of various testing equivalences in partial order semantics of Petri nets was carried out in [4]. To the best authors’ knowledge, causal tree semantics in the framework of Petri nets has not been studied yet.

In verification of complex safety-critical systems, it is important to study not only qualitative characteristics of system behavior but also quantitative ones. For these purposes, testing equivalences were applied in the framework of a number of real-time models. For discrete-time transition systems, alternative characterizations of time testing equivalences were obtained in [12, 13] with the use of an extended concept of the so-called admissible sets. In [14, 15], semantic theory based on testing equivalences has been suggested for algebras of processes with time constraints, and alternative characterizations of testing pre-orders have been formulated in terms of the so-called refusal traces. The authors of paper [15] have proved the possibility of discretization in the context of time process algebra developed by them and, as a result, reduced dense-time testing relations to discrete-time ones. In [16], interleaving testing relations, as well as results related to their alternative characterization and possibility of discretization are extended to the Petri net model with time characteristics associated with tokens, and time intervals associated with arcs from places to transitions. In [17], testing relations are studied for time and causal semantics of event structure models. In addition, in [18–20], classification of equivalences from the spectrum of linear/branching time for interleaving, causal tree, and partial order semantics is given in the framework of dense-time event structure models. Partial order semantics was put forward for timed Petri nets, where each transition is associated with its firing duration [21, 22], and for safe time Petri nets, where each transition is made to correspond to a firing delay interval [23]. However, as far as we know, no studies of testing equivalences in semantics of causal net processes and causal trees have been reported in the literature. It is only works [24, 25] where relationships between the trace and bisimulation equivalences in the interleaving and partial order semantics of safe time Petri nets were studied.

The goal of this work is to define, study, and compare testing equivalences in the interleaving, causal net, and causal tree semantics in the context of safe time Petri nets (elementary net systems whose transitions are labeled with time firing intervals, can fire only if their lower time bounds are attained, and are forced to fire when their upper time bounds are reached). We establish relationships between the equivalences under consideration and show that they coincide in the semantics of time causal processes and that of time causal trees.

2 TIME PETRI NETS: SYNTAX AND INTERLEAVING SEMANTICS

In this section, we define basic terminology concerning the model of Petri nets with timing constraints and its interleaving semantics. First, we recall definitions of Petri net structure and behavior. Let Act be a set of actions.

Definition 1. A (labeled over$Act$) Petri net (PN) is a tuple $\mathcal{N} = (P,T,F,{{M}_{0}},L)$, where P is a finite set of places, T is a finite set of transitions ($P \cap T = \emptyset$ and $P \cup T \ne \emptyset$), $F \subseteq (P \times T) \cup (T \times P)$ is a flow relation, $\emptyset \ne {{M}_{0}} \subseteq P$ is an initial marking, and L : $T \to Act$ is a labeling function. For an element $x \in P \cup T$, let $^{ \bullet }x = \{ y\,|\,(y,x) \in F\}$ and ${{x}^{ \bullet }} = \{ y\,|\,(x,y) \in F\}$ be sets of input and output elements. For a subset $X \subseteq P \cup T$, these sets of elements are extended to the sets $^{ \bullet }X = \bigcup\nolimits_{x \in X} {{\,}^{ \bullet }}x$ and ${{X}^{ \bullet }} = \bigcup\nolimits_{x \in X} \,{{x}^{ \bullet }}$, respectively.

A marking M of a Petri net $\mathcal{N}$ is an arbitrary subset of P. A transition $t \in T$is enabled at a marking M if $^{ \bullet }t \subseteq M$¹. Let $En(M)$ denote the set of transitions enabled at M. If transition t is enabled at a M, then its firing results in a new marking $M'$ (denoted as $M\mathop \to \limits^t M'$) when $M{\kern 1pt} ' = (M{{{\backslash }}^{ \bullet }}t) \cup {{t}^{ \bullet }}$. We will use the notation $M\mathop \to \limits^\vartheta M'$ if $\vartheta = {{t}_{1}} \ldots {{t}_{k}}$ and $M = {{M}^{0}}\mathop \to \limits^{{{t}_{1}}} {{M}^{1}}$ … M^{k – 1}$\mathop \to \limits^{{{t}_{k}}}$ M^k = M ' ($k \geqslant 0$). In this case, ϑ is a firing sequence from M (to $M'$) and $M'$ is a marking in the Petri net $\mathcal{N}$reachable from the marking M. Let $RM(\mathcal{N})$ be a set of all markings in the Petri net $\mathcal{N}$ that are reachable from M₀.

A Petri net $\mathcal{N}$ is called T-restricted if $^{ \bullet }t \ne \emptyset \ne {{t}^{ \bullet }}$ for all transitions $t \in T$; it is called contact-free if, for an arbitrary marking $M \in RM(\mathcal{N})$ and any transition t that is enabled at the marking M, condition $M \cap {{t}^{ \bullet }}$ = ∅ holds.

A time Petri net [23] is a Petri net in which each transition is associated with a time interval that shows possible moments of firing for an enabled transition (transition that has a sufficient number of tokens at its input places); the enabled transition can fire if and only if its lower boundary is reached while the upper boundary is not exceeded; if the transition is not fired, it must fire when the upper boundary is reached.

The domain $\mathbb{T}$ of time values is a set of nonnegative rational numbers. We assume that $[{{\tau }_{1}},{{\tau }_{2}}]$ is a closed interval between two time instants ${{\tau }_{1}},{{\tau }_{2}} \in \mathbb{T}$. The upper boundary may be equal to infinity. Let $Interv$ be a set of all such intervals.

Definition 2. A (labeled over$Act$) time Petri net is a pair $\mathcal{T}\mathcal{N} = (\mathcal{N},D)$, where $\mathcal{N}$ is the underlying (labeled over Act) Petri net and $D:T \to Interv$ is a static timing function that assigns a time interval to each transition. The boundaries of the time interval $D(t) \in Interv$ are called the earliest firing time (Eft) and the latest firing time (Lft) of the transition $t \in T$.

The state of a time Petri net$\mathcal{T}\mathcal{N}$ is a pair $S = (M,I)$, where M is a marking of the Petri net $\mathcal{N}$ and $I:En(M) \to \mathbb{T}$ is a dynamic timing function. The initial state of the time Petri net $\mathcal{T}\mathcal{N}$ is a pair ${{S}_{0}} = ({{M}_{0}},{{I}_{0}})$, where M₀ is an initial marking of the Petri net $\mathcal{N}$ and ${{I}_{0}}(t) = 0$ for all $t \in En({{M}_{0}})$. A transition t enabled at a marking M in the Petri net $\mathcal{N}$is fireable from a state$S = (M,I)$after a delay time$\theta \in \mathbb{T}$ if ($Eft(t) \leqslant I(t)$ + θ) and ($I(t') + \theta \leqslant Lft(t')$ for all t' ∈ $En(M)$). If transition t is fireable from a state S = $(M,I)$ after a delay time $\theta$, then its firing results in a new state $S' = (M',I')$ (denoted as $S\mathop \to \limits^{(t,\theta )} S'$) such that $M\mathop \to \limits^t M'$ and, $\forall t' \in T\diamondsuit$,

$$I'(t') = \left\{ {\begin{array}{*{20}{l}} {I(t') + \theta ,\quad {\text{if}}\;t' \in En(M{{{\backslash }}^{ \bullet }}t),} \\ {0,\quad {\text{if}}\;t' \in En(M'){\backslash }En(M{{{\backslash }}^{ \bullet }}t),} \\ {{\text{not}}\;{\text{defined}}\;{\text{otherwise}}.} \end{array}} \right.$$

We write $S\mathop \to \limits^\sigma S'$ if $\sigma = ({{t}_{1}},{{\theta }_{1}}) \ldots ({{t}_{k}},{{\theta }_{k}})$ and S = ${{S}^{0}}\xrightarrow{{({{t}_{1}},{{\theta }_{1}})}}$S¹ … ${{S}^{{k - 1}}}\xrightarrow{{({{t}_{k}},{{\theta }_{k}})}}{{S}^{k}} = S'$ ($k \geqslant 0$). Then, σ is a firing sequence of the time Petri net $\mathcal{T}\mathcal{N}$ from S (to$S'$) and $S'$ is a reachable state of the time Petri net$\mathcal{T}\mathcal{N}$from S. Let $\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ be a set of all firing sequences from ${{S}_{0}}$ and $RS(\mathcal{T}\mathcal{N})$ be a set of all states in the time Petri net $\mathcal{T}\mathcal{N}$reachable from ${{S}_{0}}$. For σ = $({{t}_{1}},{{\theta }_{1}})$ ... $({{t}_{k}},{{\theta }_{k}}) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$, L(σ) = (a₁, θ₁) ... $({{a}_{k}},{{\theta }_{k}})$ if ${{a}_{i}} = L({{t}_{i}})$ for all $1 \leqslant i \leqslant k$. Let us define the interleaving language of the time Petri net$\mathcal{T}\mathcal{N}$ as follows: $\mathcal{L}(\mathcal{T}\mathcal{N})$ = {L(σ) ∈ (Act × $\mathbb{T}){\text{*}}\,|\,\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})\}$.

A time Petri net $\mathcal{T}\mathcal{N}$ is said to be T-restricted if the base Petri net is T-restricted; contact-free if, for any state $S = (M,I) \in RS(\mathcal{T}\mathcal{N})$ and any transition t fireable from the state S after some delay time $\theta$, $(M{{{\backslash }}^{ \bullet }}t) \cap {{t}^{ \bullet }} = \emptyset$²; and time-progressive if, for any sequence of transitions $\{ {{t}_{1}},{{t}_{2}}, \ldots ,{{t}_{n}}\} \subseteq T$ such that $t_{i}^{ \bullet }{{ \cap }^{ \bullet }}{{t}_{{i + 1}}} \ne \emptyset$ ($1 \leqslant i < n$) and $t_{n}^{ \bullet }{{ \cap }^{ \bullet }}{{t}_{1}} \ne \emptyset$, the inequality $\sum\nolimits_{1 \leqslant i \leqslant n} \,Eft({{t}_{i}}) > 0$³ holds. In what follows, we consider only T-restricted, contact-free, and time-progressive time Petri nets.

Example 1. An example of a labeled over Act =$\{ a,b,c,d\}$ time Petri net $\mathcal{T}\mathcal{N}$ is shown in Fig. 1, where the places are represented by circles and transitions by barriers; the names are depicted near the elements. The elements included in the flow relation are connected by arrows, and each place contained in the initial marking is that with a token (bold point). The values of the labeling and static timing functions are printed next to the transitions. It is not difficult to check that t₁ and t₃ are transitions enabled at the initial marking ${{M}_{0}} = {\text{\{ }}{{p}_{1}},{{p}_{2}}{\text{\} }}$; moreover, they can fire at the initial state S₀ = $({{M}_{0}},{{I}_{0}})$, where I₀(t) = $\left\{ {\begin{array}{*{20}{l}} {0,\quad {\text{if}}\;t \in \{ {{t}_{1}},{{t}_{3}}\} ,} \\ {{\text{not}}\;{\text{defined}}\;{\text{otherwise}},} \end{array}} \right.$ after a time delay $\theta \in [2,3]$. Note that $\sigma = ({{t}_{1}},3)$$({{t}_{3}},0)$$({{t}_{2}},2)$$({{t}_{3}},2)$$({{t}_{1}},0)$$({{t}_{5}},2)$$({{t}_{4}},0)$ is a firing sequence from S₀ in the time Petri net $\mathcal{T}\mathcal{N}$. Furthermore, $\mathcal{T}\mathcal{N}$ is T‑restricted, contact-free, and time-progressive. □

Fig. 1.

An example of a time Petri net.

3 CAUSALITY-BASED SEMANTICS OF TIME PETRI NETS

3.1 Basic Definitions

We begin with definitions related to time nets.

Definition 3. A (labeled over Act) time net is a finite acyclic net $TN = (B,E,G,l,\tau )$, where B is a set of conditions, E is a set of events, $G \subseteq (B \times E) \cup (E \times B)$ is a flow relation such that $\{ e\,|\,(e,b) \in G\}$ =  $\{ e\,|\,(b,e) \in G\}$ = E, $l:E \to Act$ is a labeling function, and $\tau :E \to \mathbb{T}$ is a time function such that $e{{G}^{ + }}e' \Rightarrow \tau (e) \leqslant \tau (e')$.

Let us introduce additional notation for the time net $TN = (B,E,G,l,\tau )$. Let $\prec = {{G}^{ + }}$, $\preccurlyeq = G{\text{*}}$ and τ(TN) = $\max \{ \tau (e)\,|\,e \in E\}$. Let us also introduce sets $^{ \bullet }x\, = \,\{ y\,|\,(y,x)\, \in \,G\}$ and ${{x}^{ \bullet }}\, = \,\{ y\,|\,(x,y)\, \in \,G\}$ for $x \in B$ ∪ E; $^{ \bullet }X = \bigcup\nolimits_{x \in X} {{\,}^{ \bullet }}x$ and ${{X}^{ \bullet }} = \bigcup\nolimits_{x \in X} \,{{x}^{ \bullet }}$ for $X \subseteq B \cup E$; $^{ \bullet }TN = \{ b \in B\,|{{\,}^{ \bullet }}b = \emptyset \}$; and $T{{N}^{ \bullet }}$ = $\{ b\, \in$B | ${{b}^{ \bullet }}$ = ∅}.

$TN = (B,E,G,l,\tau )$ is referred to as a (labeled over Act) time causal net if ${{{\text{|}}}^{ \bullet }}b{\text{|}} \leqslant 1$ and ${\text{|}}{{b}^{ \bullet }}{\text{|}} \leqslant 1$ for all conditions $b \in B$. Note that η(TN) = $({{E}_{{TN}}},{{ \preccurlyeq }_{{TN}}} \cap ({{E}_{{TN}}} \times {{E}_{{TN}}}),{{l}_{{TN}}},{{\tau }_{{TN}}})$ is a (labeled over Act) time partially ordered set (poset).⁴

Let us introduce notation and definitions for the time causal net $TN = (B$, $E$, $G$, l, $\tau )$:

• $\downarrow e = \{ x\,|\,x \preccurlyeq e\}$ is a set of predecessors of an event$e \in E$, $Earlier(e) = \{ e' \in E\,|\,\tau (e') < \tau (e)\}$ is a set of time predecessors of an event$e \in E$;

• $E{\kern 1pt} ' \subseteq E$ is a downward-closed subset of E if $\downarrow e' \cap E \subseteq E'$ for every $e' \in E'$. For such a subset, we use notation $Cut(E') = (E{{'}^{ \bullet }} \cup TN){{{\backslash }}^{ \bullet }}E'$. $E' \subseteq E$ is called a timely sound subset of $E$ if $\tau (e') \leqslant \tau (e)$ for all $e' \in E'$ and $e \in E{\backslash }E'$;

• A sequence $\rho = {{e}_{1}} \ldots {{e}_{k}}$ ($k \geqslant 0$) of events from $E$ is a linearization of a time causal net$TN$ if every event from $E$ appears only once in the sequence and the following condition holds: $({{e}_{i}} \prec {{e}_{j}} \vee \tau ({{e}_{i}}) < \tau ({{e}_{j}})) \Rightarrow$i < j for all 1 ≤ i, $j \leqslant k$. Let us introduce the set $E_{\rho }^{l}$ = $\bigcup\nolimits_{1 \leqslant i \leqslant l} {{e}_{i}}$ ($0 \leqslant l \leqslant k$). Clearly, $E_{\rho }^{l}$ is a downward-closed and timely sound subset of E, and, moreover, $\tau ({{e}_{k}}) = \tau (TN)$.

From the definitions of the time causal net and its linearization, we obtain the following assertion.

Lemma 1. Any time causal net has a linearization.

Time causal nets $TN = (B,E,G,l,\tau )$ and $TN' = (B'$, E', G', l', τ') are isomorphic (denoted as $TN \simeq TN'$) if there exists a bijective mapping $\beta {\kern 1pt} :\;B \cup E \to B' \cup E'$ such that (a) $\beta (B) = B'$ and $\beta (E) = E'$; (b) $xGy \Leftrightarrow \beta (x)G'\beta (y)$ for all $x,y \in B \cup E$; (c) $l(e) = l'(\beta (e))$ and $\tau (e) = \tau '(\beta (e))$ for all $e \in E$. We say that TN is a prefix of $TN'$ (denoted as $TN \to TN'$) if $B \subseteq B'$, $E$ is a downward-closed and timely sound subset of $E'$, $E{{'\backslash }}E = \{ e\}$, $G = G' \cap (B \times E \cup E \times B)$, $l = l'{{{\text{|}}}_{E}}$, and $\tau = \tau '{{{\text{|}}}_{E}}$.

Example 2.Figure 2 shows a time causal net $TN = (B,E,G,l,\tau )$. Here, conditions are depicted by circles, and events, by barriers; names of elements are placed next to the elements; elements included in the flow relation are connected by arrows; the values of functions l and $\tau$ are shown next to the events. Let the time causal nets be $TN' = (B',E',G',l',\tau ')$, where B' = $\{ {{b}_{1}},{{b}_{2}},{{b}_{3}},{{b}_{4}}\}$, $E' = \{ {{e}_{1}},{{e}_{3}}\}$, $G' = G \cap (B' \times E' \cup E' \times B')$, $l' = l{{{\text{|}}}_{{E'}}}$, $\tau ' = \tau {{{\text{|}}}_{{E'}}}$, and $TN'' = (B'',E'',G'',l'',\tau '')$, where $B'' = \{ {{b}_{1}},{{b}_{2}},{{b}_{3}}\}$, $E'' = \{ {{e}_{1}}\}$, G'' = $G \cap (B'' \times E'' \cup E''$ × × B''), $l'' = l{{{\text{|}}}_{{E''}}}$, $\tau '' = \tau {{{\text{|}}}_{{E''}}}$. It is easy to verify that $TN''$ is a prefix of $TN'$. □

3.2 Time Causal Processes of Time Petri Nets

In this subsection, we discuss the concept of causality-based net processes of time Petri nets, which was proposed in [23].

Definition 4. Let $\mathcal{T}\mathcal{N} = ((P,T,F,{{M}_{0}},L),D)$ be a time Petri net and $TN = (B,E,G,l,\tau )$ be a time causal net. A mapping $\varphi {\kern 1pt} :\;B \cup E \to P \cup T$ is a homomorphism from$TN$ to $\mathcal{T}\mathcal{N}$ if the following conditions hold:

• $\varphi (B) \subseteq P$, $\varphi (E) \subseteq T$;

• the restriction of φ to $^{ \bullet }e$ is a bijection between $^{ \bullet }e$ and $^{ \bullet }\varphi (e)$ the restriction of φ to ${{e}^{ \bullet }}$ is a bijection between ${{e}^{ \bullet }}$ and $\varphi {{(e)}^{ \bullet }}$ for all $e \in E$;

• the restriction of φ to $^{ \bullet }TN$ is a bijection between $^{ \bullet }TN$ and M₀;

• $l(e) = L(\varphi (e))$ for all $e \in E$.

A pair $\pi = (TN,\varphi )$ is a time causal process of a time Petri net$\mathcal{T}\mathcal{N}$ if TN is a time causal net and φ is a homomorphism from TN to $\mathcal{T}\mathcal{N}$.

Let $\pi = (TN,\varphi )$ be a time causal process of a time Petri net $\mathcal{T}\mathcal{N}$, $B' \subseteq {{B}_{{TN}}}$, and $t \in En(\varphi (B'))$. Then, the time of enabling (TOE) of $t$, i.e., the latest global time moment when tokens appear in all input places is defined as follows: ${\mathbf{TO}}{{{\mathbf{E}}}_{\pi }}(B',t)$ = $\max(\{ {{\tau }_{{TN}}}{{(}^{ \bullet }}b)\,|\,b\, \in \,B_{{[t]}}^{'}{{{\backslash }}^{ \bullet }}TN\}$ ∪ {0}, where $B_{{[t]}}^{'} = \{ b \in B'\,|\,{{\varphi }_{{TN}}}(b) \in {{\;}^{ \bullet }}t\}$.

In order that the values of time functions of time causal processes of time Petri nets correspond to time intervals of firing of net transitions, the concept of correct time causal processes of time Petri nets is introduced.

Definition 5. A time causal process $\pi = (TN,\varphi )$ of a time Petri net $\mathcal{T}\mathcal{N}$ is said to be correct if, for each $e \in E$, the following conditions hold:

• $\tau (e) \geqslant \mathop {{\mathbf{TOE}}}\nolimits_\pi {{(}^{ \bullet }}e,\varphi (e)) + Eft(\varphi (e))$,

• $\forall t \in En(\varphi ({{C}_{e}}))\diamondsuit \tau (e) \leqslant {\mathbf{TO}}{{{\mathbf{E}}}_{\pi }}({{C}_{e}},t) + Lft(t)$, where ${{C}_{e}} = Cut(Earlier(e))$.

Let $\mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ be a set of correct time causal processes of time Petri nets $\mathcal{T}\mathcal{N}$. Let $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}) = \{ TP\,|\,\exists \pi$ = $(TN,\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$:TP ≃⁵$\eta (TN)\}$ denote a set of time posets isomorphic to time posets obtained from correct time causal processes of time Petri nets $\mathcal{T}\mathcal{N}$.

Example 3. Let φ be a mapping from a time causal net TN (Fig. 2) to a time Petri net $\mathcal{T}\mathcal{N}$ (Fig. 1) defined as follows: $\varphi ({{b}_{i}}) = {{p}_{i}}$ ($1 \leqslant i \leqslant 6$), $\varphi ({{b}_{i}}) = {{p}_{{i - 6}}}$ ($7 \leqslant i \leqslant 10$), and $\varphi ({{e}_{i}}) = {{t}_{i}}$ ($1 \leqslant i \leqslant 5$), $\varphi ({{e}_{6}}) = {{t}_{1}}$, $\varphi ({{e}_{7}}) = {{t}_{3}}$. For the time causal net $TN'$ defined in Example 2, we set $\varphi ' = \varphi \,|{{\,}_{{E' \cup B'}}}$. It is easy to see that $\pi = (TN,\varphi )$ and $\pi ' = (TN',\varphi ')$ are time causal processes of the time Petri nets $\mathcal{T}\mathcal{N}$.

For the set $\widetilde B = \{ {{b}_{3}},{{b}_{4}}\} \subset B$ and transition ${{t}_{2}}$ ∈ $En(\varphi (\widetilde B))$, we calculate ${\mathbf{TO}}{{{\mathbf{E}}}_{\pi }}(\widetilde B,{{t}_{2}})$ = $\max(\{ {{\tau }_{{TN}}}{{(}^{ \bullet }}b)$ | b ∈ ${{\tilde {B}}_{{[{{t}_{2}}]}}}{{{\backslash }}^{ \bullet }}TN\} \cup \{ 0\} )$ = $\max (\{ \tau ({{e}_{1}})\, = \,3$, τ(e₃) = 3} ∪ {0}) = 3. It is easy to check that the time causal processes $\pi = (TN,\varphi )$ and $\pi ' = (TN',\varphi ')$ are correct. □

We say that $\pi = (TN,\varphi )$ and $\pi ' = (TN',\varphi ')$ from $\mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ are isomorphic (denoted as $\pi \simeq \pi '$) if there exists an isomorphism $f{\kern 1pt} :\;TN \simeq TN'$ such that φ(x) = $\varphi '(f(x))$ for all $x \in B \cup E$; we also write $\pi \to \pi '$ in $\mathcal{T}\mathcal{N}$ if $TN \to TN'$ and $\varphi = \varphi '{{{\text{|}}}_{{B \cup E}}}$.

Let us consider relationship between the firing sequences and correct time causal processes of time Petri nets. For $\pi = (TN,\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$, we define function FS_π that maps linearization $\rho = {{e}_{1}} \ldots {{e}_{k}}$ of TN into a sequence of the form $F{{S}_{\pi }}(\rho ) = (\varphi ({{e}_{1}}),\tau ({{e}_{1}}) - 0)$ ... $(\varphi ({{e}_{k}}),\tau ({{e}_{k}}) - \tau ({{e}_{{k - 1}}}))$.

Proposition 1. Let $\mathcal{T}\mathcal{N}$ be a time Petri net. Then,

(a) if $\pi = (TN,\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ and ρ is a linearization of TN, there exists a unique firing sequence $F{{S}_{\pi }}(\rho ) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$;

(b) if $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$, there exists a unique (up to isomorphism) time causal process π_σ = (TN, $\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ and a unique linearization ${{\rho }_{\sigma }}$ of TN such that $F{{S}_{{{{\pi }_{\sigma }}}}}({{\rho }_{\sigma }}) = \sigma$.

Proof. Item (a) without the assumption of uniqueness of the firing sequence $F{{S}_{\pi }}(\rho )$ and item (b) without the assumption of uniqueness of the linearization ${{\rho }_{\sigma }}$ were proved in [23, Theorems 19, 21, and 22].

(a) The uniqueness of the firing sequence $F{{S}_{\pi }}(\rho )$ follows from the definitions of the homomorphism of φ and function $F{{S}_{\pi }}$.

(b) Let ${{\rho }_{\sigma }} = {{e}_{1}} \ldots {{e}_{n}}$ ($n \geqslant 0$) be a linearization of TN such that $F{{S}_{{{{\pi }_{\sigma }}}}}({{\rho }_{\sigma }}) = \sigma = ({{t}_{1}},{{\theta }_{1}}) \ldots ({{t}_{n}},{{\theta }_{n}}) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$. Let us assume the contrary, i.e., that there exists a linearization $\bar {\rho } = {{\bar {e}}_{1}} \ldots {{\bar {e}}_{n}}$ of $TN$ such that $F{{S}_{{{{\pi }_{\sigma }}}}}(\bar {\rho }) = \sigma$ and $\bar {\rho } \ne {{\rho }_{\sigma }}$. Since all linearizations of $TN$ are finite, there exists the least $k$ such that ${{e}_{k}} \ne {{\bar {e}}_{k}}$. It is clear that $\varphi ({{e}_{k}}) = \varphi ({{\bar {e}}_{k}}) = {{t}_{k}}$. Since $\mathcal{T}\mathcal{N}$ is a T-restricted time Petri net, $^{ \bullet }{{t}_{k}} \ne \emptyset$. Let us take an arbitrary place ${{p}_{k}} \in {{\;}^{ \bullet }}{\kern 1pt} {{t}_{k}}$. By the definition of homomorphism, there exist $b \in {{\;}^{ \bullet }}{{e}_{k}}$ and $\bar {b} \in {{\;}^{ \bullet }}{{\bar {e}}_{k}}$ such that $\varphi (b) = \varphi (\bar {b}) = {{p}_{k}}$. By virtue of the definition of time causal net, we have $b \ne \bar {b}$.

Consider two possible cases.

– $\{ b,\bar {b}\} \subseteq {{\;}^{ \bullet }}TN$. Then, ${{p}_{k}} \in {{M}_{0}}$. This contradicts the definition of homomorphism of φ.

– $b \in {{\;}^{ \bullet }}TN$ and $\bar {b}\not \in {{}^{ \bullet }}TN$ (the case where $\bar {b} \in {{\;}^{ \bullet }}TN$ and $b\not \in {{}^{ \bullet }}TN$ is analyzed similarly). Since $b \in {{\;}^{ \bullet }}TN$, we find that ${{p}_{k}} \in {{M}_{0}}$, of the definition of homomorphism of φ. Then, it follows that $b = {{b}_{{0,{{p}_{k}}}}}$ by construction of π_σ in [23]. Assuming that $\bar {b}\not \in {{}^{ \bullet }}TN$, we find an event $\tilde {e}$ such that $\{ \tilde {e}\} = {{\;}^{ \bullet }}\bar {b}$. Since k is minimal, the number of the event $\tilde {e}$ in both linearizations ρ and $\bar {\rho }$ is the same, i.e. $\tilde {e} = {{e}_{i}} = {{\bar {e}}_{i}}$ for some $0 < i < k$. From the definition of the function $F{{S}_{{{{\pi }_{\sigma }}}}}$, it follows that $\varphi (\tilde {e})$ = t_i. Then, ${{p}_{k}} \in t_{i}^{ \bullet }$ in accordance with the definition of φ. Moreover, $\bar {b} = {{b}_{{i,{{p}_{k}}}}}$ by construction of ${{\pi }_{\sigma }}$ in [23]. Thus, we arrived at the contradiction to property (41) from [23]: there does not exist a ${{b}_{{i,{{p}_{k}}}}}$ for any $0 < i < k$.

– $b,\bar {b}\not \in {{}^{ \bullet }}TN$. Hence, there is an event $\tilde {e}$ ($\hat {e}$) such that $\{ \tilde {e}\} = {{\;}^{ \bullet }}b$ ($\{ \hat {e}\} {{ = }^{ \bullet }}\bar {b}$). From the definition of the homomorphism φ, it follows that $\tilde {e} \ne \hat {e}$. Since k is minimal, the event $\tilde {e}$ ($\hat {e}$) has the same number in the linearizations ρ and $\bar {\rho }$, i.e., $\tilde {e} = {{e}_{i}} = {{\bar {e}}_{i}}$ for some $1 \leqslant i$ < k ($\hat {e} = {{e}_{j}} = {{\bar {e}}_{j}}$ for some $1 \leqslant j < k$). Then, by the definition of the linearization, $i \ne j$. From the definition of the function $F{{S}_{{{{\pi }_{\sigma }}}}}$, it follows that $\varphi (\tilde {e}) = {{t}_{i}}$ ($\varphi (\hat {e})$ = t_j).From the definition of the homomorphism, it follows that ${{p}_{k}} \in t_{i}^{ \bullet }$ (${{p}_{k}} \in t_{j}^{ \bullet }$). It follows from the construction of ${{\pi }_{\sigma }}$ in [23] that $b = {{b}_{{i,{{p}_{k}}}}}$ ($\bar {b} = {{b}_{{j,{{p}_{k}}}}}$). If $i < j$ < k ($j < i < k$), we arrive at the contradiction with property (41) from [23]: ${{b}_{{l,{{p}_{k}}}}}$ does not exists for any $i < l$ < k ($j < l < k$). □

Example 4. For a time causal process $\pi = (TN,\varphi )$ of a time Petri net $\mathcal{T}\mathcal{N}$ (see Example 3) and a linearization $\rho = {{e}_{1}}{{e}_{3}}{{e}_{2}}{{e}_{7}}{{e}_{6}}{{e}_{5}}{{e}_{4}}$ of a time causal net TN, FS_π(ρ) = $({{t}_{1}},3)$$({{t}_{3}},0)$$({{t}_{2}},2)$$({{t}_{3}},2)$$({{t}_{1}},0)$$({{t}_{5}},2)$$({{t}_{4}},0)$ is a firing sequence of the time Petri net $\mathcal{T}\mathcal{N}$ (see Example 1). □

By using the definition of the prefix of a time causal net and Proposition 1, it is easy to show that, if the firing sequence and the time causal process of a time Petri net are interrelated, then their direct extensions are also interrelated.

Lemma 2. Let $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ and $\pi \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ be such that $\sigma = F{{S}_{\pi }}(\rho )$, where ρ is a linearization of $T{{N}_{\pi }}$. Then,

(a) if $\sigma (t,\theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$, then there exists $\tilde {\pi }$$\in$$\mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ such that $\pi \to \tilde {\pi }$ in $\mathcal{T}\mathcal{N}$ and $\sigma (t,\theta ) = F{{S}_{{\tilde {\pi }}}}(\rho e)$, where $\rho e$ is a linearization of $T{{N}_{{\tilde {\pi }}}}$;

(b) if $\pi \to \tilde {\pi }$ in $\mathcal{T}\mathcal{N}$, then there exists $\sigma (t,\theta )$$\in$$\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ such that $\sigma (t,\theta ) = F{{S}_{{\tilde {\pi }}}}(\rho e)$, where ρe is a linearization of $T{{N}_{{\tilde {\pi }}}}$.

3.3 Time Causal Trees of Time Petri Nets

Causal trees [8] are synchronization trees that carry in their labels not only names of actions but also additional information about causes of these actions thus providing us with an interleaving representation of concurrent processes supplemented with the description of causality relations between their actions. By adding timing into labels of causal trees, we get time causal trees. In a time causal tree of a time Petri net $\mathcal{T}\mathcal{N}$, nodes are firing sequences from the set $\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ and arcs connect two nodes if one sequence is a direct extension of another. Information about predecessors for arc labels is obtained from the causality relation of the corresponding time processes of $\mathcal{T}\mathcal{N}$.

Definition 6.The time causal tree of a time Petri net$\mathcal{T}\mathcal{N}$, $TCT(\mathcal{T}\mathcal{N})$, is the tree $(\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}),A,\phi )$, where $\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ is a set of nodes with the root ε; A = $\{ (\sigma ,\sigma (t,\theta ))\,{\text{|}}\,\sigma ,\sigma (t,\theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})\}$ is a set of arcs; ϕ is a labeling function such that $\phi (\epsilon ) = \epsilon$ and ϕ(σ, $\sigma (t,\theta )) = ({{l}_{{\mathcal{T}\mathcal{N}}}}(t)$, θ, K), where K = {n – l + 1 | σ(t, θ) = $F{{S}_{{{{\pi }_{{\sigma (t,\theta )}}}}}}({{e}_{1}} \ldots {{e}_{n}}e)$, ${{e}_{1}} \ldots {{e}_{n}}e$ is a linearization of $T{{N}_{{{{\pi }_{{\sigma (t,\theta )}}}}}}$, and ${{e}_{l}}{{ \prec }_{{T{{N}_{{{{\pi }_{{\sigma (t,\theta )}}}}}}}}}e\}$. Let $path(\sigma )$ be a path in $TCT(\mathcal{T}\mathcal{N})$ from the root to a node $\sigma$⁶. By $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$ = $\{ \phi (path(\sigma ))$ ∈ $(Act \times \mathbb{T} \times {{2}^{\mathbb{N}}}){\text{*}}\,{\text{|}}\,\sigma$ ∈ $\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})\}$, we denote the set of sequences of path labels in a time causal tree of a time Petri net $\mathcal{T}\mathcal{N}$.

Example 5. Consider a time Petri net $\mathcal{T}\mathcal{N}$ (Fig. 1) and a firing sequence $\sigma = ({{t}_{1}},3)$$({{t}_{3}},0)$$({{t}_{2}},2)$$({{t}_{3}},2)$$({{t}_{1}},0)$$({{t}_{5}},2)$$({{t}_{4}},0) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$. It follows that the sequence of labels of the path from the root to the node σ has the following form: $\phi (path(\sigma )) = (a,3,\emptyset )$$(b,0,\emptyset )$$(a,2$, {1, 2}) $(b,2,\{ 1,2,3\} )$$(a,0,\{ 2,3,4\} )$$(d,2,\{ 2,3,4,5\} )$$(c,0,\{ 2$, 4, 5, 6}). □

Let us establish relationship between correct time causal processes and labeled paths in time causal trees of the two time Petri nets.

Proposition 2. Let $\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$, be time Petri nets, and let $TCT(\mathcal{T}\mathcal{N}) = (\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}),A,\phi )$ and TCT$(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ = $(\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}{\kern 1pt} '$, A', ϕ') be their time causal trees. Then,

(a) if $\pi \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ and $\pi ' \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ are time processes and $f{\kern 1pt} :\;\eta (T{{N}_{\pi }}) \to \eta (T{{N}_{{\pi '}}})$ is an isomorphism, then $\phi (path(F{{S}_{\pi }}(\rho ))) = \phi '(path(F{{S}_{{\pi '}}}(f(\rho ))))$ for any linearization $\rho$$T{{N}_{\pi }}$;

(b) if $\phi (path(\sigma )) = \phi '(path(\sigma '))$ for $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ and $\sigma ' \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$, then there exists an isomorphism $f{\kern 1pt} :\;\eta (T{{N}_{{{{\pi }_{\sigma }}}}}) \to \eta (T{{N}_{{{{\pi }_{{\sigma '}}}}}})$ such that $f({{\rho }_{\sigma }}) = {{\rho }_{{\sigma '}}}$.

Proof. (a) follows from Proposition 1(a) and properties of isomorphism f.

(b) follows from Proposition 1(b), Definition 6, and properties of homorphism φ and function FS. □

Let us prove a useful auxiliary assertion.

Proposition 3. Let $\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}{\kern 1pt} '$ be time Petri nets. Then, $\mathcal{L}(\mathcal{T}\mathcal{N}) = \mathcal{L}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ ⇐ $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$ = $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}{\kern 1pt} '))$$\Leftrightarrow$$\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}) = \mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}{\kern 1pt} ')$.

Proof. The fact that $\mathcal{L}(\mathcal{T}\mathcal{N})$ = $\mathcal{L}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ ⇐ $\mathcal{L}(TCT(\mathcal{T}\mathcal{N})) = \mathcal{L}(TCT(\mathcal{T}\mathcal{N}'))$, follows directly from the definitions.Fig. 2

Fig. 2.

An example of a time causal net.

Now, we check that $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$ = $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$ ⇒ $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}) = \mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N})$. Let us consider an arbitrary time poset $TP \in \mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N})$. This means that it is possible to find a time causal process of the net π = $(TN,\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ such that $\eta (TN) \simeq TP$. Consider an arbitrary linearization $\rho$ of $TN$. According to Lemma 1, at least one linearization of TN exists. From Proposition 1(a), it follows that there exists a firing sequence $\sigma = F{{S}_{\pi }}(\rho ) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$. In accordance with Proposition 1(b), without loss of generality, we can assume that $\pi = {{\pi }_{\sigma }}$ and $\rho = {{\rho }_{\sigma }}$. By definition, there exists a path u in $TCT(\mathcal{T}\mathcal{N})$ from the root to the node σ. Moreover, $\phi (u) \in \mathcal{L}(TCT(\mathcal{T}\mathcal{N})) = \mathcal{L}(TCT(\mathcal{T}\mathcal{N}{\kern 1pt} '))$. This implies that, in $TCT(\mathcal{T}\mathcal{N}{\kern 1pt} ')$, there exists a path $u'$ from the root to the node $\sigma ' \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ such that $\phi '(u') = \phi (u)$. By virtue of Proposition 1(b), there exists a unique (up to isomorphism) time causal process ${{\pi }_{{\sigma '}}} = (T{{N}_{{\sigma '}}},{{\phi }_{{\sigma '}}}) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ and a unique linearization ${{\rho }_{{\sigma '}}}$ of $T{{N}_{{\sigma '}}}$ such that $F{{S}_{{{{\pi }_{{\sigma '}}}}}}({{\rho }_{{\sigma '}}}) = \sigma '$. From Proposition 2(b), it follows that there is an isomorphism $f{\kern 1pt} :\;\eta (T{{N}_{\sigma }}) \to \eta (T{{N}_{{\sigma '}}})$ such that $f({{\rho }_{\sigma }}) = {{\rho }_{{\sigma '}}}$. Thus, we find that $\eta (T{{N}_{{\sigma '}}}) \simeq TP$, i.e., $TP \in \mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}{\kern 1pt} ')$.

Fig. 3.

Finally, let us check that $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N})$ = $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}{\kern 1pt} ')$ ⇒ $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$ = $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}{\kern 1pt} '))$. Consider an arbitrary $w \in \mathcal{L}(TCT(\mathcal{T}\mathcal{N}))$. This implies that there exists a path u in $TCT(\mathcal{T}\mathcal{N})$ from the root to the node $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ such that $\phi (u) = w$. According to Proposition 1(b), there is a unique (up to isomorphism) time causal process π_σ = $(T{{N}_{\sigma }},{{\varphi }_{\sigma }}) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ and a unique linearization ${{\rho }_{\sigma }}$ of $T{{N}_{\sigma }}$ such that $F{{S}_{{{{\pi }_{\sigma }}}}}({{\rho }_{\sigma }})$ = σ. Hence, $\eta (T{{N}_{\sigma }})$ ∈ $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N})$ = $\mathcal{T}\mathcal{P}os(\mathcal{T}\mathcal{N}{\kern 1pt} ')$. Then, there exists a time causal process net π' = $(TN',\varphi ')$ ∈ $\mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N}')$ such that η(TN_σ) $\simeq$$\eta (TN')$. Hence, there is an isomorphism $f{\kern 1pt} :\;\eta (T{{N}_{\sigma }}) \to \eta (TN')$. Applying Proposition 2(a), we obtain $w = \phi (path(F{{S}_{{{{\pi }_{\sigma }}}}}({{\rho }_{\sigma }})))$ = $\phi '(path(F{{S}_{{\pi '}}}(f({{\rho }_{\sigma }}))))$ ∈ $\mathcal{L}(TCT(\mathcal{T}\mathcal{N}{\kern 1pt} '))$. □

4 TESTING EQUIVALENCES

In the framework of the interleaving approach to defining testing equivalence, the tests are sequences w of actions executed (system computations) and sets W of possible subsequent actions. The process passes the test if, after execution of each sequence w of actions, at least one action from W can be executed. Two processes are testing equivalent if they pass the same set of tests. In the time variant, information on action execution times is added.

Definition 7. Let $\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ be time Petri nets.

For a sequence $w \in (Act \times \mathbb{T}){\text{*}}$ and a set W ⊆ $(Act \times \mathbb{T})$, $\mathcal{T}\mathcal{N}$afterwMUST$_{{int}}$W if, for all $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ such that $L(\sigma ) = w$, there exist $(a,\theta )$ ∈ W and $\sigma (t,\theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N})$ such that $L(\sigma (t,\theta ))$ = w(a, θ).

$\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ are said to be interleaving testing equivalent (denoted as $\mathcal{T}\mathcal{N}{{ \sim }_{{int}}}\mathcal{T}\mathcal{N}'$) if, for any sequence $w \in (Act \times \mathbb{T}){\text{*}}$ and any set $W \subseteq (Act \times \mathbb{T})$, $\mathcal{T}\mathcal{N}$afterwMUST$_{{int}}$$W$$\Leftrightarrow$$\mathcal{T}\mathcal{N}$' afterwMUST$_{{int}}$W.

Example 6. The time Petri nets $\mathcal{T}{{\mathcal{N}}_{2}}$, $\mathcal{T}{{\mathcal{N}}_{3}}$, and $\mathcal{T}{{\mathcal{N}}_{4}}$ depicted in Fig. 7 are interleaving testing equivalent, whereas $\mathcal{T}{{\mathcal{N}}_{1}}$ and $\mathcal{T}{{\mathcal{N}}_{2}}$ are not. It is easy to verify that $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$after$w = (b,0)(b,0)$${\mathbf{MUS}}{{{\mathbf{T}}}_{{int}}}$W = $\{ (a,3.9)\}$. However, in $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$, there exists a firing sequence labeled by w after which the transition labeled by a cannot fire at the time moment 3.9. Thus, the condition $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$afterw${\mathbf{MUS}}{{{\mathbf{T}}}_{{int}}}$W does not hold. □

Testing equivalences that take into account causal dependencies between actions were first introduced by Aceto et al. in [5] in the context of event structure models. For the process computations, they considered partially ordered multisets (pomsets) instead of sequences of executed actions. In [6], instead of sets of subsequent actions, directed extensions of executed pomsets were used. In addition, in [6], one more version of causal testing equivalence was suggested, which uses posets of executed actions as the computations. It was shown that this is a stronger equivalence. Following this approach, we further define the time poset based testing equivalence for time Petri nets with the use of its correct time causal processes.

Definition 8. Let $\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ be time Petri nets.

For a time poset TP and a set TP of time posets such that $TP \prec \cdot$⁷$TP'$, for any $TP' \in {\mathbf{TP}}$, $\mathcal{T}\mathcal{N}$afterTPMUST$_{{tpos}}$TP if, for any $\pi = (TN,\varphi ) \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$ and any isomorphism $f{\kern 1pt} :\;\eta (TN) \to TP$, there exist $TP' \in {\mathbf{TP}}$, π' = $(TN',\varphi ') \in \mathcal{C}\mathcal{P}(\mathcal{T}\mathcal{N})$, and isomorphism f  ' : $\eta (TN')$ → TP' such that $\pi \to \pi '$ and $f \subseteq f'$.

$\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ are called posettesting equivalent (denoted as $\mathcal{T}\mathcal{N}{{ \sim }_{{tpos}}}\mathcal{T}\mathcal{N}'$) if, for any time poset TP and any set ${\mathbf{TP}}$ of time posets such that $TP \prec \cdot TP'$, for all $TP' \in {\mathbf{TP}}$, the following condition holds: $\mathcal{T}\mathcal{N}$afterTPMUST$_{{tpos}}$${\mathbf{TP}}$$\Leftrightarrow$$\mathcal{T}\mathcal{N}'$afterTPMUST$_{{tpos}}$${\mathbf{TP}}'$.

Example 7. Consider the time Petri nets $\mathcal{T}{{\mathcal{N}}_{2}}$, $\mathcal{T}{{\mathcal{N}}_{3}}$, and $\mathcal{T}{{\mathcal{N}}_{4}}$ depicted in Fig. 7. It is easy to see that $\mathcal{T}{{\mathcal{N}}_{2}}$ and $\mathcal{T}{{\mathcal{N}}_{3}}$ are poset testing equivalent, whereas $\mathcal{T}{{\mathcal{N}}_{3}}$ and $\mathcal{T}{{\mathcal{N}}_{4}}$ are not. Let us prove the latter. Consider the time poset $TP = (\{ {{x}_{1}},{{x}_{2}}\} , \preccurlyeq ,\lambda ,\tau ),$ where $\preccurlyeq = \{ ({{x}_{i}},{{x}_{i}})\,|\,1 \leqslant i \leqslant 2\}$, $\lambda ({{x}_{1}}) = \lambda ({{x}_{2}})$ = b, $\tau ({{x}_{1}})\, = \,\tau ({{x}_{2}})$ = 0, and the time poset $TP' = (\{ {{x}_{1}},{{x}_{2}},{{x}_{3}}\} , \preccurlyeq ,\lambda ',\tau ')$, where $\preccurlyeq \, = \{ ({{x}_{i}},{{x}_{i}})\,|\,1 \leqslant i \leqslant 3\} \cup \{ ({{x}_{2}},{{x}_{3}})\}$, $\lambda '({{x}_{1}})$ = λ'(x₂) = b, $\lambda '({{x}_{3}}) = a$, $\tau '({{x}_{1}}) = \tau '({{x}_{2}}) = 0$, and $\tau '({{x}_{3}})$ = 3.9. For any time causal process π₃ = (TN₃, ${{\varphi }_{3}}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{3}})$ in which ${{E}_{{T{{N}_{3}}}}}$ consists of two concurrent events with labels b and time values equal to 0 and any isomorphism ${{f}_{3}}:\eta (T{{N}_{3}}) \to TP$, one can find a time causal process $\pi _{3}^{'} = (TN_{3}^{'},\varphi _{3}^{'}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{3}})$, in which ${{E}_{{T{{N}_{3}}}}}$ consists of two concurrent events with labels b and time values equal to 0 and a third event with label a and time value 3.9 that is in a relation of causal dependence with one of b, and isomorphism $f_{3}^{'}\eta (TN_{3}^{'}) \to TP'$ such that ${{\pi }_{3}} \to \pi _{3}^{'}$ and ${{f}_{3}} \subset f_{3}^{'}$. However, this is not true in the case of the time Petri net $\mathcal{T}{{\mathcal{N}}_{4}}$. □

Further, we define testing equivalence for time Petri nets based on their time causal trees having in mind the method employed for the event structure model in [6]. The tests will be constructed taking into account time values based on the set of labels of $Act \times \mathbb{T} \times {{2}^{\mathbb{N}}}$ tree arcs.

Definition 9. Let $\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ be time Petri nets, and let $TCT(\mathcal{T}\mathcal{N}) = (\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}),A,\phi )$ and $TCT(\mathcal{T}\mathcal{N}')$ = $(\mathcal{F}\mathcal{S}(\mathcal{T}\mathcal{N}')$, A', ϕ') be their time causal trees. For a sequence $w \in (Act \times \mathbb{T} \times {{2}^{\mathbb{N}}}){\text{*}}$ and a set W ⊆ (Act × $\mathbb{T} \times {{2}^{\mathbb{N}}})$, $TCT(\mathcal{T}\mathcal{N})$afterwMUST$_{{tct}}$W if, for all paths u in $TCT(\mathcal{T}\mathcal{N})$ from the root to the node n such that $\phi (u) = w$, there exist a label $(a,d,K) \in {\mathbf{W}}$ and an arc r from the node n such that $\phi (r) = (a,d,K)$;

$\mathcal{T}\mathcal{N}$ and $\mathcal{T}\mathcal{N}'$ are causal tree testing equivalent (denoted as $\mathcal{T}\mathcal{N}$${{ \sim }_{{tct}}}$$\mathcal{T}\mathcal{N}'$) if, for any sequence $w \in (Act \times \mathbb{T} \times {{2}^{\mathbb{N}}}){\text{*}}$ and any set ${\mathbf{W}} \subseteq (Act \times \mathbb{T} \times {{2}^{\mathbb{N}}})$, $TCT(\mathcal{T}\mathcal{N})$afterw${\mathbf{MUS}}{{{\mathbf{T}}}_{{tct}}}$W$\Leftrightarrow$$TCT(\mathcal{T}\mathcal{N})$afterw${\mathbf{MUS}}{{{\mathbf{T}}}_{{tct}}}$${\mathbf{W}}$.

Example 8. Consider the time Petri nets $\mathcal{T}{{\mathcal{N}}_{2}}$, $\mathcal{T}{{\mathcal{N}}_{3}}$, and $\mathcal{T}{{\mathcal{N}}_{4}}$ depicted in Fig. 7. It is easy to see that $\mathcal{T}{{\mathcal{N}}_{2}}$ and $\mathcal{T}{{\mathcal{N}}_{3}}$ are causal tree testing equivalent, whereas $\mathcal{T}{{\mathcal{N}}_{3}}$ and $\mathcal{T}{{\mathcal{N}}_{4}}$ are not. Let us prove the latter. To this end, we define $w = (b,0,\emptyset )(b,0,\emptyset )$ and W = $\{ (a,3.9,\{ 1\} )\}$. It is easy to check that $TCT(\mathcal{T}{{\mathcal{N}}_{3}})$afterw${\mathbf{MUS}}{{{\mathbf{T}}}_{{tct}}}$W. In $TCT(\mathcal{T}{{\mathcal{N}}_{4}})$, there are two paths labeled as $(b,0,\emptyset )(b,0,\emptyset )$; one of them terminates at a node from which an arc with label $(a,3.9,\{ 1\} )$ originates, and the other terminates at a node that lacks such an arc. Thus, the condition $TCT(\mathcal{T}{{\mathcal{N}}_{4}})$afterw${\mathbf{MUS}}{{{\mathbf{T}}}_{{tct}}}$W does not hold. □

From the definitions of the interleaving, poset, and causal tree testing equivalences, we immediately get the following

Lemma 3. Let $\mathcal{T}{{\mathcal{N}}_{1}}$ and $\mathcal{T}{{\mathcal{N}}_{2}}$ be time Petri nets. Then,

$$\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{int}}}\mathcal{T}{{\mathcal{N}}_{2}} \Rightarrow \mathcal{L}(\mathcal{T}{{\mathcal{N}}_{1}}) = \mathcal{L}(\mathcal{T}{{\mathcal{N}}_{2}}),$$

$$\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tpos}}}\mathcal{T}{{\mathcal{N}}_{2}} \Rightarrow \mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{1}}) = \mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{2}}),$$

$$\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tct}}}\mathcal{T}{{\mathcal{N}}_{2}} \Rightarrow \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{1}})) = \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}})).$$

Let us establish relationship between the interleaving and causal tree testing equivalences.

Theorem 1.$\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tct}}}\mathcal{T}{{\mathcal{N}}_{2}} \Rightarrow \mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{int}}}\mathcal{T}{{\mathcal{N}}_{2}}$.

Proof. Suppose that $\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tct}}}\mathcal{T}{{\mathcal{N}}_{2}}$. Let us show that $\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{int}}}\mathcal{T}{{\mathcal{N}}_{2}}$. Assume the contrary. Let there exist $w \in (Act \times \mathbb{T}){\text{*}}$ and $W \subseteq (Act \times \mathbb{T})$ such that $\mathcal{T}{{\mathcal{N}}_{1}}$afterwMUST_intW; however, $\neg (\mathcal{T}{{\mathcal{N}}_{2}}$afterwMUST_intW). The latter means that there exists ${{\sigma }_{2}} \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{2}})$ such that $L({{\sigma }_{2}})$ = w and that, for any $(a,\theta ) \in W$ and ${{\sigma }_{2}}(t',\theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{2}})$, the condition $L({{\sigma }_{2}}(t',\theta )) = w(a,\theta )$ does not hold. Taking into account the definitions, we find that $w \in \mathcal{L}(\mathcal{T}{{\mathcal{N}}_{2}})$ and, moreover, $\tilde {w} = {{\phi }_{2}}(path({{\sigma }_{2}})) \in \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}}))$, with $\tilde {w}{{{\text{|}}}_{{(Act \times \mathbb{T}){\text{*}}}}}$ = w. Let us introduce the set W = {(a, θ, $K)\,{\text{|}}\,(a,\theta ) \in W$, $\exists \sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{1}})$ : L(σ) = w and ${{\phi }_{1}}(path(\sigma ))$ = $\tilde {w}$, $\exists$ an arc r from $\sigma$ in $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$ : ϕ₁(r) = (a, θ, K)}. Let us show that $\mathcal{T}{{\mathcal{N}}_{1}}$after$\tilde {w}$MUST_tctW. Take an arbitrary ${{\sigma }_{1}} \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{1}})$ such that ${{\phi }_{1}}(path({{\sigma }_{1}}))$ = $\tilde {w}$. Such a σ₁ exists, since $\tilde {w} \in \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{1}}))$, by Lemma 3. Moreover, $w \in \mathcal{L}(\mathcal{T}{{\mathcal{N}}_{1}})$, according to Proposition 3. Since $\mathcal{T}{{\mathcal{N}}_{1}}$afterwMUST_intW, there exist $(a,\theta ) \in W$ and σ₁(t, $\theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{1}})$ such that $L({{\sigma }_{1}}(t,\theta ))$ = w(a, θ). By the construction of the time causal tree, there is an arc r = $({{\sigma }_{1}},{{\sigma }_{1}}(t,\theta ))$ in $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$ such that ${{\phi }_{1}}(r)$ = (a, θ, K). Hence, it follows that ${{\phi }_{1}}(r) \in {\mathbf{W}}$. By virtue of arbitrariness of ${{\sigma }_{1}}$, we have $\mathcal{T}{{\mathcal{N}}_{1}}$after$\tilde {w}$MUST$_{{tct}}$W. Thus, we arrived at the contradiction, since it is easy to check that $\neg (\mathcal{T}{{\mathcal{N}}_{2}}$after$\tilde {w}$MUST$_{{tct}}$W). □

In conclusion, we show that testing equivalences for time causal trees in the semantics of time partially ordered sets and time causal trees coincide.

Theorem 2. Let $\mathop {\mathcal{T}\mathcal{N}}\nolimits_1$ and $\mathop {\mathcal{T}\mathcal{N}}\nolimits_2$ be time Petri nets. Then,

$$\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tpos}}}\mathcal{T}{{\mathcal{N}}_{2}} \Leftrightarrow \mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tct}}}\mathcal{T}{{\mathcal{N}}_{2}}.$$

Proof. Let us prove from left to right (the proof from right to left is similar). Let $TCT(\mathcal{T}{{\mathcal{N}}_{i}})$ = $(\mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{i}})$, A_i, ϕ_i) (i = 1, 2). Suppose that $\mathcal{T}{{\mathcal{N}}_{1}}$${{ \sim }_{{tpos}}}$$\mathcal{T}{{\mathcal{N}}_{2}}$. Then, according to Lemma 3, we have $\mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{1}})$ = $\mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{2}})$. From Proposition 3, we obtain $\mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{1}})) = \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}}))$. Let us show that $\mathcal{T}{{\mathcal{N}}_{1}}{{ \sim }_{{tct}}}\mathcal{T}{{\mathcal{N}}_{2}}$. Take arbitrary w ∈ $(Act \times \mathbb{T} \times {{2}^{\mathbb{N}}}){\text{*}}$ and ${\mathbf{W}} \subseteq (Act \times \mathbb{T} \times {{2}^{\mathbb{N}}})$. Without loss of generality, we assume that $\left| w \right| = n$ (n ≥ 0). Suppose that $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$afterwMUST$_{{tct}}$W. Let us check that $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$after$w$MUST$_{{tct}}$${\mathbf{W}}$.

If $w \notin \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{1}})) = \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}}))$, then the result is evident. Consider the case where w ∈ $\mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{1}}))$ = $\mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}}))$. Then, we can take any path u from the root to some node $\sigma \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{1}})$ such that ${{\phi }_{1}}(u) = w$. According to Proposition 1(b), there exists a unique (up to isomorphism) time causal process ${{\pi }_{\sigma }} = (T{{N}_{\sigma }},{{\varphi }_{\sigma }}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{1}})$ and a unique linearization ${{\rho }_{\sigma }} = e_{1}^{\sigma } \ldots e_{n}^{\sigma }$TN_σ such that $F{{S}_{{{{\pi }_{\sigma }}}}}({{\rho }_{\sigma }})$ = σ. Let us denote $T{{P}_{w}} = \eta (T{{N}_{\sigma }})$ ∈ $\mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{1}})$.

For each $(a,\theta ,K) \in {\mathbf{W}}$, we construct a time poset $T{{P}_{{(a,\theta ,K)}}} = (X, \preccurlyeq ,\lambda ,\tau )$ as follows: $X = {{E}_{{T{{N}_{\sigma }}}}} \cup \{ {{e}_{{(a,\theta ,K)}}}\}$ (${{e}_{{(a,\theta ,K)}}}\not \in {{E}_{{T{{N}_{\sigma }}}}}$); $\preccurlyeq = {{ \preccurlyeq }_{{T{{N}_{\sigma }}}}} \cup \;\{ (e_{{n - k + 1}}^{\sigma }$, ${{e}_{{(a,\theta ,K)}}})\,|\,k \in K\}$; $\lambda {{{\text{|}}}_{{{{E}_{{T{{N}_{\sigma }}}}}}}} = {{\lambda }_{{T{{N}_{\sigma }}}}}$, $\lambda ({{e}_{{(a,\theta ,K)}}})$ = a; $\tau {{{\text{|}}}_{{{{E}_{{T{{N}_{\sigma }}}}}}}} = {{\tau }_{{T{{N}_{\sigma }}}}}$, $\tau ({{e}_{{(a,\theta ,K)}}})$ = τ(TN_σ) + θ. The set of all constructed time posets is denoted as ${\mathbf{T}}{{{\mathbf{P}}}_{{\mathbf{W}}}}\{ T{{P}_{{(a,\theta ,K)}}}\,|\,(a,\theta ,K) \in {\mathbf{W}}\}$.

Let us check that $\mathcal{T}{{\mathcal{N}}_{1}}$after$T{{P}_{w}}$MUST$_{{tpos}}$TP_W. Take an arbitrary time causal process of the net π₁ = $(T{{N}_{1}},{{\varphi }_{1}}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{1}})$ and an isomorphism f₁: $\eta (T{{N}_{1}}) \to T{{P}_{w}}$. Since $T{{P}_{w}} \in \mathcal{T}\mathcal{P}os(\mathcal{T}{{\mathcal{N}}_{1}})$, such ${{\pi }_{1}}$ and f₁ exist. From Proposition 2(a), we find that $e_{1}^{1} \ldots e_{n}^{1}$ = ${{\rho }_{1}} = {{({{f}_{1}})}^{{ - 1}}}:\eta (T{{N}_{\sigma }})$ → $\eta (T{{N}_{1}})({{\rho }_{\sigma }})$ is a linearization of TN₁ such that $w = \phi (path({{\sigma }_{1}} = F{{S}_{{{{\pi }_{1}}}}}({{\rho }_{1}})))$. Since $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$afterwMUST$_{{tct}}$W, there exists a label $(a_{1}^{'},\theta _{1}^{'},K_{1}^{'}) \in {\mathbf{W}}$ and an arc r₁ from node σ₁ such that ${{\phi }_{1}}({{r}_{1}}) = (a_{1}^{'},\theta _{1}^{'},K_{1}^{'})$. Then, one can find $TP_{1}^{'} = T{{P}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}}$ ∈ TP_W. Hence, by construction of the set TP_W, we find that $\{ {{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}}\} = {{E}_{{TP_{1}^{'}}}}{\backslash }{{E}_{{T{{N}_{\sigma }}}}}$, $a_{1}^{'} = {{\lambda }_{{TP_{1}^{'}}}}({{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}})$, $\theta _{1}^{'}$ = ${{\tau }_{{TP_{1}^{'}}}}({{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}})$ – τ(TN_σ), $K_{1}^{'}$ = {n – l + 1 | $e_{l}^{\sigma }$${{ \preccurlyeq }_{{TP_{1}^{'}}}}$${{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}}\}$. Moreover, by the definition of $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$, there exists ${{\sigma }_{1}}(t_{1}^{'},\theta _{1}^{'}) \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{1}})$, ($t_{1}^{'} \in {{T}_{{\mathcal{T}{{\mathcal{N}}_{1}}}}}$) such that ${{r}_{1}} = ({{\sigma }_{1}},{{\sigma }_{1}}(t_{1}^{'},\theta _{1}^{'}))$ and ${{\phi }_{1}}(\sigma _{1}^{'},{{\sigma }_{1}}(t_{1}^{'},\theta _{1}^{'}))$ = $({{l}_{{\mathcal{T}{{\mathcal{N}}_{1}}}}}(t_{1}^{'})$ = $a_{1}^{'},\theta _{1}^{'},K_{1}^{'})$. From Lemma 2(a), it follows that there is a time causal process $\pi _{1}^{'} = (TN_{1}^{'},\varphi _{1}^{'}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{1}})$ such that ${{\pi }_{1}} \to \pi _{1}^{'}$ and ${{\sigma }_{1}}(t_{1}^{'},\theta _{1}^{'}) = F{{S}_{{\pi _{1}^{'}}}}({{\rho }_{1}}e_{1}^{'})$ for some linearization ${{\rho }_{1}}e_{1}^{'}$ of $TN_{1}^{'}$, i.e., $\varphi _{1}^{'}(e_{1}^{'}) = t_{1}^{'}$. Let us define function $f_{1}^{'}{\kern 1pt} :\;\eta (TN_{1}^{'}) \to TP_{1}^{'}$ as follows: $f_{1}^{'}{{{\text{|}}}_{{{{E}_{{\eta (T{{N}_{1}})}}}}}}$ = f₁, $f_{1}^{'}(e_{1}^{'})$ = ${{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}}$. In addition, ${{\lambda }_{{\eta (TN_{1}^{'})}}}(e_{1}^{'}) = a_{1}^{'} = {{\lambda }_{{\mathop {TP}\nolimits_1 }}}({{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}})$; ${{\tau }_{{\eta (TN_{1}^{'})}}}(e_{1}^{'}) = \theta _{1}^{'} + \tau (T{{N}_{1}})$ = $\theta _{1}^{'} + \tau (T{{N}_{\sigma }}) = {{\tau }_{{TP_{1}^{'}}}}({{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}})$; $e_{{n - k + 1}}^{1}{{ \preccurlyeq }_{{\eta (TN_{1}^{'})}}}e_{1}^{'}$$\Leftrightarrow$$f_{1}^{'}(e_{{n - k + 1}}^{1}) = e_{{n - k + 1}}^{\sigma } \preccurlyeq {{\;}_{{\mathop {TP}\nolimits_1 }}}{{e}_{{(a_{1}^{'},\theta _{1}^{'},K_{1}^{'})}}}$ for all $k \in K_{1}^{'}$. Hence, $f_{1}^{'}$ is an isomorphism and ${{f}_{1}} \subseteq f_{1}^{'}$. Thus, $\mathcal{T}{{\mathcal{N}}_{1}}$afterTP_wMUST$_{{tpos}}$TP_W. Then, by the assumption of the theorem, $\mathcal{T}{{\mathcal{N}}_{2}}$afterTP_wMUST$_{{tpos}}$TP_W.

Further, let us show that $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$afterwMUST$_{{tct}}$W. Take an arbitrary path u₂ in $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$ from the root to the node ${{\sigma }_{2}}$ such that ${{\phi }_{2}}({{u}_{2}}) = w$. Since $w \in \mathcal{L}(TCT(\mathcal{T}{{\mathcal{N}}_{2}}))$, there is at least one such a path u₂ in $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$. In accordance with Proposition 1(b), there exists a unique (up to isomorphism) time causal process ${{\pi }_{{{{\sigma }_{2}}}}} = (T{{N}_{2}},{{\varphi }_{2}}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{2}})$ and a unique linearization ${{\rho }_{2}} = e_{1}^{2} \ldots e_{n}^{2}$ of $T{{N}_{2}}$ such that $F{{S}_{{{{\pi }_{{{{\sigma }_{2}}}}}}}}({{\rho }_{2}})$ = σ₂. Using Proposition 2(b), we find that there is an isomorphism ${{f}_{2}}:\eta (T{{N}_{2}}) \to T{{P}_{w}}$ such that ${{f}_{2}}({{\rho }_{2}}) = {{\rho }_{\sigma }}$. Since $\mathcal{T}{{\mathcal{N}}_{2}}$afterTP_wMUST$_{{tpos}}$TP_W, there exist $TP_{2}^{'} \in {\mathbf{T}}{{{\mathbf{P}}}_{{\mathbf{W}}}}$, $\pi _{{{{\sigma }_{2}}}}^{'} = (TN_{2}^{'},\varphi _{2}^{'}) \in \mathcal{C}\mathcal{P}(\mathcal{T}{{\mathcal{N}}_{2}})$, and an isomorphism $f_{2}^{'}:\eta (TN_{2}^{'}) \to TP_{2}^{'}$ such that ${{\pi }_{{{{\sigma }_{2}}}}} \to \pi _{2}^{'}$ and ${{f}_{2}} \subseteq f_{2}^{'}$. According to Lemma 2(b), there is ${{\sigma }_{2}}(\widetilde t,\widetilde \theta ) \in \mathcal{F}\mathcal{S}(\mathcal{T}{{\mathcal{N}}_{2}})$ such that, for some linearization ${{\rho }_{2}}e_{2}^{'}$ of $TN_{2}^{'}$, we have ${{\sigma }_{2}}(\widetilde t,\widetilde \theta ) = F{{S}_{{\pi _{2}^{'}}}}({{\rho }_{2}}e_{2}^{'})$. By construction of TP_W, there exists a label $(a,\theta ,K) \in {\mathbf{W}}$ such that $TP_{2}^{'} = T{{P}_{{(a,\theta ,K)}}}$, and, hence, {e_{(a, θ, K)}} = ${{E}_{{TP_{2}^{'}}}}{\backslash }{{E}_{{T{{N}_{\sigma }}}}}$. Since $T{{N}_{2}} \to TN_{2}^{'}$ and $T{{P}_{w}} \prec \cdot TP_{2}^{'}$, we have $\{ e_{2}^{'}\} = {{E}_{{TN_{2}^{'}}}}{\backslash }{{E}_{{T{{N}_{2}}}}}$ and $f_{2}^{'}(e_{2}^{'})$ = e_{(a, θ, K)}. Since $f_{2}^{'}$ is an isomorphism, we have ${{\lambda }_{{\eta (TN_{2}^{'})}}}(e_{2}^{'}) = {{\lambda }_{{TP_{2}^{'}}}}({{e}_{{(a,\theta ,K)}}})$ = a, ${{\tau }_{{\eta (TN_{2}^{'})}}}(e_{2}^{'}) = {{\tau }_{{TP_{2}^{'}}}}({{e}_{{(a,\theta ,K)}}}) = \tau (T{{N}_{\sigma }}) + \theta$ = $\tau (T{{N}_{2}})$ + θ, and $e_{i}^{\sigma }{{ \preccurlyeq }_{{TP_{2}^{'}}}}{{e}_{{(a,\theta ,K)}}}$$\Leftrightarrow$${{(f_{2}^{'})}^{{ - 1}}}(e_{i}^{\sigma }) = e_{i}^{2}{{ \preccurlyeq }_{{\eta (TN_{2}^{'})}}}e_{2}^{'}$ for all $1 \leqslant i \leqslant n$. Then, it follows that $(\widetilde t,\widetilde \theta ) = (\varphi _{2}^{'}(e_{2}^{'}),\theta )$ and $e_{{n - k + 1}}^{2} \preccurlyeq {{\;}_{{\eta (TN_{2}^{'})}}}e_{2}^{'}$ for all $k \in K$. Hence, in $TCT(\mathcal{T}{{\mathcal{N}}_{2}})$, there exists an arc ${{r}_{2}} = ({{\sigma }_{2}},{{\sigma }_{2}}(\widetilde t,\widetilde \theta ))$ such that ${{\phi }_{2}}({{r}_{2}})$ = (a, θ, K). Thus, we have $TCT(\mathcal{T}{{\mathcal{N}}_{1}})$afterwMUST_tctW$\Rightarrow$$TCT(\mathcal{T}{{\mathcal{N}}_{2}})$afterwMUST_tctW.

In view of symmetry, we have $\mathcal{T}{{\mathcal{N}}_{1}}$${{ \sim }_{{tpos}}}$$\mathcal{T}{{\mathcal{N}}_{2}} \Rightarrow$$\mathcal{T}{{\mathcal{N}}_{1}}$${{ \sim }_{{tct}}}$$\mathcal{T}{{\mathcal{N}}_{2}}$. □

5 CONCLUSIONS

We have shown that some well-known causality-based testing equivalences employed in the untimed and timed event structures literature can be extended to time Petri nets. In particular, we have introduced and studied testing equivalences in interleaving, partial order, and combined semantics in the setting of safe Petri nets with strong timing (transitions are labeled with time firing intervals, enabled transitions are able to fire only if their lower time bounds are attained, and are forced to fire when their upper time bounds are reached). In doing so, we dealt with three behavioral representations of time Petri nets: firing sequences representing interleaving semantics; time causal net processes, from causal nets of which partial orders are derived; and causal tree semantics constructed from the firing sequences and partial orders. We have found relationships, firstly, between the firing sequences and correct time processes for time Petri nets and, secondly, between labeled paths in time causal trees and correct time processes. We have established that the interleaving testing equivalence is weaker than that determined with the use of the time causal tree. The main result of the study is the proof of the coincidence of the testing equivalences in the semantics of time partial orders and time causal trees. It is worth noting that this result is also true for the untimed versions of the equivalences in the setting of untimed contact-free elementary net systems.

As for the future work, we plan to study the relationship between the equivalences and semantics under consideration and those in the linear-time/branching-time and interleaving/partial order spectra ([25]). We also plan to study the possibility of extending the results obtained to time Petri nets with invisible actions.