# Decidability problems for weak Time Petri Nets with read, reset and transfer arcs

Didier Lime, Rémi Parrot, Olivier H. Roux

► To cite this version:

Didier Lime, Rémi Parrot, Olivier H. Roux. Decidability problems for weak Time Petri Nets with read, reset and transfer arcs. Petri Net 2025, Jun 2025, Paris, France. pp.333-353, 10.1007/978-3-031-94634-9_16. hal-05513518

HAL Id: hal-05513518

https://hal.science/hal-05513518v1

Submitted on 16 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Decidability problems for weak Time Petri Nets
with read, reset and transfer arcs

Didier Lime¹[0000-0001-9429-7586], Rémi Parrot¹[0000-0002-1943-8171], and
Olivier H. Roux¹[0000-0003-1665-0481]

Nantes Université, École Centrale Nantes, CNRS, LS2N, UMR 6004, F-44000 Nantes,
France

`{firstname}.{surname}@ls2n.fr`

**Abstract.** We address the class of Time Petri Nets (TPNs) where time intervals are associated with transitions and constrain when those transitions can be fired. For TPN with strong semantics, i.e. where time elapsing cannot disable transitions, reachability, coverability and boundedness problems are undecidable. They are however decidable with the weak semantics in which time elapsing can disable transitions.

We first propose an intermediate semantics allowing us to study the decidability border between weak and strong semantics. We prove that with only one transition in strong semantics, reachability, coverability and boundedness are undecidable.

We then consider the so-called read, reset and transfer arcs for which the
coverability problem is decidable in the untimed context and we study
their impact on TPN with a weak semantics (weak TPN). We prove that
coverability becomes undecidable for weak TPN when we add either 2
read arcs, or 2 reset arcs, or 2 transfer arcs.

Lastly, considering bounded nets, we propose a state space computation
algorithm for weak TPN with read, reset and transfer arcs that proves
the decidability of the reachability problem.

**Keywords:** Time Petri nets · Weak semantics · Read arc · Reset arc · Transfer arc · Decidability · State Class Graph.

# 1 Introduction

A number of extensions of Petri Nets with time have been proposed where time
can be a duration or an interval that can be associated with arcs, places or
transitions (see [4] for a survey). In these timed extensions of Petri nets, two
types of semantics can be considered for time elapsing. In the strong semantics,
time elapsing cannot disable transitions whereas in the weak semantics, all time
delays are allowed.

In this paper, we address the class of Time Petri Nets [9] where time intervals
are associated with transitions, which is one of the most commonly-used subclass
of Petri nets with time. It will henceforth be referred to as TPN.
For bounded TPN, reachability and coverability problems are decidable for both semantics [2, 12]. But for unbounded nets these problems are undecidable with the strong semantics [7] and decidable with the weak one [12].

We propose an intermediate model between these two semantics with a cursor allowing us to study the decidability border between weak and strong semantics.

In the same spirit, we propose to study the classical read, reset and transfer arcs for which the coverability problem is decidable in the untimed case and to study their impact on TPNs in weak semantics.

Reset and transfer nets have been studied as particular cases of the so-called Generalized Self-Modifying nets [6]. Reachability is undecidable [1] and coverability is decidable for reset and transfer nets, whereas boundedness is decidable for transfer but not for reset nets.

Read arcs describe reading without consuming [13] and have been introduced as test arcs [5] or as particular case of Contextual nets [11]. Without taking true concurrency into account, a read arc can be simulated by both an input arc and an output arc between the read place and the reading transition. Hence reachability and coverability are decidable for Petri Nets with read arcs.

*Contributions.* We introduce a new formalism blending together the weak and strong semantics pushing the idea of [8] further. We call it Weakly-strong TPNs (WS-TPNs).

We prove that with TPNs with weak semantics, we are very close to the decidability border: if we allow a single transition to behave with strong semantics, then coverability is undecidable. Similarly, if we allow two read arcs, or two reset arcs, or two transfer arcs, we also have undecidability of coverability.

In light of these negative results, we then focus on bounded TPNs mixing strong and weak semantics and give and prove an algorithm to explicitly compute a finite abstraction of its state-space, as an extension of the classical state class graph of Berthomieu [2].

*Outline.* In Section 2, we introduce the formalism of WS-TPNs and related definitions, as well as TPNs (with weak semantics) with read, reset, and transfer arcs. In Section 3, we prove the aforementioned undecidability results. In Section 4, we extend the state class graph construction to WS-TPNs. Finally, we conclude in Section 5.

## 2 Weakly-Strong Time Petri Nets

$\mathbb{N}, \mathbb{Z}$ and $\mathbb{R}_+$ are respectively the sets of natural integers, integers and non-negative real numbers. For a finite set $X$ with of size $|X| = n$, an element of $A^X$ can also be seen as a vector in $A^n$ (with $A = \mathbb{N}, \mathbb{Z}, \mathbb{R}_+$), by fixing an arbitrary order on the elements of $X$. The usual operators $+, -, \times, <, \leq, >, \geq$ and $=$ are used on vectors of $A^n$ and are the point-wise extensions of their counterparts in $A$. We call *valuation* an element $\nu \in A^X$. For such a valuation and for $d \in A$, $\nu + d$ denotes the vector $(\nu + d)(x) = \nu(x) + d$.
Let $I_{\mathbb{N}}$ and $I_{\mathbb{R}_+}$ be the set of intervals whose finite bounds (or end-points) are respectively in $\mathbb{N}$ and $\mathbb{R}_+$. Let $I \in I_{\mathbb{R}_+}$, $I$ is its lower bound and $\bar{I}$ is its upper bound if it exists, $+\infty$ otherwise. Let $d \in \mathbb{R}_+$, $I-d$ denotes the (possibly empty) interval defined by: $I-d = \{x-d \mid x \in I \text{ and } x \ge d\}$. The downward closure of $I$ is denoted by $\downarrow I = \{x \in \mathbb{R}_+ \mid \exists y \in I \text{ and } x \le y\}$. The closure of $I$ is denoted by $\text{cl}(I) = \{x \in \mathbb{R}_+ \mid I \le x \text{ and if } \bar{I} \ne +\infty, x \le \bar{I}\}$.

## 2.1 Definition of Weakly-Strong Time Petri Nets (WS-TPNs)

**Definition 1 (Petri nets).** A Petri net (PN) is a tuple $N = (P, T, F, m_0)$ where

- $P$ is a finite set of places;

- $T$ is a finite set of transitions with $P \cap T = \emptyset$;

- $m_0 \in \mathbb{N}^P$ is the initial marking;

- $F: (P \times T) \cup (T \times P) \to \mathbb{N}$ is a flow (and weight) function where $F(x,y)$ is the weight of the arc from $x$ to $y$ and is zero if there is no arc from $x$ to $y$.

A marking $m$ (state) is a mapping in $\mathbb{N}^P$ and $m(p)$ is the number of tokens in place $p$.

$\forall t \in T$, we denote $\bullet t$ and $t^\bullet$ the backward and forward vectors in $\mathbb{N}^{|P|}$ s.t. $\forall p \in P, \bullet t(p) = F(p,t)$ and $t^\bullet(p) = F(t,p)$.

The state (marking) of a net evolves according to usual firing rules of transitions:

- A transition $t \in T$ is enabled by $m$ if each input place $p$ of $t$ is marked with at least $F(p,t)$ tokens i.e. $m \ge \bullet t$. Let $\text{enab}(m) = \{t \in T \mid m \ge \bullet t\}$ be the set of transitions enabled by $m$.

- An enabled transition $t \in T$ can fire leading to a new marking $m' = m - \bullet t + t^\bullet$

A time Petri net extends the definition of Petri net, by considering that a transition requires some time to be ready to fire.

**Definition 2.** A Time Petri Net (TPN) is the tuple $(P, T, F, m_0, I_s)$ where $(P, T, F, m_0)$ is a Petri net and $I_s: T \to I_{\mathbb{N}}$ is a map called the static firing interval function that associates a temporal (firing) interval with any transition.

In a TPN, a transition $t \in T$ can fire if it has been enabled for a time belonging to its interval $I_s(t)$. There exists two semantics defining what happens at the upper bound of the firing interval. Intuitively,

- Under the strong semantics, time is not allowed to elapse anymore if the end of the interval has been reached. The transition has to fire, or has to be disabled by the firing of another transition.

- Under the weak semantics, time can be elapsed regardless of enabled transitions. However, if an enabled transition outreaches its firing interval, then it will not be able to fire anymore. It is considered asleep, until it is disabled by the firing of another transition.
We propose a new class of time Petri net allowing to express both semantics, and some in-betweens, in a unique framework.

**Definition 3.** A Weakly-Strong Time Petri Net (WS-TPN) is the tuple $N = \langle P, T, F, m_0, I_s, \Pi \rangle$ where $\langle P, T, F, m_0, I_s \rangle$ is a TPN and $\Pi \subseteq 2^T$ is a set of subsets of $T$ called packs.

In WS-TPNs, time can be elapsed only if no pack $\pi \in \Pi$ sees all its enabled transitions $t \in \pi$ outreach their firing intervals (fall asleep). In other words, it is possible to outreach the firing interval of some transitions by elapsing time, but not all the enabled transitions of one pack.

A time Petri net is usually represented by a bipartite directed graph where places are circles, with tokens inside representing the marking, and transitions are rectangles with static firing intervals below. The packs are represented with dashed frames (in red).

*Example 1.* An example of WS-TPN is represented in figure 1.

<figure><img src="image_2.png" /><figcaption>Fig. 1: The WS-TPN $N_1$ with initial marking $m_0 = (1, 1, 0)$ and packs $\Pi = \{\{t_0, t_1\}, \{t_1, t_2\}, \{t_3\}\}$</figcaption></figure>

## 2.2 Semantics of WS-TPNs

A state of a WS-TPN is a pair $(m, I)$ where $m$ is a marking and $I: T \to \mathbb{I}_{\mathbb{R}_+}$ is a map called *dynamic firing interval* function such that for each enabled transition $t$ in $m$, $I(t)$ denotes the remaining durations to wait before $t$ can fire. An enabled transition $t$ can fire when its dynamic interval contains zero: $0 \in I(t)$.

A transition $t_k$ is newly enabled after firing $t_i$ from marking $m$ if “it is not enabled by $m - \bullet t_i$ and it is enabled by $m' = m - \bullet t_i + t_i \bullet$”. Let $\uparrow \text{enab}(m, t_i)$ be the set of transitions newly enabled by firing $t_i$ from $m$, formally:

$$ \uparrow \text{enab}(m, t_i) = \{t_k \mid t_k \in \text{enab}(m - \bullet t_i + t_i \bullet) \\ \text{and } (t_k \notin \text{enab}(m - \bullet t_i) \text{ or } t_k = t_i)\} $$

We say that a transition is *awake* in a state $(m, I)$, if it is enabled by $m$ and can be fired immediately or in the future i.e. it has been enabled for less than
its upper bound ($I(t) \neq \emptyset$). Then a pack $\pi \in \Pi$ is awake in a state $(m, I)$ if at least one transition $t$ of $\pi$ is awake.

**Definition 4 (Awake transitions and packs in a state).** Let $(m, I)$ be a state. The set of awake transitions in $(m, I)$ is $\mathit{awake}((m, I)) = \{t \in T \mid t \in \mathit{enab}(m) \text{ and } I(t) \neq \emptyset\}$. The set of awake packs in $(m, I)$ is $\pi$-awake((m, I)) = \{\pi \in \Pi \mid \exists t \in \mathit{awake}((m, I)) \cap \pi\}$.

In WS-TPNs, a pack that is awake in a given state should remain awake by elapsing time.

We need the definition of a timed transition system to define the semantics of WS-TPNs.

**Definition 5 (Timed Transition System).** A Timed Transition System (TTS) over the set of actions $\Sigma$ is a tuple $S = (Q, q_0, \Sigma, \rightarrow)$ where $Q$ is a set of states, $q_0 \in Q$ is the initial state, $\Sigma$ is a finite set of actions disjoint from $\mathbb{R}_+$, $\rightarrow \subseteq Q \times (\Sigma \cup \mathbb{R}_+) \times Q$ is a set of edges. If $(q, e, q') \in \rightarrow$, we also write $q \xrightarrow{e} q'$.

We now give the definition of the semantics of WS-TPNs.

**Definition 6 (Semantics of WS-TPN).** The semantics of a WS-TPN $N = (P, T, F, m_0, I_s, \Pi)$ is a timed transition system $S_N = (Q, q_0, T, \rightarrow)$ where: $Q = (\mathbb{N})^P \times (\mathbb{I}_{\mathbb{R}_+})^T$, $q_0 = (m_0, I_s)$, $\rightarrow \in Q \times (T \cup \mathbb{R}_+) \times Q$ consists of the discrete and continuous transition relations:

- the discrete transition relation is defined for all $t_i \in T$ by $(m, I) \xrightarrow{t_i} (m', I')$ iff:

$$ \left\{ \begin{array}{l} t_i \in \mathit{enab}(m) \quad \text{and} \quad m' = m - \bullet t_i + t_i \\ 0 \in I(t_i) \\ \forall t_k \in T, I'(t_k) = \begin{cases} I_s(t_k) & \text{if } t_k \in \uparrow \mathit{enab}(m, t_i) \\ I(t_k) & \text{otherwise.} \end{cases} \end{array} \right. $$

- the continuous transition relation is defined for all $d \in \mathbb{R}_+$ by $(m, I) \xrightarrow{d} (m, I')$ iff:

$$ \left\{ \begin{array}{l} \forall t_k \in \mathit{enab}(m), I'(t_k) = I(t_k) - d \\ \pi\text{-awake}((m, I)) = \pi\text{-awake}((m, I')) \end{array} \right. $$

A run of $N$ is a possibly infinite sequence $q_0 a_1 q_1 a_2 q_2 \dots$ such that $\forall i > 0$, $q_i \in Q$, $a_i \in (T \cup \mathbb{R}_+)$ and $q_{i-1} \xrightarrow{a_i} q_i$. We note $q \xrightarrow{t@d} q'$ for the sequence elapsing $d \in \mathbb{R}_+$ followed by the firing of $t$ from $q$: $q \xrightarrow{d} q_d \xrightarrow{t} q'$. We write $q \xrightarrow{t} q'$ if there exists $d \in \mathbb{R}_+$ such that $q \xrightarrow{t@d} q'$.

**Example 2.** Three runs of $N_1$ (from Figure 1) are represented in Figure 2: $q_0 \xrightarrow{t_0@d_0} q_1 \xrightarrow{t_2@d_1} q_2 \xrightarrow{t_3@d_1} q_3$, $q_0 \xrightarrow{t_0@1.3} q_5 \xrightarrow{t_3@d_2} q_6$ and $q_0 \xrightarrow{t_1@2.5} q_4$. In the first one $t_0$ fires before $t_2$. In the second one, $t_2$ falls asleep at time 1 then $t_0$ fires at time 1.3. In the third, $t_2$ and $t_0$ fall asleep at time 1 and 2 (resp.), then $t_1$ fires at time 2.5.
<figure><img src="image_3.png" /><figcaption>Fig. 2: Some runs of $N_1$ (from figure 1). The vectors *m* and *I* are represented in order of index of the places and the transitions (resp.). The dynamic intervals of disabled/asleep transitions are greyed out.</figcaption></figure>

## 2.3 Particular structures of packs

In [8], a weakly-strong semantics on time Petri nets based on structural properties of the net (conflicts and bundles, which are extended conflicts) was presented. The framework of WS-TPN generalizes this notion to any possible packs, and therefore can be used to model these properties.

**Weak and Strong semantics** This framework is able to express both the weak semantics and the strong semantics over TPNs. Let $N = \langle P, T, F, m_0, I_s, \Pi \rangle$ be a WS-TPN, and $N' = \langle P, T, F, m_0, I_s \rangle$ its corresponding TPN.

If $N$ has no packs ($\Pi = \emptyset$), then there are necessarily no awake packs in all the states. Therefore, the condition in the semantics to elapse time is always true, which is equivalent to the weak semantics on $N'$.

If the packs of $N$ are all the singletons of the power set of $T$ ($\Pi = \bigcup_{t \in T} \{{t}\}$), then the awake packs in one state are exactly the ones with an enabled transition. Thus, it is possible to elapse time only if no transition falls asleep by doing so. This exactly expresses the strong semantics on $N'$.

## 2.4 Weak TPN with read, reset and transfer arcs

We conclude this section by introducing the classical read, reset, and transfer arcs. For simplicity we add them to TPNs and not to WS-TPNs as the following undecidability results using those arcs need only the weak semantics of TPNs. It would be straightforward to adapt this definition to WS-TPNs.

Reset arcs extend Petri Nets with the possibility of emptying places regardless of their previous contents. Transfer arcs allow to transfer the whole contents of some place to some other one. These arcs increase expressive power of Petri Nets making reachability undecidable [1, 6]. Read arcs describe reading without
consuming [13]. In the untimed setting, ignoring the issue of true concurrency,
they do not increase expressive power of Petri Nets and reachability problem
remains decidable.

**Definition 7 (Read, Reset and Transfer nets).** *A Petri net with read, reset and transfer arcs is a tuple $N = (P, T, F, F_r, m_0)$ where*

- $P$ is a finite set of places,

- $T$ is a finite set of transitions

- $m_0$ is the initial marking

- $F: (P \times T) \cup (T \times P) \to \mathbb{N} \cup P$ is a flow function where $F(x, y) = p$ with $p \in P$ means that $F(x, y)$ is equal to the number of tokens in place $p$. Moreover, $\forall (p, t, p') \in (P \times T \times P), \text{ we have :}$

- if $F(p, t) = p'$ then $p = p'$

- if $F(t, p') = p$, then $F(p, t) = p$ and we say that $(p, p')$ is a transfer arc

- if $F(p, t) = p$ and $\not\exists p'' \in P$ with $F(t, p'') = p$ then $(p, t)$ is a reset arc

- $F_r: (P \times T) \to \mathbb{N}$ is the read function

Reset and transfer arcs are not involved in the enabling of a transition since when $F(p,t) \notin \mathbb{N}$ then $F(p,t)$ is equal to the number of tokens in place $p$ whatever that number may be, including zero. On the other hand, read arcs are involved in the enabling of transitions. For all $t \in T$ we denote by $^{\circ}t$, the reading vector in $\mathbb{N}^{|P|}$ s.t. $\forall p \in P, ^{\circ}t(p) = F_r(p,t)$.

Moreover for a marking $m$, we have $\bullet t(p) = m(p)$ when $F(p,t) = p \in P$ and $\bullet t(p) = F(p,t)$ otherwise, and $t^\bullet(p') = m(p)$ when $F(t,p') = p \in P$ and $t^\bullet(p') = F(t,p')$ otherwise.

- Transition $t$ is enabled by $m$ if each input place $p$ of $t$ is marked with at least $F(p,t)$ and $F_r(p,t)$ tokens i.e. $m \ge \bullet t + \circ t$

- An enabled transition $t \in T$ can fire leading to a new marking $m' = m - \bullet t + t^\bullet$.

3 Undecidability Results

**Definition 8 (Problems).** Let $N = (P, T, F, m_0)$ a Petri net and reach($N$) the set of reachable markings.

- The marking reachability problem: given $m \in \mathbb{N}^P$, does $m \in \text{reach}(N)$ ?

- The marking coverability problem: given $m \in \mathbb{N}^P$, does there exist $m' \in \mathbb{N}^P$ such that $m' \ge m$ and $m' \in \text{reach}(N)$ ?

- The boundedness problem: does there exist $b \in \mathbb{N}$ such that for all $m \in \text{reach}(N)$ and for all $p \in P$, $m(p) \le b$ ?

These definitions extend to the other classes of Petri nets that we study in
this section, and in particular to TPN.
## 3.1 Reachability and coverability problems for WS-TPN

The marking reachability, the marking coverability and the boundedness problems are decidable for TPN with weak semantics [12].

We show that the halting problem for 2-counter machines can be reduced to the reachability problem of weakly-strong TPN, with only one transition in strong semantics.

**Definition 9 (2-counter Machine).** A deterministic 2-counter machine is a tuple $(c_1, c_2, L, I)$ where:

- $c_1$ and $c_2$ are counters with non-negative integer values;

- $L$ is a finite set of lines including an initial state `init` and a halting state `halt`;

- $I$ is a finite set of instructions of the form `(l, c, l')` or `(l, c, l', l'')` with $c \in \{c_1, c_2\}$, representing respectively increment (we write also `inc(l, c, l')` for readability) and conditional decrement (`jzdec(l, c, l', l'`) instructions.

Calling `l` the source line of the instruction in both cases, there can be at most one instruction in `I` for any given source line (be it an `inc` or a `jzdec`).

**Definition 10 (Configuration of a 2-counter machine).** A configuration of a 2-counter machine $(c_1, c_2, L, I)$ is a tuple $(v_1, v_2, s)$ with $v_1, v_2 \in \mathbb{N}$, and $l \in L$. The machine can go from configuration $(v_1, v_2, l)$ to configuration $(v'_1, v'_2, l')$ if and only if:

- either there exists an instruction `inc(l, c_i, l')` such that $v'_i = v_i + 1$ and $v'_{3-i} = v_{3-i}$

- or there exists an instruction `jzdec(l, c_i, l_z, l_{nz})` such that either $l' = l_{nz}$, $v_i > 0$, $v'_i = v_i - 1$ and $v'_{3-i} = v_{3-i}$, or $l' = l_z$, $v_i = 0$, $v'_i = v_i$ and $v'_{3-i} = v_{3-i}$.

**Theorem 1 (Undecidability of the halting problem [10]).** The problem of knowing whether a deterministic 2-counter machine can go from configuration $(0, 0, init)$ to some configuration $(v_1, v_2, halt)$, with $v_1, v_2 \in \mathbb{N}$, is undecidable.

First recall that for TPNs with strong semantics, coverability is undecidable [7]. This result is obtained by reduction from the halting problem for 2-counter machines, with a TPN widget encoding increments (figure 3a) and one encoding conditional decrement (figure 3b).

We have one place for each counter, where the counter value is given by the number of tokens in the place, and one place for each line. By abusing the notations, we use the same names for those corresponding objects in the machine and in the TPN. Then the following lemma holds:

**Lemma 1 ([7]).** The place `halt` can be marked in the TPN obtained by assembling the widget for all the instructions if and only if the 2-counter machine halts.

*Proof.* The increment widget is quite straightforward. The conditional decrement works by using time to ensure a priority of transition $nz_j$ over transition $z_j$. □
Now assume those widgets are TPNs with weak semantics. The increment widget still works as intended: if the machine halts we can still traverse the widget and increment the number of tokens in $c_i$ and if the machine does not halt, the only new behaviors are those in which the $inc_j$ transition falls asleep, but then, since the machine is deterministic that transition will never become newly enabled again and the whole net is blocked.

The situation is, as expected (since coverability is decidable), not the same for the `jzdec` instruction as now nothing prevents the net from firing the $z_j$ transition even when $c_i$ is marked, simply by letting $nz_j$ fall asleep.

<figure><img src="image_4.png" /><figcaption>Fig. 3: Instructions `inc` and `jzdec` as a TPN with strong semantics and WS-TPN. The places in blue ($c_i$) are shared between all the instructions.</figcaption></figure>

Actually only the $nz_j$ transition needs to have strong semantics, so the WS-TPN in figure 3c faithfully models the conditional decrement instruction.

**Lemma 2.** *The place halt can be marked in the WS-TPN obtained by assembling the widgets in fig. 3a (treated as WS-TPN) for all inc instructions and the widgets in fig. 3c for all jzdec instructions if and only if the 2-counter machine halts.*

*Proof.* If the machine halts then by correctness of the construction of [7], there is an execution in the WS-TPN that marks place halt.

If the machine does not halt, either no transition falls asleep, and the resulting execution would be an execution of the same net with strong semantics, and then by correctness of the construction of [7] that execution does not mark halt. Or there is exists a transition that falls asleep in one of the widget. Since $nz_j$ is alone in its pack, it cannot fall asleep and there remains only two cases:
1. if that transition is an $inc_j$ transition in a $inc$ widget, as explained before, since the machine is deterministic the token enabling that transition (in the $l_j$ place) can never be removed and the transition will stay asleep forever, blocking the execution that therefore cannot mark halt.

2. if it is a $z_j$ transition in a $jzdec$ widget, then it must be the case that $c_i$ is empty otherwise $nz_j$ would have fired before $z_j$ could fall asleep. Then $nz_j$ can never fire, and for the same reasons as in the previous case the execution is blocked without reaching halt. □

With this construction, we have as many transitions with strong semantics as there are $jzdec$ instructions in the machine. We now show how this can be reduced to only one such transition.

Consider the new version of the $jzdec$ widget as a WS-TPN shown in figure 4. The idea is to share the zero-test both between $jzdec$ instruction on a given counter, and between the two counters. For the former, we decouple the shared widget and the control flow: when in line $l_j$, to do a $jzdec$, we send a token to shared place $p_{test}$ and wait on transitions $jump_k$ and $jump_l$. The shared zero-test proceeds as before and a token arrives either in $p_z$ if the tested counter is zero or in $p_{nz}$ if it is not. In the former case, $jump_k$ becomes enabled and can fire and mark $l_k$, and in the latter case $l_l$ will become marked (unless, as always transitions fall asleep), as expected. Note that when $p_z$ is marked, only $jump_k$ is possible, and none of the other $jump_{k'}$, because only place $p_{test_j}$ is marked and none of the other $p_{test_{j'}}$. The same holds symmetrically for $p_{nz}$ and $jump_l$.

To share the widget between counters, we actually ask for both places $c_1$ and $c_2$ to be non-zero to mark $p_{nz}$, but we add one token in the counter that is not involved in the instruction before the test, so that it is for sure non-zero. That token will be removed when exiting either by $jump_k$ or $jump_l$. In that way, either the tested counter, say $c_1$, is non-zero. Then by construction so is $c_2$ and $nz$ fires before $z$ because of the strong semantics. Or $c_1$ is zero, then $nz$ cannot fire, and $z$ will eventually fire (if it does not fall asleep). The test therefore works as expected.

With these modification the usual lemma holds, and in addition the obtained WS-TPN has only a single pack, which contains a single transition, i. e., there is a single transition with strong semantics in the whole net.

**Lemma 3.** *The place halt can be marked in the WS-TPN obtained by assembling the widgets in fig. 3a (treated as WS-TPN) for all inc instructions and the widgets in fig. 4 for all jzdec instructions if and only if the 2-counter machine halts.*

*Proof.* With the above explanations, it is clear that if the machine halts, there is an execution in the net that mimics the execution of the machine and eventually marks the place halt.

When the machine does not halt, we just need to make sure that we have not added spurious executions that would still mark place halt. As we have seen above, when no transition ever falls asleep, the zero-test and then the $jzdec$ instruction, are mimicked correctly. In both the zero and non-zero case, there is only a single possible execution that marks respectively $l_k$ or $l_l$ as expected.
<figure><img src="image_5.png" /><figcaption>Fig. 4: Instructions `jzdec(l_j, c_1, l_k, l_l)` and `jzdec(l'_j, c_2, l'_k, l'_l)` as a WS-TPN with packs $\Pi = \{{\color{blue}nz}\}$. All the instructions `jzdec` share the blue part of the widget (`\{c_1, c_2, p_{test}, p_{nz}, p_z, nz, z\}`).</figcaption></figure>

If some transition falls asleep, we have additional cases: transitions $test_j$, $jump_k$, and $jump_l$.

- if transition $test_j$ falls asleep, as before, because of the determinism of the machine the token will stay in $l_j$ forever and the WS-TPN is just blocked, and place `halt` is not marked;

- if transition $jump_k$ falls asleep (assuming the counter was zero), then place $l_k$ will not become marked and the widget for the next instruction cannot execute so there is no way that place $p_z$ is ever emptied by another instruction widget, and thus the WS-TPN is blocked without ever marking place `halt`;

- if transition $jump_l$ falls asleep, the case is symmetrical the $jump_k$ case. $\square$

It follows that:

**Theorem 2.** *The marking coverability problem is undecidable for WS-TPNs with a single pack, which contains a single transition.*

In general, coverability is weaker than reachability. Indeed suppose one wants to test if a marking $m$ is coverable using reachability, one can just add a transition with for all places $p$ an input arc with weight $m(p)$ and an output arc to some
common witness place. Also add for all places an additional transition with just an input arc to that place. Finally, ask if the marking with only one token in the witness place and none in the others is reachable.

**Corollary 1.** The marking reachability problem is undecidable for WS-TPNs with a single pack, which contains a single transition.

**Lemma 4.** The WS-TPN obtained with the same construction as lemma 3 and by adding a place and arcs going from all the transitions of the net to that place is bounded if and only if the 2-counter machine halts.

*Proof.* The added place (called $p_c$) simply counts the number of transitions fired during the execution. The proof is similar to the previous one:

- If the machine halts, then in all possible executions of the net the counters and the place $p_c$ are bounded. All the others places are either empty or contain one token (if we reached a deadlock).

- If the machine does not halt, then there is (at least one) infinite execution of the net. Therefore the marking of $p_c$ is not bounded.

It follows that:

**Theorem 3.** The boundedness problem is undecidable for WS-TPNs with a single pack, which contains a single transition.

**Corollary 2.** The marking coverability, the marking reachability and the boundedness problems are undecidable for TPNs with weak semantics augmented with a single transition with strong semantics.

## 3.2 Coverability problem for weak TPN with read, reset or transfer arcs

In the untimed setting, reachability, coverability and boundedness problems are decidable for Petri Nets with read arcs. For reset and transfer nets, reachability is undecidable [1] and coverability is decidable but boundedness is decidable for transfer nets but not for reset nets [6].

We propose to study the decidability impact on these arcs on TPNs under weak semantics. Like in the previous section, we reduce the halting problem for 2-counter machine to the marking coverability problem for TPN with read, reset and transfer arcs.

The widget encoding inc instruction has been given in the previous section (figure 3a), then we focus on the jzdec instruction.

**Read** The encoding is given in figure 5. The encoding is based on the transition ion (note that i.o.n. means immediately or never) whose time interval is [0, 0] and which can either fire immediately after being enabled or never fire at all if it falls asleep.
**Lemma 5.** The place halt can be marked in the weak TPN obtained by assembl ing the widgets in fig. 3a for all inc instructions and the widgets in fig. 5 for all jzdec(., cᵢ, .., ..) instructions if and only if the 2-counter machine halts.

*Proof.* We start with a marking *m* where, apart from *c*ᵢ, *l*ⱼ is the only marked place with *m*(*l*ⱼ) = 1.

Assume the value of $c_i$ is equal to 0 (then $m(c_i) = 0$). The net can only fire the sequence of transitions $test_j$.one.ion.z reaching a marking where the only marked place is $l_k$ and the place $c_i$ remains empty.

Assume now that the value of $c_i$ is greater than 0 (i.e. $m(c_1) \ge 1$). $test_j$ is the only firable transition, then it fires and both transitions *one* and *ion* are enabled.

- If ion fires, the place ongoing becomes empty and the transition one is no more firable because of the read arc. We reach a deadlock.

- If we elapse 1 time unit, ion falls asleep and one can fire. Now, the only transition which can be fired is nz leading to a marking $m'$ where (apart from $c_1$) the only marked place is $l_l$ and the value of the counter is now $m'(c_i) = m(c_i) + 1 - 2 = m(c_i) - 1$.

If any other transition than ion falls asleep, the net reaches a deadlock.

Therefore, if the machine halts, there is an execution of the net that mimics the execution of the machine and eventually marks the place halt. If the machine does not halt, either the net mimics the execution of the machine or it reaches a deadlock, but in no case it marks the place halt. □

<figure><img src="image_6.png" /><figcaption>Fig. 5: The jzdec($l_j$, $c_1$, $l_k$, $l_l$) for weak TPN with one read arc: $F_r(ongoing, one) = 1$. All the instructions jzdec(., cᵢ, .., ..) share the blue part of the widget ($\{c_i, p_{test}, ongoing, afterOneTU, p_{ion}, p_{nz}, p_z, one, ion, nz, z\}$).</figcaption></figure>
**Reset** The encoding is given in figure 6. As for the read arc, the idea is to fire the transition ion (i.e. immediately or never) only when the counter is zero and after the firing of one. This time, when the counter is non-zero, the immediate firing of ion will lead to a deadlock, and its firing after 1 time unit must be made impossible. The transition ion must therefore remain continuously enabled after the firing of test<sub>j</sub> and must not be newly enabled by the firing of one. To do this, test<sub>j</sub> produces 2 tokens in ongoing.

**Lemma 6.** The place halt can be marked in the weak TPN obtained by assembling the widgets in fig. 3a for all inc instructions and the widgets in fig. 6 for all jzdec(., c<sub>i</sub>, ..) instructions if and only if the 2-counter machine halts.

*Proof.* We start with a marking *m* where, apart from *c*<sub>*i*</sub>, *l*<sub>*j*</sub> is the only marked place with *m*(*l*<sub>*j*</sub>) = 1.

Assume the value of $c_i$ is equal to 0 (then $m(c_i) = 0$). The net can only fire the sequence of transitions $test_j$, $one$, $ion$, $z$ reaching a marking where the only marked place is $l_k$ and the place $c_i$ remains empty.

Assume now that the value of $c_i$ is greater than 0 (i.e. $m(c_i) \ge 1$). $test_j$ is the only firable transition, then it fires and both transitions one and ion are enabled.

- If ion fires, it remains a token in the place ongoing and the place noMoreThanOnce has been reset by the reset arc. Then, the transition one is disabled. We are either in a deadlock if $c_i$ is empty, or we can fire again the transition ion and we reach a deadlock.

- If we elapse 1 time unit after the firing of $test_j$, ion falls asleep and we can fire the transition one. Since there are 2 tokens in ongoing, the transition ion is not newly enabled by the firing of one and thus stays asleep. Now, the only transition which can fire is *nz* removing the 2 tokens of ongoing and leading to a marking $m'$ where (apart from $c_i$) the only marked place is $l_i$. The value of the counter is now $m'(c_i) = m(c_i) + 1 - 2 = m(c_i) - 1$.

As in the proof of Lemma 5, if any other transition than ion falls asleep, the net reaches a deadlock. □

**Transfer** The model is the same as for the reset arc but we add a place garbage and we replace the reset arc by a transfer arc from noMoreThanOnce to garbage as follows:

- $F(\text{noMoreThanOnce}, \text{ion}) = \text{noMoreThanOnce}$

- $F(\text{ion}, \text{garbage}) = \text{noMoreThanOnce}$

**Lemma 7.** The place halt can be marked in the weak TPN obtained by assembling the widgets in fig. 3a for all inc instructions and the widgets in fig. 6 with the transfer arc described previously for all jzdec(., c<sub>i</sub>, ..) instructions if and only if the 2-counter machine halts.
<figure><img src="image_7.png" /><figcaption>Fig. 6: The $jzdec(l_j, c_i, l_k, l_l)$ for weak TPN with one reset arc (noMoreThanOnce, ion). All the instructions $jzdec(., c_i, ..)$ share the blue part of the widget $(\{c_i, p_{test}, noMoreThanOnce, ongoing, afterOneTU, p_{ion}, p_{nz}, p_z, one, ion, nz, z\})$.</figcaption></figure>

*Proof.* The proof is similar than the one of lemma 6. The tokens will accumulate in the *garbage* place each time the instruction is executed. This is not a problem since we are interested in the coverability of places *l*.

**Theorem 4.** *The marking coverability, the marking reachability and the boundedness problems are undecidable for the following classes of TPN in weak semantics:*

- TPN with 2 read arcs

- TPN with 2 reset arcs

- TPN with 2 transfer arcs

*Proof.* The widgets used in lemmas 5, 6 and 7 require one special arc for all the instructions $jzdec(., c_i, ..)$. Then we need 2 special arcs, one per counter.

To get back to a marking reachability or a boundedness problem one can use the same tricks as in the section 3.1. □

# 4 State Class Graph

As always with continuous time, the models have an infinity of states. Therefore we propose a new symbolic representation of the states space of WS-TPNs based on classes $[3, 2]$. This representation is finite for bounded nets.

The idea is to group all the states that can be reached by a sequence of transitions $\sigma = t_1...t_n \in T^*$ from the initial state $q_0$. We propose here an algorithm to compute these sets $\{q \in Q \mid q_0 \overset{t_1}{\longrightarrow} q_1 ... \overset{t_n}{\longrightarrow} q\}$ called state classes.
## 4.1 Firing and sleeping domain and state classes

Classically a *firing time* is a variable associated with each enabled transition of the net. For WS-TPNs, we have to consider the set $W = \{t_1, \dots, t_k\}$ of awake transitions. A firing time $\theta_i$ is associated with each $t_i \in W$, and is compacted in a vector notation $\boldsymbol{\theta} = (\theta_1, \dots, \theta_k) \in (\mathbb{R}_+)^W$. Additionally, a *sleeping time* is associated with each awake transition that may fall asleep. Let $W_s = \{t_i \in W \mid \overline{I_s}(t_i) \neq +\infty\}$. A sleeping time $\lambda_i$ is associated with each $t_i \in W_s$, and is compacted in a vector notation $\boldsymbol{\lambda} = (\lambda_1, \dots, \lambda_{k'}) \in (\mathbb{R}_+)^{W_s}$.

A *firing and sleeping domain* $D$ is a set of firing and sleeping times $(\boldsymbol{\theta}, \boldsymbol{\lambda})$. It is a convex polyhedron of $(\mathbb{R}_+)^{|W|+|W_s|}$ described by a system of linear inequalities. These inequalities are of two types: rectangular $v_i \sim c$ and diagonal $v_i - v_j \sim c$, $v_i = \theta_i$ or $v_i = \lambda_i$, $\sim \in \{\le, \ge, <, >\}$ and $c \in \mathbb{N}$. For the sake of simplicity, we use the same index for the variables $\theta_i$ and $\lambda_i$ and the awake transitions $t_i$. A domain is empty $D = \emptyset$ when there is no solution to the system of linear inequalities.

**Definition 11 (State class).** A state class is a tuple $K = (m, W, D)$, where $m$ is a marking, $W \subseteq T$ is a set of awake transitions, $W_s = \{t_i \in W \mid \overline{I_s}(t_i) \neq +\infty\}$ and $D \subseteq (\mathbb{R}_+)^{|W|+|W_s|}$ is a firing and sleeping domain.

Let $q = (m, I)$ be a state of the net. The dynamic interval function $I$ can be seen, like a firing domain, as a polyhedron of $(\mathbb{R}_+)^T$. We denote $I|_A$ the restriction of $I$ to $A \subseteq T$. We say that a state belongs to a state class if its dynamic interval function is included in the firing domain, and the supremum of its dynamic interval function is in the sleeping domain.

**Definition 12 (Membership of states in a class).** Let a state class $K = (m, W, D)$ and a state $q = (m', I)$. We say $q \in K$ iff $m = m'$, *awake*($q$) = $W$ and $\forall \boldsymbol{\theta} \in I|_W, \exists (\boldsymbol{\theta}, \boldsymbol{\lambda}) \in D$ s.t. $\forall t_i \in W_s, \lambda_i = \overline{I}(t_i)$.

## 4.2 Construction of the State Class Graph

In contrast to simple TPNs, for WS-TPNs we have to consider two types of events: firing a transition $t \in T$ and putting a set of transitions $S \subseteq T$ to sleep, i.e. exceeding their firing intervals, which will be denoted $\hat{S}$. The set of actions consisting of putting a transition to sleep is denoted $\hat{T} = \{\hat{S} \mid S \subseteq T\}$.

The State Class Graph (SCG) of a WS-TPN $N = (P, T, F, m_0, I_s, \Pi)$ is the set of classes $(K_\sigma)_{\sigma \in (T \cup \hat{T})^*}$ obtained as follows:

- The initial class is $K_\epsilon = (m_0, W_0, D_0)$, where $W_0 = \text{awake}((m_0, I_s))$ and $D_0$ is the domain s.t. $\forall (\boldsymbol{\theta}, \boldsymbol{\lambda}) \in D_0, \forall t_i \in W_0, \theta_i \in I_s(t_i)$ and if $\overline{I_s}(t_i) \neq +\infty, \lambda_i = \overline{I_s}(t_i)$.

- If the sequence $\sigma$ is feasible, i. e., we can find delays so that transitions in $\sigma$ fire in order with those delays putting the corresponding transitions in $\sigma$ to sleep, and $K_\sigma = (m, W, D)$, then we have to check if $t_f \in W$ can fire and what set of transitions can fall sleep before that. Let $W_s = \{t_i \in W \mid \overline{I_s}(t_i) \neq +\infty\}$, and let $S \subseteq W_s$.
S can fall asleep and $t_f$ can fire after that iff

$$ \left\{ \begin{array}{l} D \wedge \bigwedge_{t_i \in S} \{\theta_f \succ_i \lambda_i\} \wedge \bigwedge_{\substack{t_i \in W \\ t_i \neq t_f}} \{\theta_i \geq \theta_f\} \neq \emptyset \\ \forall \pi \in \Pi, \pi \cap W \neq \emptyset \iff \pi \cap (W \setminus S) \neq \emptyset \end{array} \right. $$

where $\succ_i=$> if $D \wedge \{\theta_i = \lambda_i\} \neq \emptyset$ and $\succ_i=$> otherwise.

- If S can fall asleep and $t_f$ can fire after that, then the sequence $\sigma.\hat{S}.t_f$ is feasible, then $K_{\sigma, \hat{S}, t_f} = \langle m', W', D' \rangle$ is computed from $K_{\sigma} = \langle m, W, D \rangle$:

• $m' = m - \bullet t_f + t_f \bullet$

• $W' = ((W \setminus S) \cap \text{enab}(m')) \cup (\uparrow \text{enab}(m, t_f))$

• Let $W'_s = \{t_i \in W' | \overline{I_s(t_i)} \neq +\infty\}$. $D'$ is described by inequalities over variables $\theta'_i$ (resp. $\lambda'_i$) added for all $t_i \in W'$ (resp. $t_i \in W'_s$). Formally, $\forall (\theta', \lambda') \in D'$, $\exists (\theta, \lambda) \in D$ s.t.:

$$ \left\{ \begin{array}{l} \forall t_i \in W' \cap (\uparrow \text{enab}(m, t_f)), \theta'_i \in I_s(t_i) \\ \forall t_i \in W' \setminus (\uparrow \text{enab}(m, t_f)), \theta'_i \geq 0 \text{ and } \theta'_i = \theta_i - \theta_f \\ \forall t_i \in W'_s \cap (\uparrow \text{enab}(m, t_f)), \lambda'_i = \overline{I_s(t_i)} \\ \forall t_i \in W'_s \setminus (\uparrow \text{enab}(m, t_f)), \lambda'_i \geq 0 \text{ and } \lambda'_i = \lambda_i - \theta_f \end{array} \right. $$

The construction of SCG is also valid for nets with reset, read and transfer arcs. Since they only affect the discrete behaviour, we just need to adapt the firing of transitions by following the semantics.

**Remark 1.** It is important to explicitly put transitions to sleep in the SCG. Otherwise it does not capture all the possible discrete executions of the net. It may happen that a transition $t_s$ can fall asleep in a class but cannot do it after firing another transition $t_f$. Indeed, firing $t_f$ may disable all the others transitions in the pack of $t_s$ thus forbidding it to fall asleep.

In a real implementation of the algorithm constructing the SCG, the computation of the new domain $D'$ after firing and putting transitions to sleep is done by adding the new variables $(\theta', \lambda')$ and constraints to $D$ (by conjunction), and by eliminating the variables $(\theta, \lambda)$ with Fourier-Motzkin.

**Example 3.** The state class graph of $N_1$ (from figure 1) is represented in the figure 7.

## 4.3 Properties of the SCG

To construct the state class graph, as in [3, 2], we just build the potentially infinite tree of state classes for all possible sequences $\sigma$ and merge on-the-fly classes with the same marking, same awake transitions and same solutions to their firing and sleeping domains. For a bounded net, this procedure terminates:

**Proposition 1.** Let N be a bounded WS-TPN, then its State Class Graph is finite.
<figure><img src="image_8.png" /><figcaption>Fig. 7: SCG of $N_1$ (from figure 1).</figcaption></figure>

*Proof.* Compared to the construction of Berthomieu [3, 2], the main difference is the addition of the $\lambda$ variables. The same arguments as for the classical state class graph, then ensure that there can only be a finite number of state classes.

Let $\sigma \in (T \cup \hat{T})^*$ be a sequence of actions, namely firing and putting transitions to sleep. We note $\tilde{\sigma} \in T^*$ the sequence of actions derived from $\sigma$ where only the firings remain. Formally, if $\sigma = \hat{S}_1 t_1 \hat{S}_2 t_2 \dots \hat{S}_n t_n$ then $\tilde{\sigma} = t_1 \dots t_n$.

**Proposition 2.** Let a WS-TPN $N = \langle P, T, F, m_0, I_s, \Pi \rangle$, its initial state $q_0 = (m_0, I_s)$ and its SCG $(K_\sigma)_{\sigma \in (T \cup \hat{T})^*}$. Let $\tau = t_1 \dots t_n \in T^*$ and $q \in Q$. There exists $q_1, \dots, q_{n-1} \in Q$ s.t. $q_0 \xrightarrow{t_1} q_1 \dots \xrightarrow{t_{n-1}} q_{n-1} \xrightarrow{t_n} q$ iff there exists $\sigma \in (T \cup \hat{T})^*$ s.t. $\tilde{\sigma} = \tau$, $K_\sigma$ is in the SCG and $q \in K_\sigma$.

*Proof.* Let $H(n)$ be the induction hypothesis that the lemma holds for all sequences $\tau$ of size $n \ge 0$.

The initial case $H(0)$ is simply $q_0 \in K_\epsilon$, which is straightforward.

Let $n \ge 0$, we suppose $H(n)$ and prove $H(n+1)$. Let $\tau = t_1 \dots t_n \in T^*$, $t_{n+1} \in T$ and $q \in Q$.

⇒ We suppose that there exists $q_1, \dots, q_n \in Q$ s.t. $q_0 \xrightarrow{t_1} q_1 \dots \xrightarrow{t_n} q_n \xrightarrow{t_{n+1}} q$. From $H(n)$ we know that there exists $\sigma \in (T \cup \hat{T})^*$ s.t. $\tilde{\sigma} = \tau$, $K_\sigma = \langle m, W, D \rangle$ is in the SCG and $q_n = (m, I) \in K_\sigma$.

By definition, there exists $d \in \mathbb{R}_+$ s.t. $q_n \xrightarrow{d} q' \xrightarrow{t_{n+1}} q_{n+1}$. Let $S = \text{awake}(q_n) \setminus \text{awake}(q')$ be the set of transitions that fall asleep by elapsing $d$ from $q_n$. Let $t_f = t_{n+1}$. We first prove that $\sigma.\hat{S}.t_f$ is feasible in the SCG.
Let $t_i \in S$. First, for all $\theta_i \in I(t_i)$, $\theta_i < d$. Thus, $\overline{I(t_i)} < d$ if $\text{cl}(\downarrow I(t_i)) = \downarrow I(t_i)$ and $\overline{I(t_i)} \le d$ otherwise. Then, there exists $\boldsymbol{\theta} \in I|_W$ s.t. $d \le \theta_f$. Moreover, since $q_n \in K_\sigma$, $\exists(\boldsymbol{\theta}, \boldsymbol{\lambda}) \in D$ s.t. $\lambda_i = \overline{I(t_i)}$. Therefore $\lambda_i < \theta_f$ if $D \wedge \{\theta_i = \lambda_i\} \ne \emptyset$ and $\lambda_i \le \theta_f$ otherwise.

Let $t_i \in W \setminus (S \cup \{t_f\})$. First, there exists $\theta'_i \in I(t_i)$ s.t. $d \le \theta'_i$. Moreover, since $0 \in I(t_f) - d$, there exists $\theta'_f \in I(t_f)$ s.t. $\theta'_f \le d$. Therefore, $\exists \boldsymbol{\theta} \in I|_W$ s.t. $\theta_i = \theta'_i$ and $\theta_f = \theta'_f$. Then $\exists(\boldsymbol{\theta}, \boldsymbol{\lambda}) \in D$ s.t. $\theta_f \le \theta_i$.

The condition on the packs follows exactly the semantics, and it then true. Therefore $\sigma.\hat{S}.t_f$ is feasible in the SCG. Let $K_{\sigma.\hat{S}.t_f} = \langle m', W', D' \rangle$. We prove now that $q_{n+1} \in K_{\sigma.\hat{S}.t_f}$.

It is straightforward to show that $q_{n+1} = (m', I')$, for some $I'$, and awake ($q_{n+1}$) = $W'$. Let $\boldsymbol{\theta}' \in I'|_{W'}$. For all $t_i \in W'$, $\theta'_i \in I_s(t_i)$ if $t_i \in \uparrow \text{enab}(m, t_f)$, else $\exists \theta_i \in I(t_i)$ s.t. $\theta'_i = \max(0, \theta_i - d)$. Since $0 \in I(t_f) - d$, it follows that $d \in I(t_f)$. Let $\theta_f = d$, then if $t_i \in \uparrow \text{enab}(m, t_f)$, $\theta'_i = \max(0, \theta_i - \theta_f)$. Since $q_n \in K_\sigma$, $\exists(\boldsymbol{\theta}, \boldsymbol{\lambda}) \in D$ s.t. $\forall t_i \in W_s$, $\lambda_i = \overline{I(t_i)}$. We define $\boldsymbol{\lambda}'$ s.t. $\forall t_i \in W'_s$, $\lambda_i = \overline{I_s(t_i)}$ if $t_i \in \uparrow \text{enab}(m, t_f)$, else $\lambda'_i = \lambda_i - \theta_f = \lambda_i - d = \overline{I'(t_i)}$. Hence $\exists(\boldsymbol{\theta}', \boldsymbol{\lambda}') \in D'$ s.t. $\forall t_j \in W'$, $\lambda_j = \overline{I'(t_j)}$, which terminates to prove that $q_{n+1} \in K_{\sigma.\hat{S}.t_f}$.

We suppose that there exists $\sigma \in (T \cup \hat{T})^*$ s.t. $\tilde{\sigma} = \tau.t_{n+1}$, $K_\sigma$ is in the SCG and $q \in K_\sigma$. Let $\sigma = \sigma_n.\hat{S}.t_{n+1}$ with $\sigma_n = \hat{S}_1 t_1 \dots \hat{S}_n t_n$. It is straightforward to show that $\exists d \in \mathbb{R}_+$, $q_n, q' \in Q$ s.t. $q_n = (m, I) \xrightarrow{d} q' \xrightarrow{t_{n+1}} q_{n+1}$ and $S = \text{awake}(q_n) \setminus \text{awake}(q')$. The predecessor is given by the definition of the domain, and $d$ is one of the possible firing time $\theta_{n+1} \in I(t_{n+1})$. Then $H(n)$ terminates the proof. $\square$

The (discrete) language of a WS-TPN $N$ is the set of sequences that matches runs of the net. It is denoted $\mathcal{L}(N) = \{\sigma = t_1 \dots t_n \mid \exists q_1, \dots, q_n \in Q \text{ and } q_0 \xrightarrow{t_1} q_1 \dots \xrightarrow{t_n} q_n\}$. Similarly the language of a SCG $G = (K_\sigma)_{\sigma \in (T \cup \hat{T})^*}$ is the set of sequences of firing derived from feasible sequences: $\mathcal{L}(G) = \{\sigma \in T^* \mid \exists \sigma' \in (T \cup \hat{T})^* \text{ s.t. } \tilde{\sigma}' = \sigma \text{ and } K_{\sigma'} \text{ exists}\}$.

**Corollary 3.** A WS-TPN and its State Class Graph have the same (discrete) language.

# 5 Conclusion

We have proposed a new class of time Petri nets, called WS-TPNs, that seamlessly integrate both the strong semantics, related to urgency, and the weak semantics of time Petri nets.

Using this class, we prove that while (unbounded) TPNs with weak semantics have nice decidability results (even reachability is decidable), coverability becomes undecidable if we allow even a single transition to behave along the strong semantics.
We complete this negative result by proving that the same holds when adding
instead two read arcs, or two reset arcs, or two transfer arcs, while those arcs
had no such impact on regular Petri nets, and [12] has shown that a TPN with
weak semantics and the corresponding Petri net (obtained by removing time
intervals) have the same set of reachable markings.

We finally show how to construct a finite abstraction of the state space for
bounded WS-TPNs that capture the set of discrete sequences of the net, in a
similar fashion to regular bounded TPNs with strong semantics [3, 2].

Further work include investigating structural restrictions on the use of tran-
sitions following a strong semantics in WS-TPNs, to obtain decidable subclasses.
Similarly we would also find relevant structural sufficient conditions, mostly on
conflicts, that ensure that no transition ever falls asleep.

References

1. Araki, T., Kasami, T.: Some decision problems related to the reachability problem for Petri nets. Theoretical Computer Science 3(1), 85–104 (1976)

2. Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)

3. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time petri nets. In: Proceedings IFIP. pp. 41–46. Elsevier Science Publishers (1983)

4. Boyer, M., Roux, O.H.: On the compared expressiveness of arc, place and transition time Petri nets. Fundamenta Informaticae 88(3), 225–249 (2008)

5. Christensen, S., Hansen, N.D.: Coloured Petri nets extended with place capacities, test arcs and inhibitor arcs. In: Ajmone Marsan, M. (ed.) Application and Theory of Petri Nets 1993. vol. 691, pp. 186–205. Springer Berlin Heidelberg, Berlin, Heidelberg (1993)

6. Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Automata, Languages and Programming (ICALP’98). vol. 1443, pp. 103–115. Springer, Aalborg, Denmark, (1998)

7. Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theoretical Computer Science 4 pp. 277–299 (1977)

8. Komenda, J., Lahaye, S., Parrot, R., Roux, O.H.: Weakly strong semantics of time Petri nets for performance evaluations. IFAC-PapersOnLine 58(1), 66–71 (2024), 17th IFAC Workshop on discrete Event Systems WODES 2024

9. Merlin, P.M.: A study of the recoverability of computing systems. Ph.D. thesis, Dep. of Information and Computer Science, University of California, Irvine (1974)

10. Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA (1967)

11. Montanari, U., Rossi, F.: Contextual nets. Acta Informatica 32(6), 545–596 (Jun 1995)

12. Reynier, P.A., Sangnier, A.: Weak time Petri nets strike back. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009 - Concurrency Theory. vol. 5710, pp. 557–571. Springer (2009)

13. Vogler, W., Semenov, A., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR’98 Concurrency Theory. pp. 501–516. Springer Berlin Heidelberg, Berlin, Heidelberg (1998)