# On the Expressive Power of Transfinite Sequences for Continuous Petri Nets

Stefan Haar, Serge Haddad

► To cite this version:

Stefan Haar, Serge Haddad. On the Expressive Power of Transfinite Sequences for Continuous Petri Nets. PETRI NETS 2024 - 45th International Conference Application and Theory of Petri Nets and Concurrency, Jun 2024, Geneva, Switzerland. pp.109-131, 10.1007/978-3-031-61433-0_6. hal-04514473

HAL Id: hal-04514473

https://inria.hal.science/hal-04514473v1

Submitted on 21 Mar 2024

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 Attribution 4.0 International License
# On the Expressive Power of Transfinite Sequences for Continuous Petri Nets

Stefan Haar, Serge Haddad

Université Paris-Saclay, INRIA and LMF, ENS Paris-Saclay, CNRS
Gif-sur-Yvette, France

**Abstract.** Continuous Petri nets (CPNs) form a model of (uncountably infinite) dynamic systems that has been successfully explored for modelling and theoretical purposes. Here, we focus on the following topic. Let the *mode* of a marking be the set of transitions fireable in the future. Along a firing sequence, the sequence of different modes is non increasing, and forms what we call the *trajectory* of the sequence. The set of achievable trajectories is an important issue, for instance in the study of biological processes. In CPNs, a marking can be reachable by a finite sequence, or lim-reachable by an infinite convergent sequence. The set of trajectories (resp. markings) obtained via lim-reachability (sometimes strictly) includes the set of trajectories (resp. markings) obtained via reachability. Here, we introduce transfinite firing sequences over countable ordinals and establish several results: (1) while trans-reachability is equivalent to lim-reachability, the set of trajectories associated with trans-reachability may be strictly larger than the one associated with lim-reachability; (2) w.r.t. trajectories, transfinite sequences over ordinals smaller than $\omega^2$ are enough; and (3) checking whether a trajectory is achievable is NP-complete.

We then turn to a more difficult problem: the specification, for all transfinite firing sequences, of their achievable *signatures*, i.e. the sequences of markings witnessing the changes of mode along the trajectory. In view of this goal, we define a finite symbolic reachability tree (SRT) that tracks the possible signatures of the system; in the SRT, a set of markings with same mode is associated with each vertex. We establish that, for bounded CPNs, reversibility holds inside the leaves of the SRT (which correspond to the long-run behaviours). This property is also crucial in the application domains that motivate this work, namely regulation, signaling, ecosystems and other biological networks, where all quantities are bounded in mass or energy. Finally, from an algorithmic point of view, we show how to build an effective representation of the SRT in exponential time, even when the CPN is unbounded.

# 1 Introduction

**Petri nets in Life Sciences.** Over the last decades, life sciences have been increasingly benefitting from the increased application of formal methods involving discrete event system models. This is particularly true for boolean and
Thomas networks; but several authors (Heiner et al. [14, 2], Chaouia et al. [4–6], and others) have successfully used and studied (discrete) Petri nets, specifically in systems biology for the modelling of metabolism, cellular regulation (including the first author [7, 16]), signalling ([18]), or ecosystems [1]. For the relation between Boolean Networks and Petri nets, see [8]. Further application fields for Petri nets in the life sciences, such as ecology [1], are currently emerging.

A central objective in these efforts is to identify and study attractors, infor-
mally stated as the possible long run behaviours of the system. These objects
are crucial in several domains. For instance, in the context of cellular regula-
tion, attractors give exactly the phenotypes of the studied system, whereas the
collapse or blossom of an ecosystem is characterized by the attractors it enters.
Furthermore an attractor fulfills reversibility: all visited states in an attractor
can be visited again.

While in general Petri nets, attractors may not exist, as soon as the net is
bounded, the reachability graph is finite and its terminal strongly connected
components correspond to the attractors. The boundedness of the nets is in
line with research in systems biology; regulation, signaling and other biological
networks are mass/energy bounded. An efficient method for exhaustive attractor
search via unfolding prefixes of safe discrete Petri nets was presented in [7].

**The limits of discrete models.** The discrete and non-deterministic nature of Petri nets are a key asset in these applications in the sense that they provide exhaustive treatment at a reasonable complexity (PSPACE for the reachability problem of bounded nets), compared to the predominant ODE or Markovian models in life sciences thus far. In fact, some works have studied more permissive discrete firing rules, between discrete Petri nets ([9]) and Boolean Networks ([10, 11, 7, 17]). The key motivation here is to ensure a better state space coverage, to avoid false predictions, diagnoses, or therapies. On the formal side, a gap in the reachability coverage had been first reported for contextual Petri nets [9]; following this, extensions to the traditional spectrum of semantics was developed for Boolean networks [10, 11, 7, 17], culminating in a *most permissive* or *MP* semantics [17]. This MPS provides a sound overapproximation of the natural, continuous behaviour of the system, paired with a low complexity for the discrete reachability problem (see [17] and the *zenodo* tool). Faithful refinement of this overapproximation remains an important open problem. From the *continuous* end of the spectrum, several authors (e.g. Heiner et al. [15]) have introduced continuous and fuzzy Petri nets as models of biological systems, in order to account for uncertainties in the modeling and observation of natural systems. However, the theory necessary for exploiting such models in prediction is still missing.

**Continuous Petri nets (CPN)**[13, 12, 3]. In a CPN, the marking can evolve
by firing a real quantity of a transition thus leading to a place marking defined
by a real. CPNs present several interests both from a theoretical and a modelling
point of view:
- Infinite firing sequences can be “convergent” and reach at the limit some marking. This yields the notion of lim-reachability which is sometimes more appropriate for modelling biological systems;

- reachability, lim-reachability and some other interesting problems can be solved in polynomial time while more difficult problems like the deadlock-freeness problem are NP-complete. These results hold even in unbounded CPNs, a major advantage over Petri nets.

**Our contributions.** Motivated by biological applications we focus on the following topic. Let the *mode* of a marking be the set of transitions fireable in the future. Along a firing sequence, the sequence of different modes is non increasing and forms what we call the *trajectory* of the sequence. The set of achievable trajectories is an important issue for instance in the study of biological processes. In CPNs, a marking can be reachable by a finite sequence or lim-reachable by an infinite convergent sequence. The set of signatures (resp. markings) obtained via lim-reachability (sometimes strictly) includes the set of trajectories (resp. markings) obtained via reachability. Here we introduce transfinite firing sequences over countable ordinals and establish several results:

- while trans-reachability is equivalent to lim-reachability, the set of trajectories associated with trans-reachability may be strictly larger than the one associated with lim-reachability;

- w.r.t. trajectories transfinite sequences over ordinals less than $\omega^2$ are enough;

- checking whether a trajectory is achievable is a NP-complete problem.

Afterwards, we turn on a more difficult problem: the specification for all transfinite firing sequences of their *signature*, i.e. the sequence of markings witnessing the changes of mode in the trajectory. In view of this goal, we define a finite symbolic reachability tree (SRT) which tracks the possible signatures of the system and where a set of markings with same mode is associated with each vertex. From an algorithmic point of view, we show how to build an effective representation of the SRT in exponential time even. While all these results hold for possibly unbounded CPNs, we establish that for bounded CPNs inside the leaves of the SRT (which correspond to the long-run behaviours), the CPN is reversible as it is the case for bounded discrete models (see above).

**Organisation.** In Section 2, we introduce continuous Petri nets and recall some of their theoretical properties needed for developing our results. Then in Section 3, we define transfinite firing sequences, their trajectory and signature and establish several related results including the NP-completeness of the trajectory problem. Afterwards in Section 4, we define the SRT and establish the reversibility inside its leafs and design the building of an effective representation. Finally in Section 5, we conclude and give some perspectives to this work. Omitted proofs can be found in the appendix.

## 2 Continuous Petri nets

We will follow the terminology and notations of [13] and for some notions the ones of [3, 12]. The omitted proofs of the results presented in this section can be found in [12].
**Notations.** Denote $\mathbb{R}_+ \triangleq [0, \infty)$, $\mathbb{I} \triangleq [0, 1]$, $\mathbf{0} \triangleq (0, \dots, 0) \in \mathbb{R}^n$. Let $\mathbf{v} \in \mathbb{R}_+^X$ where $X$ is a finite set. Then $[[\mathbf{v}]] \triangleq \{x \in X \mid \mathbf{v}[x] > 0\}$ and will be called the support of $\mathbf{v}$.

**2.1 Definitions and previous results**

Syntactically, there is no difference between CPNs and ordinary Petri nets.

**Definition 1 (Continuous Petri Net (CPN)).** A net is a tuple $\mathcal{N} = (P, T, \text{Pre}, \text{Post})$, where:

- $P$ a finite nonempty set of places;

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

- $\text{Pre}(\text{resp. Post})$ is the backward (resp. forward) $P \times T$ incidence matrix, whose entries belong to $\mathbb{N}$.

**Notations.** The incidence matrix of $\mathcal{N}$ is the matrix $\mathbf{C} \triangleq \text{Post} - \text{Pre}$. For $p \in P$, set $\bullet p \triangleq \{t \in T : \text{Post}(p, t) > 0\}$ and $p \bullet \triangleq \{t \in T : \text{Pre}(p, t) > 0\}$. Dually, for $t \in T$, set $\bullet t \triangleq \{p \in P : \text{Pre}(p, t) > 0\}$ and $t \bullet \triangleq \{p \in P : \text{Post}(p, t) > 0\}$. If $x \in P \cup T$, write $\bullet x \triangleq \bullet x \cup x \bullet$. These notations are extended to sets of items: $\bullet X \triangleq \bigcup_{x \in X} \bullet x$, $X \triangleq \bigcup_{x \in X} x \bullet$ and $\bullet X \triangleq \bigcup_{x \in X} \bullet x$. The reverse CPN is defined by: $\mathcal{N}^{-1} \triangleq (P, T, \text{Post}, \text{Pre})$.

In a CPN, the marking of a place is a non negative real and a CPN allows a fraction of a transition firing, scaling the quantities to be consumed and produced accordingly.

**Definition 2 (Marking, Marked CPN).** A (continuous) marking $\mathbf{m}$ of a CPN $\mathcal{N}$ is an item of $\mathbb{R}_+^P$. A marked CPN is a pair $(\mathcal{N}, \mathbf{m}_0)$ where $\mathbf{m}_0$ is an initial marking.

**Definition 3 (Enabling, Firing).** Let $\mathcal{N}$ be a CPN, $\mathbf{m}$ be a marking of $\mathcal{N}$, and $t \in T$. Then:

1. $\text{enab}(t, \mathbf{m})$, the enabling degree of $t$ in $\mathbf{m}$, is defined by $\min_{p \in \bullet t} \frac{\mathbf{m}(p)}{\text{Pre}(p, t)}$ when $\bullet t \neq \emptyset$, and $\infty$ otherwise. If $\text{enab}(t, \mathbf{m}) > 0$, one says that $t$ is enabled in $\mathbf{m}$.

2. For every $t$ and $\alpha \in [0, \text{enab}(t, \mathbf{m})] \cap \mathbb{R}$, $t$ can be $\alpha$-fired in $\mathbf{m}$, leading to a new marking $\mathbf{m}'$ given by: $\forall p \in P \ \mathbf{m}'(p) \triangleq \mathbf{m}(p) + \alpha \cdot \mathbf{C}(p, t)$, and we write $\mathbf{m} \xrightarrow{\alpha t} \mathbf{m}'$ (allowing null firings).

**Notation.** By analogy with Petri nets, we sometimes rewrite $\mathbf{m} \xrightarrow{1t} \mathcal{N} \mathbf{m}'$ as $\mathbf{m} \xrightarrow{t} \mathcal{N} \mathbf{m}'$. $\mathcal{Z} \triangleq \mathbb{R}_+ \times T$ denotes the set of firing steps. We denote by $\omega$ the first infinite ordinal.

**Definition 4.** Let $\mathbf{m}_0$ be a marking, $n \in \mathbb{N}$ and $\sigma = (\alpha_i t_i)_{i \le n}$ be a finite sequence over $\mathcal{Z}$. Then $\sigma$ is a finite firing sequence from $\mathbf{m}_0$ if there exists a finite sequence of markings $(\mathbf{m}_i)_{i \le n+1}$ such that for all $i \le n$, $\mathbf{m}_i \xrightarrow{\alpha_i t_i} \mathbf{m}_{i+1}$. In that case, write $\mathbf{m}_0 \xrightarrow{\sigma} \mathcal{N} \mathbf{m}_{n+1}$.
Let $\sigma = (\alpha_i t_i)_{i \in \mathbb{N}}$ be an infinite sequence over $\mathcal{Z}$ with $\sum_{i \in \mathbb{N}} \alpha_i < \infty$. Then $\sigma$ is an infinite firing sequence from $\mathbf{m}_0$ if there exists a infinite family of markings $(\mathbf{m}_i)_{i \le \omega}$ such that (1) for all $i \in \mathbb{N}$, $\mathbf{m}_i \xrightarrow{\sigma} \mathbf{m}_{i+1}$ and (2) $\lim_{i \to \infty} \mathbf{m}_i = \mathbf{m}_\omega$. In that case, write $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}_\omega$.

**Observation and notations.** The finiteness of $\sum_{i \in \mathbb{N}} \alpha_i$ ensures the existence of $\lim_{i \to \infty} \mathbf{m}_i$. When there is no ambiguity about $\mathcal{N}$, $\mathbf{m} \xrightarrow{\sigma} \mathbf{m}'$ will simply be denoted $\mathbf{m} \xrightarrow{\sigma} \mathbf{m}'$. Sometimes we omit the final marking and write $\mathbf{m} \xrightarrow{\sigma} \mathcal{N}$ instead of $\mathbf{m} \xrightarrow{\sigma} \mathcal{N} \mathbf{m}'$. Let $\sigma = (\alpha_i t_i)_{i \le n}$ be a finite sequence (resp. $\sigma = (\alpha_i t_i)_{i \in \mathbb{N}}$ be an infinite sequence such that $\sum_{i \in \mathbb{N}} \alpha_i < \infty$). Then $\vec{\sigma} \in \mathbb{R}_+^T$, the Parikh vector of $\sigma$, is defined by $\vec{\sigma}[t] \triangleq \sum_{i=t} \alpha_i$. Let $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$. Then the state equation $\mathbf{m} = \mathbf{m}_0 + \mathbf{C}\vec{\sigma}$ can be established by recurrence and possibly taking limits.

**Definition 5.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then:

The reachability set is defined by:

$$ \mathbf{RS}(\mathcal{N}, \mathbf{m}_0) \triangleq \{\mathbf{m} : \exists \sigma \in \mathcal{Z}^* \mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}\}. $$

The lim-reachability set is defined by:

$$ \lim \mathbf{RS}(\mathcal{N}, \mathbf{m}_0) \triangleq \{\mathbf{m} : \exists \sigma \in \mathcal{Z}^\infty \mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}\}. $$

Since the last step $\mathbf{m} \xrightarrow{\alpha t} \mathbf{m}'$ of a finite firing sequence can be mimicked by the in-
finite firing sequence $\mathbf{m} \xrightarrow{(2^{-n}\alpha t)_{n \ge 1}} \mathbf{m}'$, we have $\mathbf{RS}(\mathcal{N}, \mathbf{m}_0) \subseteq \lim \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$.
However generally these two sets are different.

The next definitions and propositions are related to the main topic of our
study: given a marking $\mathbf{m}_0$, what are the transitions eventually firable in the
future, starting from $\mathbf{m}_0$?

**Definition 6 (Firing set).** The firing set of a marked CPN $(\mathcal{N}, \mathbf{m}_0)$
$\mathbf{FS}(\mathcal{N}, \mathbf{m}_0) \subseteq 2^T$ is defined by: $\mathbf{FS}(\mathcal{N}, \mathbf{m}_0) \triangleq \{[[\vec{\sigma}]] \mid \exists \sigma \in \mathcal{Z}^* \exists \mathbf{m} \mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}\}$.

The next propositions summarize key results about firing sets and their close
connexion with reachability and lim-reachability.

**Proposition 1.** Let $\mathcal{N}$ be a CPN and $\mathbf{m}, \mathbf{m}'$ be markings of $\mathcal{N}$.

- If $[[\mathbf{m}]] \subseteq [[\mathbf{m}']]$ then $\mathbf{FS}(\mathcal{N}, \mathbf{m}) \subseteq \mathbf{FS}(\mathcal{N}, \mathbf{m}')$;

- $\mathbf{FS}(\mathcal{N}, \mathbf{m})$ is closed under union;

- if $T' = \{t_1, \dots, t_k\} \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$ then there exists a sequence $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$ with $\sigma = \alpha_1 t_{\beta(1)} \dots \alpha_k t_{\beta(k)}$, $\beta$ a permutation of $\{1, \dots, k\}$, $\alpha_i > 0$ for all $i$, and $[[\mathbf{m}]] = [[\mathbf{m}_0]] \cup \mathbf{T}'\mathbf{T}'$.

**Definition 7.** Let $\mathcal{N}$ be a CPN and $\mathbf{m}$ be a marking. Then $T_{\mathcal{N},\mathbf{m}}$, the mode of $\mathbf{m}$ in $\mathcal{N}$ is defined by: $T_{\mathcal{N},\mathbf{m}} \triangleq \{t \in T \mid \exists \mathbf{m} \xrightarrow{\sigma} \mathcal{N} \text{ with } t \in [[\vec{\sigma}]]\}$.

**Notations and observations.** The previous proposition implies that $T_{\mathcal{N},\mathbf{m}}$ is both the maximal item of $\mathbf{FS}(\mathcal{N}, \mathbf{m})$ and the union of these items. When there is no ambiguity about $\mathcal{N}$, we will simply write $T_{\mathbf{m}}$ for $T_{\mathcal{N},\mathbf{m}}$. Since the firing set only depends on the support of the marking, $T_{\mathbf{m}}$ (resp. $T_{\mathcal{N},\mathbf{m}}$, $\mathbf{FS}(\mathcal{N}, \mathbf{m})$) can also be denoted $T_{[[\mathbf{m}]]}$ (resp. $T_{\mathcal{N},[[\mathbf{m}]]}$, $\mathbf{FS}(\mathcal{N}, [[\mathbf{m}]])$).
**Proposition 2.** Let $\mathcal{N}$ be a CPN, $P' \subseteq P$ and $T' \subseteq T$. Then:

- one can check in polynomial time whether $T' \in \mathbf{FS}(\mathcal{N}, P')$;

- one can compute in polynomial time $T_{\mathcal{N},P'}$.

The next theorems now establish a characterization of reachability and lim-reachability. Observe that the latter one is obtained by dropping from the former one Condition (3).

**Theorem 1.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\mathbf{m}$ be a marking.

Then $\mathbf{m} \in \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ iff there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that:

(1) $\mathbf{m} = \mathbf{m}_0 + \mathbf{C} \cdot \mathbf{v}$, (2) $[[\mathbf{v}]] \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$, and (3) $[[\mathbf{v}]] \in \mathbf{FS}(\mathcal{N}^{-1}, \mathbf{m})$.

When such a $\mathbf{v}$ exists, there exists a finite $\sigma$ with $\vec{\sigma} = \mathbf{v}$ and $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$.

The structure of an infinite firing sequence witnessing the membership in $\lim \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ was established in the proof but not stated in the previous version of the following theorem.

**Theorem 2.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\mathbf{m}$ be a marking.

Then $\mathbf{m} \in \lim \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ iff there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that:

(1) $\mathbf{m} = \mathbf{m}_0 + \mathbf{C} \cdot \mathbf{v}$ and (2) $[[\mathbf{v}]] \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$.

Furthermore if $\mathbf{m} \in \lim \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, then there exist finite sequences $\sigma_0, \sigma_1$

such that $\mathbf{m}_0 \xrightarrow{\sigma_0} \mathbf{m}_1 \xrightarrow{(2^{-n}\sigma_1)_{n \ge 1}} \mathbf{m}$

with $[[\vec{\sigma}_0]] = [[\vec{\sigma}_1]] = [[\mathbf{v}]]$ and $[[\mathbf{m}_0]] \cup \bullet[[\vec{\sigma}_1]] \bullet = [[\mathbf{m}_1]]$.

Theorem 2 and its applications here motivate the following definition.

**Definition 8.** Let $\mathcal{N}$ be a CPN, $\mathbf{m}, \mathbf{m}'$ be markings and $\sigma$ be a finite sequence.

Then $\sigma' = (2^{-n}\sigma)_{n \ge 1}$ is a repetitive discounted sequence from $\mathbf{m}$ to $\mathbf{m}'$ if $\mathbf{m} \xrightarrow{\sigma'} \mathbf{m}'$ and $\bullet[[\vec{\sigma}]] \bullet \subseteq [[\mathbf{m}]]$.

The next lemma characterizes existence of repetitive discounted sequences.

**Lemma 1.** Let $\mathcal{N}$ be a CPN and $\mathbf{m}, \mathbf{m}'$ be two markings. Then there exists a repetitive discounted sequence from $\mathbf{m}$ to $\mathbf{m}'$ iff there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that: $\mathbf{m}' = \mathbf{m} + \mathbf{C} \cdot \mathbf{v}$ and $\bullet[[\mathbf{v}]] \bullet \subseteq [[\mathbf{m}]]$.

*Proof.* The necessity of this condition follows immediately by defining $\mathbf{v} = \vec{\sigma}$ when $\sigma' = (2^{-n}\sigma)_{n \ge 1}$ is the repetitive discounted sequence.

Since $\bullet[[\mathbf{v}]] \bullet \subseteq [[\mathbf{m}]]$, for all $t \in [[\mathbf{v}]]$, $\{t\} \in T_{\mathcal{N},[[\mathbf{m}]]} \cap T_{\mathcal{N}^{-1},[[\mathbf{m}]]}$ and by union $[[\mathbf{v}]] \in T_{\mathcal{N},[[\mathbf{m}]]} \cap T_{\mathcal{N}^{-1},[[\mathbf{m}]]}$.

For all $n \ge 0$, let us introduce $\mathbf{m}_n = 2^{-n}\mathbf{m} + (1 - 2^{-n})\mathbf{m}'$.

$\mathbf{m}_0 = \mathbf{m}$ and for all $n \ge 0$, $\mathbf{m}_{n+1} = \mathbf{m}_n + \mathbf{C} \cdot 2^{-(n+1)}\mathbf{v}$ and $[[\mathbf{m}_n]] = [[\mathbf{m}]]$.

Using Theorem 1, there exists $\sigma''$ such that $\mathbf{m} \xrightarrow{\sigma''} \mathbf{m}_1 = 2^{-1}\mathbf{m} + 2^{-1}\mathbf{m}'$ with $\vec{\sigma}'' = \frac{1}{2}\mathbf{v}$. Thus for all $n \ge 0$,

$2^{-n}\mathbf{m} \xrightarrow{2^{-n}\sigma''} 2^{-(n+1)}\mathbf{m} + 2^{-(n+1)}\mathbf{m}'$ implying in turn:

$$ \mathbf{m}_n = (1 - 2^{-n})\mathbf{m}' + 2^{-n}\mathbf{m} \xrightarrow{2^{-n}\sigma''} (1 - 2^{-n})\mathbf{m}' + 2^{-(n+1)}\mathbf{m} + 2^{-(n+1)}\mathbf{m}' = \mathbf{m}_{n+1} $$

So, with a slight abuse of notation, denoting $\sigma = 2\sigma''$, one gets: $\mathbf{m} \xrightarrow{(2^{-n}\sigma)_{n \ge 1}} \mathbf{m}'$.

□
## 2.2 Two motivating examples

*Example 1.* In figures, places are represented by circles with their initial markings inside, transitions by rectangles (each one with a label identifying it) and Pre (resp. Post) specified by weighted edges entering (resp. leaving) transitions. Consider the Petri net/CPN on the left hand side of Figure 1. It can be thought of as describing an epidemics situation, in which persons are initially healthy ($p_1$) but prone to catch one of two mild diseases ($p_2$ or $p_3$). If carriers of both diseases meet, a new and highly contagious syndrome ($p_4$) may emerge, which can spread in the populations of both $p_2$ and $p_3$. The reachability graph with only three states is depicted in the center part of Figure 1, where the modes are noted next to each node. The only terminal strongly connected components (TSCCs), also called attractors in this context, are {$p_2$} and {$p_3$}. However using the CPN firing rules we obtain the much richer dynamics. It can be checked that While {$p_2$} and {$p_3$} remain attractors, a third one emerges in {$p_4$}, showing how the continuous dynamics may increase the set of attractors of a system (in other circumstances, attractors may lose that status, merge etc).

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** A CPN/Petri net (left), its reachability graph (center) and another CPN (right).</figcaption></figure>

*Example 2.* Let us examine the CPN on the right of Figure 1. In natural systems, such a structure may correspond to a subsystem spanned by $p_2$ and $p_3$ that is reversible as long as some amount of resource $p_1$ is available, but stops when $p_1$ is depleted by a decay process. Let us examine the sequence of modes visited by a firing sequence $\sigma$. If $\sigma$ is a finite sequence then $p_1$ remains marked along the sequence; thus the single visited mode is $T$. For $\sigma = (2^{-n}t_1)_{n \ge 1}$, the marking reached by this infinite sequence is $1p_3$, and the corresponding sequence of modes is {$t_3$}. The marking $1p_2$ with associated mode $\emptyset$ is reachable from $1p_3$ in one step (by firing $1t_3$). It is possible to reach $1p_2$ with $\sigma = (2^{-n}t_1 2^{-n}t_3)_{n \ge 1}$. However the sequence of modes of this infinite sequence is $T\emptyset$. In fact, no finite or infinite sequence of firings from $m_0$ will produce the sequence of modes $T\{t_3\}\emptyset$. However, if we introduce transfinite sequences (i.e. indexed by ordinals instead of integers)
then the sequence $\sigma = (2^{-n}t_1)_{n \ge 1} 1t_3$, where the last transition firing is indexed by ordinal $\omega$, yields the sequence of modes $T\{t_3\}\emptyset$. This example motivates what will be introduced in the next section.

### 3 Signatures and trajectories

In the following, we lift the representation level to abstract away from the individual continuous markings. The key step is to shift attention from a marking $\mathbf{m}$ to its mode $T_{\mathbf{m}}$ (i.e. the transitions still fireable in the future).

**Notation.** Let $\kappa$ be a countable ordinal (i.e. an ordinal with countable cardinality). Then $\sigma = (\alpha_i t_i)_{i<\kappa}$, where for all $i$, $(\alpha_i t_i) \in \mathcal{Z}$, is a $\kappa$-transfinite sequence. Let $\sigma = (\alpha_i t_i)_{i<\kappa}$ be a $\kappa$-transfinite sequence and $i < i' \le \kappa$. Then $\sigma_{i,i'} = (\alpha_{i''}t_{i''})_{i\le i''<i'}$.

**Definition 9.** Let $\mathbf{m}_0$ be a marking, $\kappa$ be a countable ordinal and $\sigma = (\alpha_i t_i)_{i<\kappa}$ be a $\kappa$-transfinite sequence over $\mathcal{Z}$. Then $\sigma$ is a firing sequence from $\mathbf{m}_0$, denoted $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}_{\kappa}$, iff there exists a transfinite family of markings $(\mathbf{m}_i)_{i\le\kappa}$ such that:

- for all $i < \kappa$, $\mathbf{m}_i \xrightarrow{\alpha_i t_i} \mathbf{m}_{i+1}$;

- for all limit ordinals $\kappa' \le \kappa$, $\lim_{i<\kappa'} \mathbf{m}_i = \mathbf{m}_{\kappa'}$;

- $\sum_{i<\kappa} \alpha_i < \infty$.

**Notation.** In the sequel, $\sigma$, a $\kappa$-transfinite firing sequence, will be denoted by the pair $\sigma = ((\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa})$, and as usual the firing relation will be denoted by $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}_{\kappa}$.

**Definition 10.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then the trans-reachability set is defined by:

$$ \text{trans-}\mathbf{RS}(\mathcal{N}, \mathbf{m}_0) \triangleq \{\mathbf{m} \mid \exists \sigma \text{ } \kappa \text{ -transfinite sequence such that } \mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}\}. $$

The following proposition and its corollary establish that trans-reachability is equivalent to lim-reachability. Generalizing the case of infinite firing sequences, the Parikh vector of $\sigma$ is defined by $\vec{\sigma}[t] \triangleq \sum_{t_i=t} \alpha_i$.

**Proposition 3.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = ((\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa})$ be a $\kappa$-transfinite firing sequence. Then:

$$ (1) \quad \mathbf{m}_{\kappa} = \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma} \quad \text{and} \quad (2) \quad [[\vec{\sigma}]] \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0). $$

*Proof.* We proceed by induction on ordinals.

**Case 1:** $\kappa = \kappa' + 1$. Thus $\mathbf{m}_{\kappa} = \mathbf{m}_{\kappa'} + \alpha_{\kappa'} \mathbf{C}(t_{\kappa'})$. By induction, $\mathbf{m}_{\kappa'} = \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa'}$. Thus $\mathbf{m}_{\kappa} = \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa}$. Since $\vec{\sigma}_{0,\kappa'} \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$, applying Proposition 1, there exists a finite sequence $\mathbf{m}_0 \xrightarrow{\sigma'} \mathbf{m}'$ with $\vec{\sigma}' = \vec{\sigma}_{0,\kappa'}$ and $[[\mathbf{m}')] = [[\mathbf{m}_0]] \cup \bullet \vec{\sigma}' \bullet$ implying $[[\mathbf{m}_{\kappa'}]] \subseteq [[\mathbf{m}]]$. Thus there exists some $\alpha > 0$ such that $\mathbf{m}' \xrightarrow{\alpha t_{\kappa'}}$, which entails that $[[\vec{\sigma}_{0,\kappa'}]] \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$.

**Case 2:** $\kappa$ is a limit ordinal. Since $T$ is finite, there exists an ordinal $\kappa' < \kappa$ with $[[\vec{\sigma}_{0,\kappa'}]] = [[\vec{\sigma}_{0,\kappa}]]$. Applying the induction hypothesis, $[[\vec{\sigma}_{0,\kappa}]] \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_0)$. Let $\varepsilon > 0$. Since $\sum_{i<\kappa} \alpha_i < \infty$, there exists some $\kappa_{\varepsilon} < \kappa$ such that for all $\kappa_{\varepsilon} \le \kappa' < \kappa$ $\sum_{\kappa' \le i < \kappa} \alpha_i \le \varepsilon$. Let $B = \max(\text{Pre}(p, t), \text{Post}(p, t) \mid p \in P, t \in T)$. Then for all $\kappa_{\varepsilon} \le \kappa' < \kappa$:
- by induction, $\mathbf{m}_{\kappa'} = \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa'}$;

- and so $\|\mathbf{m}_{\kappa'} - \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa}\| \le B\epsilon$.

Since $\mathbf{m}_{\kappa} = \lim_{\kappa' < \kappa} \mathbf{m}_{\kappa'}$, this implies that $\|\mathbf{m}_{\kappa} - \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa}\| \le B\epsilon$.

Letting $\epsilon$ go to 0, one gets that $\mathbf{m}_{\kappa} = \mathbf{m}_0 + \mathbf{C} \cdot \vec{\sigma}_{0,\kappa}$.

□

Combining Proposition 3 with Theorem 2, we obtain the following corollary which generalizes the case of infinite firing sequences.

**Corollary 1.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa} \rangle$ a $\kappa$-transfinite firing sequence. Then there exist finite sequences $\sigma_0, \sigma_1$ such that
$$ \mathbf{m}_0 \xrightarrow{\sigma_0} \mathbf{m}_1 \xrightarrow{(2^{-n}\sigma_1)_{n\ge 1}} \mathbf{m}_{\kappa} \text{ with } [[\vec{\sigma}_0]] = [[\vec{\sigma}_1]] = [[\vec{\sigma}]] \text{ and } [[\mathbf{m}_0]] \cup \bullet [[\vec{\sigma}_1]] = [[\mathbf{m}_1]]. $$

As shown by the next proposition, along a transfinite firing sequence the modes associated with the visited markings are non increasing.

**Proposition 4.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa} \rangle$ be a $\kappa$-transfinite firing sequence. Then for all $i < i'$, $T_{\mathbf{m}_i} \subseteq T_{\mathbf{m}_i}$.

*Proof.* We proceed by a transfinite induction with nothing to prove for $\kappa = 0$.

**Case 1:** $\kappa = \kappa' + 1$. Thus $\mathbf{m}_{\kappa'} \xrightarrow{\alpha_{\kappa'} t_{\kappa'}} \mathbf{m}_{\kappa}$ which implies that every transition eventually fireable from $\mathbf{m}_{\kappa}$ is also eventually fireable from $\mathbf{m}_{\kappa'}$. So $T_{\mathbf{m}_{\kappa}} \subseteq T_{\mathbf{m}_{\kappa'}}$.

**Case 2:** $\kappa$ is a limit ordinal. Since $\mathbf{m}_{\kappa} = \lim_{i<\kappa} \mathbf{m}_i$, there exists some $\kappa_0$ such that for all $\kappa_0 \le \kappa' < \kappa$, $[[\mathbf{m}_{\kappa}]] \subseteq [[\mathbf{m}_{\kappa'}]]$. So $T_{\mathbf{m}_{\kappa}} = T_{[[\mathbf{m}_{\kappa}]]} \subseteq T_{[[\mathbf{m}_{\kappa'}]]} = T_{\mathbf{m}_{\kappa'}}$. Thus given an arbitrary $\kappa'' < \kappa$, either $\kappa'' \ge \kappa_0$ and the result is established or $\kappa'' < \kappa_0$ which implies by induction that $T_{\mathbf{m}_{\kappa''}} \supseteq T_{\mathbf{m}_{\kappa_0}} \supseteq T_{\mathbf{m}_{\kappa}}$. $\square$

So along a transfinite firing sequence the mode of the visited markings may only decrease a finite number of times. We aim at tracking these changes of mode and so we introduce some useful abstractions for a sequence.

**Definition 11.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa} \rangle$ be a $\kappa$-transfinite firing sequence.

- The leaps of $\sigma$ are those ordinals $\iota_0 < \dots < \iota_k$ with $k \le |T|$ inductively defined by $\iota_0 = 0$ and if $\iota_\ell$ exists and $T_{\mathbf{m}_{\iota_\ell}} \ne T_{\mathbf{m}_\kappa}$ then $\iota_{\ell+1}$ exists and $\iota_{\ell+1} = \min(\iota > \iota_\ell \mid T_{\mathbf{m}_\iota} \ne T_{\mathbf{m}_{\iota_\ell}})$;

- the signature of $\sigma$, $\mathrm{sig}(\sigma)$, is the pair $((\mathbf{m}_{\iota_i})_{i\le k}, \mathbf{m}_\kappa)$;

- the abstract signature of $\sigma$, $\mathrm{asig}(\sigma)$, is the pair $((T_{\mathbf{m}_{\iota_i}})_{i\le k}, \mathbf{m}_\kappa)$;

- the trajectory of $\sigma$, $\mathrm{traj}(\sigma)$, is $(T_{\mathbf{m}_{\iota_i}})_{i\le k}$.

**Notation.** Let $T$ be a set. Then the set of possible trajectories $\mathrm{Traj}(T) \triangleq \{(T_i)_{i\le k} \mid \forall i < k \ T_{i+1} \subseteq T_i \subseteq T\}$. By a slight abuse of notations, the markings $\mathbf{m}_{\iota_\ell}$ will also be called leaps of $\sigma$.

The next proposition shows that given a signature of a transfinite firing sequence, there exists another transfinite firing sequence of ordinal less than $\omega^2$ with same signature. Furthermore this sequence has a special shape.
**Proposition 5.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa} \rangle$ be a $\kappa$-transfinite firing sequence with $k+1$ leaps. Then there exist finite sequences $\sigma_{0,0}, \sigma_{0,1}, \dots, \sigma_{k,0}, \sigma_{k,1}$ such that:

- for all $i \le k$, $\mathbf{m}_{i,0} \xrightarrow{\sigma_{i,0}} \mathbf{m}_{i,1} \xrightarrow{(2^{-n}\sigma_{i,1})_{n\ge 1}} \mathbf{m}_{i+1,0}$
  with $\mathbf{m}_{0,0} = \mathbf{m}_0$ and $\mathbf{m}_{k+1,0} = \mathbf{m}_\kappa$;

- $[[\vec{\sigma}_{i,0}]] = [[\vec{\sigma}_{i,1}]]$ and $[[\mathbf{m}_{i,0}]] \cup \bullet[[\vec{\sigma}_{i,1}]] \bullet = [[\mathbf{m}_{i,1}}]$;

- $\text{sig}(\sigma') = \text{sig}(\sigma)$ with $\sigma' = (\sigma_{i,0}(2^{-n}\sigma_{i,1})_{n\ge 1})_{i\le k}$, being a $(k+1)\omega$-transfinite sequence;

- the leaps of $\sigma'$ are $0, \omega, 2\omega, \dots, k\omega$.

*Proof.* We establish the result by recurrence on $k$.

**Basis case** $k=0$. This case corresponds to the situation where $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$ with $T_{\mathbf{m}} = T_{\mathbf{m}_0}$. Applying Corollary 1, there there exist finite sequences $\sigma_0, \sigma_1$ such that $\mathbf{m}_0 \xrightarrow{\sigma_0} \mathbf{m}_1 \xrightarrow{(2^{-n}\sigma_1)_{n\ge 1}} \mathbf{m}_\kappa$ with $[[\vec{\sigma}_0]] = [[\vec{\sigma}_1]] = [[\vec{\sigma}]]$ and $[[\mathbf{m}_0]] \cup \bullet[[\vec{\sigma}_1]] \bullet = [[\mathbf{m}_1]]$. Let $\sigma' = \sigma_0(2^{-n}\sigma_1)_{n\ge 1}$ and consider an arbitrary marking $\mathbf{m}'$ visited by $\sigma'$. Since the modes are non increasing $T_{\mathbf{m}'} \supset T_{\mathbf{m}}$ and so there is no leaps other than $\mathbf{m}_0$ in $\sigma'$ which establishes this case.

**Inductive case.** Let $\sigma = \langle (\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa} \rangle$ be a transfinite firing sequence with signature $((\mathbf{m}_{i_i})_{i_i\le k}, \mathbf{m}_\kappa)$. Let $\sigma = \sigma_1\sigma_2$ where $\sigma_1$ leads from $\mathbf{m}_0$ to $\mathbf{m}_{i_1}$ (the second leap of $\sigma$) and $\sigma_2$ leads from $\mathbf{m}_{i_1}$ to $\mathbf{m}$. By hypothesis of recurrence there exist finite sequences $\sigma_{1,0}, \sigma_{1,1}, \dots, \sigma_{k,0}, \sigma_{k,1}$ fulfilling the properties of the proposition w.r.t. $\sigma_2$. Applying Corollary 1, there there exist finite sequences $\sigma'_0, \sigma'_1$ such that $\mathbf{m}_0 \xrightarrow{\sigma'_0} \mathbf{m}_1 \xrightarrow{(2^{-n}\sigma'_1)_{n\ge 1}} \mathbf{m}_{i_1}$ with $[[\vec{\sigma}_0]] = [[\vec{\sigma}'_1]] = [[\vec{\sigma}'_1]]$ and $[[\mathbf{m}_0]] \cup \bullet[[\vec{\sigma}_1]] \bullet = [[\mathbf{m}_1]]$. Let $\sigma' = \sigma'_0(2^{-n}\sigma'_1)_{n\ge 1}$. Since $[[\mathbf{m}_0]] \subseteq [[\mathbf{m}_1]]$, $T_{\mathbf{m}_1} = T_{\mathbf{m}_0}$

For $i \ge 1$, let $\mathbf{m}_{1,i}$ be the marking reached by the sequence $\sigma'_0(2^{-n}\sigma'_1)_{1\le n \le i}$. Observe that $\mathbf{m}_{1,i}$ is a convex combination of $\mathbf{m}_1$ and $\mathbf{m}_{i_1}$ with non null coefficients. So $[[\mathbf{m}_1]] \subseteq [[\mathbf{m}_{1,i}]]$ which implies that $T_{\mathbf{m}_{1,i}} = T_{\mathbf{m}_1} = T_{\mathbf{m}_0}$. For any arbitrary marking $\mathbf{m}' \ne \mathbf{m}_{i_1}$ visited by $\sigma'$, there exists some $\mathbf{m}_{1,i}$ visited later and so $T_{\mathbf{m}'} \supset T_{\mathbf{m}_{1,i}} = T_{\mathbf{m}_0}$. So the only leaps of $\sigma'$ are $\mathbf{m}_0$ and $\mathbf{m}_{i_1}$ which concludes the proof. $\square$

If we only consider modes and omit visited markings that we will tackle in the next section, the existence of a trajectory is a central issue.

**Definition 12.** The trajectory problem takes as input a marked CPN $(\mathcal{N}, \mathbf{m}_0)$ and a trajectory $\tau \in \text{Traj}(T)$ and checks whether there exists $\sigma$ a transfinite firing sequence of $(\mathcal{N}, \mathbf{m}_0)$ such that $\text{traj}(\sigma) = \tau$.

**Proposition 6.** The trajectory problem is NP-complete.

*Proof.* The proof of the hardness part is presented in the appendix. For the membership in NP, let us consider a marked CPN $(\mathcal{N}, \mathbf{m}_0)$ and a sequence $\tau = T_0 \dots T_K \in \text{Traj}(T)$ with $T_0 = T_{\mathbf{m}_0}$.

The non deterministic procedure, denoted $\mathcal{A}$, relies on the existence of the special shape (provided by Proposition 5) of the possibly transfinite firing sequence with
associated trajectory $\tau$,

$$ \begin{array}{rcl} \mathbf{m}_0 &=& \mathbf{m}_{0,0} \xrightarrow{\sigma_{0,0}} \mathbf{m}_{0,1} \xrightarrow{(2^{-n}\sigma_{0,1})_{n \ge 1}} \mathbf{m}_{1,0} \xrightarrow{\sigma_{1,0}} \dots \\ \dots &\xrightarrow{(2^{-n}\sigma_{K-2,1})_{n \ge 1}} & \mathbf{m}_{K-1,0} \xrightarrow{\sigma_{K-1,0}} \mathbf{m}_{K-1,1} \xrightarrow{(2^{-n}\sigma_{K-1,1})_{n \ge 1}} \mathbf{m}_{K,0} \end{array} $$

i.e., such that for all $i < K$:

$$ - [[\vec{\sigma}_{i,0}] = [[\vec{\sigma}_{i,0}]] \text{ and } [[\mathbf{m}_{i,0}]] \cup \bullet [[\vec{\sigma}_{i,1}]] \bullet = [[\mathbf{m}_{i,1}]]; $$

$$ - T_i = T_{[[\mathbf{m}_{i,0}]]} = T_{[[\mathbf{m}_{i,1}]]}; $$

$$ - \text{and } T_K = T_{[[\mathbf{m}_{K,0}]]}. $$

• A first guesses (in polynomial time) a sequence of subset of transitions $(X_i)_{i<K}$ and a sequence of subsets of places $(P_{i,0}, P_{i,1})_{0<i<K} P_{K,0}$ with $P_{0,0} = [[\mathbf{m}_0]]$.

• Then A checks whether for all $i < K$ $P_{i,0} \cup \bullet X_i \bullet = P_{i,1}$.

• Afterwards A checks (in polynomial time due to Proposition 1) whether for all $i < K$, $T_{P_{i,0}} = T_{P_{i,1}} = T_i$, and $T_{P_{K,0}} = T_K$.

• Then A checks the qualitative conditions of reachability and lim-reachability characterizations (see Theorems 1 and 2) : for all $i < K$, $X_i \in \mathbf{FS}(\mathcal{N}, P_{i,0}) \cap \mathbf{FS}(\mathcal{N}^{-1}, P_{i,1})$. Since $\mathbf{FS}(\mathcal{N}, P_{i,0}) \subseteq \mathbf{FS}(\mathcal{N}, P_{i,1})$, there is no need to check whether $X_i \in \mathbf{FS}(\mathcal{N}, P_{i,1})$. Again due to Proposition 1, these tests are performed in polynomial time.

• If the previous checks are successful, A builds the following linear program (including implicit strict inequalities due to the conditions about the supports) related to the quantitative conditions of reachability and lim-reachability characterizations where the (positive) variables are the components of the set of markings $\{\mathbf{m}_{i,j}\}_{i<K,j \in \{0,1\}} \cup \{\mathbf{m}_{K,0}\}$ and the set of Parikh vectors $\{\mathbf{v}_{i,j}\}_{i<K,j \in \{0,1\}}$:

$$ \begin{array}{l} \mathbf{m}_{0,0} = \mathbf{m}_0 \wedge \\ \quad \bigwedge_{0 \le i < K} \mathbf{m}_{i,1} = \mathbf{m}_{i,0} + \mathbf{C} \cdot \mathbf{v}_{i,0} \\ \wedge \quad \bigwedge_{0 \le i < K} \mathbf{m}_{i+1,0} = \mathbf{m}_{i,1} + \mathbf{C} \cdot \mathbf{v}_{i,1} \\ \quad \wedge \quad \bigwedge_{0 \le i < K, j \in \{0,1\}} [[\mathbf{m}_{i,j}]] = P_{i,j} \wedge [[\mathbf{v}_{i,j}]] = X_i \end{array} $$

Here and later on, an equation like $[[\mathbf{v}_{i,j}]] = X_i$ is an abbreviation for:

$$ \bigwedge_{t \in X_i} \mathbf{v}_{i,j}[t] > 0 \wedge \bigwedge_{t \in T \setminus X_i} \mathbf{v}_{i,j}[t] = 0. $$

Then A checks in polynomial time if this linear program is satisfiable. $\square$

## 4 A symbolic reachability tree

In Examples 1 and 2 above, we have used an abstraction approach that lumps together markings having the same set of eventually firable transitions into modes. Here, we will formalize the associated semantics in the form of symbolic reachability trees, introduced in Subsection 4.1. In Subsection 4.2, the “reversibility” of
the leaves of these trees will be established, using linear algebra theory. Finally
we develop a construction of an effective representation of symbolic reachability
trees in Subsection 4.3.

**4.1 Definition**

The aim of the symbolic reachability tree (SRT) that we will build is to rep-
resent in an effective way all the abstract signatures of $\kappa$-transfinite sequences
of a marked CPN. By effective we mean that we can check not only whether a
potential abstract signature exists, but also for inclusion or equality of the sets
of abstract signatures of two CPNs.

In order to define an appropriate SRT, we first introduce the abstract reach-
ability graph. Since the mode of a marking only depends on its support, the
abstract reachability graph tracks the possible evolution of the supports of reach-
able markings. Therefore, the vertices of this graph are the subsets of P. Let us
summarize some of the results of the previous section that guide us for the
construction of the edges of this graph:

- For $\mathbf{m} \xrightarrow{\sigma} \mathbf{m}'$, a transfinite firing sequence with $T_{\mathbf{m}'} = T_{\mathbf{m}}$, there exists an infinite firing sequence $\sigma'$ with $\mathbf{m} \xrightarrow{\sigma'} \mathbf{m}'$ implying $[[\vec{\sigma}')] \in \mathbf{FS}(\mathcal{N}, [[\mathbf{m}]])$;

- For $\mathbf{m} \xrightarrow{\sigma} \mathbf{m}'$, a transfinite firing sequence whose only leaps are the initial and final markings, there exist a finite sequence $\sigma_0$ and a repeated discounted firing sequence $(2^{-n}\sigma_1)_{n \ge 1}$ with $\mathbf{m} \xrightarrow{\sigma_0} \mathbf{m}_1 \xrightarrow{(2^{-n}\sigma_1)_{n \ge 1}} \mathbf{m}'$, $[[\vec{\sigma}_0]] = [[\vec{\sigma}_1]] = [[\vec{\sigma}]]$ and $[[\mathbf{m}_1]] = [[\mathbf{m}_0]] \cup \cdot[[\vec{\sigma}_1]]\cdot$. The leaps of this alternative firing sequence are also the initial and final markings.

Thus there will be two kinds of edges from $P'$ to $P'' \neq P'$ in our graph. When $T_{P''} = T_{P'}$, there is an anonymous edge from $P'$ to $P''$ if there exists a set of transitions $T'$ with $T' \in \mathbf{FS}(\mathcal{N}, P')$ and $P'' \subseteq P' \cup T'\cdot$, since those are the only places that may be marked after the firing of an infinite sequence whose support is $T'$ and $P' \setminus \cdot T' \subseteq P''$ since these places remain marked after such a firing. When $P'' \subsetneq P$ and $T_{P''} \subseteq T_{P'}$ there is an edge labelled by some $T' \subseteq T$ with (1) $\cdot T'\cdot \subseteq P'$ and (2) $P' \setminus \cdot T' \subseteq P''$. Here, (1) is a necessary condition for the existence of a repeated discounted firing sequence described in Lemma 1, and (2) is a necessary condition ensuring that the support of the target marking is $P''$. This kind of edges is called border edges. Omitting labels for anonymous edges will be justified during the description of the SRT.

**Definition 13 (Abstract reachability graph).** Let $\mathcal{N}$ be a CPN. Then its
abstract reachability graph $\text{ARG}(\mathcal{N}) = (V, E)$ is defined as follows:

- $V = 2^P$ is its set of vertices;

- For all $P' \neq P'' \subseteq P$ with $T_{P'} = T_{P''}$, $P' \to P''$ is an edge of $E$ iff there exists $T' \subseteq T$ such that:

(1) $T' \in \mathbf{FS}(\mathcal{N}, P')$ and (2) $P' \setminus \cdot T' \subseteq P'' \subseteq P' \cup T'\cdot$.

- For all $T' \subseteq T$, $P'' \subseteq P' \subseteq P$, $T_{P''} \subseteq T_{P'}$, $P' \xrightarrow{T'} P''$ is an edge of $E$ iff:

(1) $\cdot T' \cdot \subseteq P'$ and (2) $P' \setminus \cdot T' \subseteq P''$.
Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then its abstract reachability graph $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$ is the restriction of $\text{ARG}(\mathcal{N})$ to the vertices reachable from $[[\mathbf{m}_0]]$.

**Lemma 2.** *The reflexive closure of $\rightarrow$, the anonymous relation of $\text{ARG}(\mathcal{N})$, denoted $\rightarrow^*$ is transitive.*

*Proof.* Let $P_1 \rightarrow P_2 \rightarrow P_3$ with $P_3 \neq P_1$. So for $i \in \{1, 2\}$, there exists $T_i$ with $T_i \in \text{FS}(\mathcal{N}, P_i)$ and $P_i \setminus \text{\textbullet} T_i \subseteq P_{i+1} \subseteq P_i \cup T_i$. Let $T' = T_1 \cup T_2$. Then: $P_1 \setminus \text{\textbullet} T' = (P_1 \setminus \text{\textbullet} T_1) \setminus \text{\textbullet} T_2 \subseteq P_2 \setminus \text{\textbullet} T_2 \subseteq P_3 \subseteq P_2 \cup T_2$. Pick an arbitrary marking $\mathbf{m}$ with $[[\mathbf{m}]] = P'$. Applying Proposition 1, there exists $\mathbf{m} \xrightarrow{\sigma} \mathbf{m}'$ with $[[\vec{\sigma}]] = T_1$ and $[[\mathbf{m}')] = [[\mathbf{m}]] \cup \text{\textbullet} T_1$.

Thus $[[\mathbf{m}')] \supseteq P_2$. Since $T_2 \in \text{FS}(\mathcal{N}, P_2)$ there exists $\mathbf{m}' \xrightarrow{\sigma'}$ with $[[\vec{\sigma}]] = T_2$.

So $\mathbf{m} \xrightarrow{\sigma\sigma'}$ implying $T' \in \text{FS}(\mathcal{N}, P_1)$. Thus $P_1 \rightarrow P_3$.

□

The next definitions show how to define the acceptance of a signature of a transfinite firing sequence by the ARG.

**Definition 14.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN, $s = (P_i^{-} \xrightarrow{X_i} P_i^{+})_{0<i\leq k}$ a sequence of border edges of $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$ and $P_f \subseteq P$. Then the pair $(s, P_f)$ is a symbolic path of $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$ if $[[\mathbf{m}_0]] \rightarrow^* P_f$ when $s = \varepsilon$, and $s \neq \varepsilon$ implies

- $[[\mathbf{m}_0]] \rightarrow^* P_1^{-}$ and $P_k^{+} \rightarrow^* P_f$;

- for all $0 < i < k$, $P_i^{+} \rightarrow^* P_{i+1}$.

**Definition 15.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN, $(s, P_f)$ be a symbolic path of $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$ with $s = (P_i^{-} \xrightarrow{X_i} P_i^{+})_{0<i\leq k}$ and $\sigma$ be a transfinite firing sequence with $\text{sig}(\sigma) = ((\mathbf{m}_i)_{i\leq k}, \mathbf{m}_f)$. Then $\text{sig}(\sigma)$ is accepted by $(s, P_f)$ if for all $i \leq k$, $P_i^{+} = [[\mathbf{m}_i]]$ and $P_f = [[\mathbf{m}_f]]$.

**Example 3.** Figure 2 depicts a marked CPN $(\mathcal{N}, \mathbf{m}_0)$ and its abstract reachability graph. The anonymous edges are represented by single lines, border edges by double lines. For border edges labelled by $T'$, we omit the brackets defining $T'$ (e.g., $\{t_1, t_2\}$ is shown as $t_1, t_2$). Let $\sigma = \mathbf{m}_0 \xrightarrow{t_1 t_2} \mathbf{0}$ a firing sequence with $\text{sig}(\sigma) = (\mathbf{m}_0 \ 1p_2 \ \mathbf{0}, \mathbf{0})$, and the following symbolic path in $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$: $c = (\{p_1\} \xrightarrow{t_1} \{p_2\} \{p_2\} \xrightarrow{t_2} \emptyset, \emptyset)$; $c$ accepts $\text{sig}(\sigma)$. For firing sequence $\sigma' = \mathbf{m}_0 \xrightarrow{(2^{-n}t_1 2^{-n}t_2)_{n\geq 1}} \mathbf{0}$ with $\text{sig}(\sigma') = (\mathbf{m}_0 \ \mathbf{0}, \mathbf{0})$, take pair: $c' = (\{p_1, p_2\} \xrightarrow{\{t_1, t_2\}} \emptyset, \emptyset)$ in $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$. Since $\{p_1\} \rightarrow^* \{p_1, p_2\}$, $c'$ accepts $\text{sig}(\sigma')$. Figure 3 depicts another marked CPN $(\mathcal{N}', \mathbf{m}'_0)$ and its abstract reachability graph. Consider the symbolic path in $\text{ARG}(\mathcal{N}', \mathbf{m}'_0)$: $c'' = (\{p_1, p_2\} \xrightarrow{\{t_1, t_2\}} \emptyset, \emptyset)$. The abstract reachability graph does not depend on the exact weights of the net. Here, if $x = 1$, then no signature of a firing sequence will be accepted by $c''$ since for all lim-reachable marking $\mathbf{ms}$, $\|\mathbf{m}\|_1 \triangleq \mathbf{m}(p_1) + \mathbf{m}(p_2) = 1$. On the other hand, if $x = 2$, then $\sigma'' = \mathbf{m}_0 \xrightarrow{\frac{1}{4}t_1} \mathbf{m}_1 \xrightarrow{(2^{-n}(\frac{1}{2}t_1 1t_2 \frac{1}{4}t_1))_{n\geq 1}} \mathbf{0}$ with $\mathbf{m}_1 = \frac{1}{2}p_1 + \frac{1}{4}p_2$ fulfills $\text{sig}(\sigma'') = (\mathbf{m}_0 \ \mathbf{0}, \mathbf{0})$.
<figure><img src="image_3.png" /><figcaption>Fig. 2. A marked CPN and its ARG.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 3. Another marked CPN and its ARG.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 4. The symbolic reachability tree of the marked CPN of Figure 2.</figcaption></figure>

The next proposition shows that the ARG accepts the signatures of all trans-
finite firing sequences (but possibly more as illustrated by the CPN of Figure 3).
Its proof is an immediate consequence of the definition of the edges as discussed
above.

**Proposition 7.** Let ($\mathcal{N}$, $\mathbf{m}_0$) be a marked CPN and $\sigma$ be a transfinite firing sequence for ($\mathcal{N}$, $\mathbf{m}_0$). Then there exists a symbolic path ($s, P_f$) of ARG($\mathcal{N}$, $\mathbf{m}_0$) such that $\text{sig}(\sigma)$ is accepted by ($s, P_f$).

In order to take into account the markings while building the SRT, we intro-
duce two operators on sets of markings of CPN.

**Definition 16.** Let $\mathcal{N}$ be a CPN and $R$ be a set of markings. Then:
$$ \text{closure}(R) = \{\mathbf{m}' \mid \exists \mathbf{m} \in R \ [[\mathbf{m}]] \to^* [[\mathbf{m}']] \wedge \mathbf{m}' \in \lim\nolimits_{\mathbf{m}'} \mathbf{RS}(\mathcal{N}, \mathbf{m})\}. $$
Let $\mathrm{tr} = P' \xrightarrow{T'} P''$ be a border edge of $\mathrm{ARG}(\mathcal{N})$. Then $\mathrm{succ}(\mathrm{tr}, R)$ is:

$$ \{ \mathbf{m}' \mid \exists \mathbf{m} \xrightarrow{(2^{-n}\sigma)_{n \ge 1}} \mathbf{m}' \wedge \mathbf{m} \in R \wedge [[\mathbf{m}]] = P' \wedge [[\mathbf{m}')] = P'' \wedge [[\vec{\sigma}]] = T' \}. $$

We are now in a position to define the symbolic reachability tree which will keep track of the abstract signatures of a marked CPN.

**Definition 17 (Symbolic reachability tree).** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. The symbolic reachability tree $\mathrm{SRT}(\mathcal{N}, \mathbf{m}_0)$, of $(\mathcal{N}, \mathbf{m}_0)$ is a directed tree whose vertices $v$ are labelled by a non empty set of markings $R_v$ and their common mode $T_v$, and edges are labelled by border edges of $\mathrm{ARG}(\mathcal{N}, \mathbf{m}_0)$, inductively defined by:

- The root $r$ is labelled by $T_r = T_{\mathbf{m}_0}$ and $R_r = \mathrm{closure}(\{\mathbf{m}_0\})$.

- Let $v$ be a vertex labelled by $T_v$ and $R_v$. For all border edge $\mathrm{tr} = P' \xrightarrow{T'} P''$ such that $\mathrm{succ}(\mathrm{tr}, R_v) \neq \emptyset$ there is a vertex $v'$ and an edge $v \xrightarrow{\mathrm{tr}} v'$ with $T_{v'} = T_{P''}$ and $R_{v'} = \mathrm{closure}(\mathrm{succ}(\mathrm{tr}, R_v))$.

This tree is finite with depth at most $T$ since every vertex has a finite number of children with their mode strictly included in the mode of their father.

**Example 4.** In the examples of SRTs we only represent the set of markings labelling a vertex omitting their common mode. The SRT of the CPN of Figure 2 is depicted in Figure 4. The set of markings associated with the root are the lim-reachable markings such that $p_1$ remains marked. Using the border edge $P \xrightarrow{\{t_1\}} \{p_2\}$, one reaches the vertex $v_2$ whose set of markings is such that $p_1$ is unmarked and $p_2$ is marked, and thus their common mode is $\{t_2\}$. Via the border edge $P \xrightarrow{\{t_1, t_2\}} \emptyset$, one reaches the vertex $v_3$ whose set of markings is the null marking with $\emptyset$ as mode. Observe that some vertices have the same set of markings and could be merged, thus producing a directed acyclic graph. The SRT of the CPN of Figure 3 when $x = 2$ is depicted in Figure 5. The set of markings associated with the root are those lim-reachable markings for which either $p_1$ or $p_2$ remains marked; hence their common mode is $T$. This set is characterized by the inequalities $0 < \mathbf{m}(p_1) + 2\mathbf{m}(p_2) \le 1$. Using the border edge $P \xrightarrow{\{t_1, t_2\}} \emptyset$, one creates the vertex $v_1$, whose set of markings is the null marking, with $\emptyset$ as mode.

The next two propositions establish that the SRT exactly captures the signatures of the CPN.

<figure><img src="image_6.png" /><figcaption>**Fig. 5.** The symbolic reachability tree of the marked CPN of Figure 3 when $x = 2$.</figcaption></figure>
**Proposition 8.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma$ be a $\kappa$-transfinite firing sequence with $\text{sig}(\sigma) = ((\mathbf{m}_i)_{i\le k}, \mathbf{m}_\kappa)$. Then there exists a path $\rho = r \xrightarrow{tr_1} v_1 \xrightarrow{tr_2} \dots \xrightarrow{tr_k} v_k$ in SRT$(\mathcal{N}, \mathbf{m}_0)$ such that: $\forall 1 \le i \le k \; \mathbf{m}_i \in R_{v_i} \wedge \mathbf{m}_\kappa \in R_{v_\kappa}$.

*Proof.* Due to Proposition 5, there exist finite (possibly null) sequences $\sigma_{0,0}$, $\sigma_{0,1}$, ..., $\sigma_{k,0}$, $\sigma_{k,1}$ with $0 \le k \le |T|$ such that:

- for all $i \le k$, $\mathbf{m}_{i,0} \xrightarrow{\sigma_{i,0}} \mathbf{m}_{i,1} \xrightarrow{(2^{-n}\sigma_{i,1})_{n\ge 1}} \mathbf{m}_{i+1,0}$ with $\mathbf{m}_{0,0} = \mathbf{m}_0$ and $\mathbf{m}_{k+1,0} = \mathbf{m}_\kappa$;

- $[[\vec{\sigma}_{i,0}]] = [[\vec{\sigma}_{i,1}]]$ and $[[\mathbf{m}_{i,0}]] \cup [[\bullet[\vec{\sigma}_{i,1}]] \bullet] \subseteq [[\mathbf{m}_{i,1}]]$;

- $\text{sig}(\sigma') = \text{sig}(\sigma)$, where $\sigma' = (\sigma_{i,0}(2^{-n}\sigma_{i,1})_{n\ge 1})_{i\le k}$ is a finite-length $(k+1)\omega$-transfinite sequence;

- the leaps of $\sigma'$ are $0, \omega, 2\omega, \dots, k\omega$.

When $T_{\mathbf{m}_\kappa} = T_{\mathbf{m}_0}$, by definition of $R_r = \text{closure}(\mathbf{m}_0)$, one has $\mathbf{m}_\kappa \in R_r$ since $\mathbf{m}_\kappa$ is lim-reachable from $\mathbf{m}_0$; thus $\rho$ consists only of $r$.

Otherwise we build $\rho$ in an inductive way. Note that $T_{\mathbf{m}_{0,1}} = T_{\mathbf{m}_0}$, and since $\mathbf{m}_{0,1}$ is reachable from $\mathbf{m}_0$, also $\mathbf{m}_{0,1} \in R_r$. Define $P' = [[\mathbf{m}_{0,1}}]]$, $P'' = [[\mathbf{m}_{1,0}}]]$ and $X = [[\sigma_{0,1}}]]$. Note that $\text{tr}_1 = P' \xrightarrow{X} P''$ is a border edge of $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$ and $\mathbf{m}_{1,0} \in \text{succ}(\text{tr}_1, R_r)$. Thus $\text{succ}(\text{tr}_1, R_r) \ne \emptyset$, and there is a vertex $v_1$ and a transition $r \xrightarrow{\text{tr}_1} v_1$ with $\mathbf{m}_{1,0} \in \text{succ}(\text{tr}_1, R_r)$ and $\mathbf{m}_{1,1} \in \text{closure}(\text{succ}(\text{tr}_1, R_r)) = R_{v_1}$.

By induction hypothesis, one gets a path $r \xrightarrow{\text{tr}_1} v_1 \cdots \xrightarrow{\text{tr}_k} v_k$ such that for all $1 \le i \le k$, $\mathbf{m}_{i,0} \in R_{v_i}$. Since $\mathbf{m}_\kappa = \mathbf{m}_{k+1,0}$ is lim-reachable from $\mathbf{m}_{k,0}$ and $T_{\mathbf{m}_\kappa} = T_{\mathbf{m}_{k,0}}$, we have $\mathbf{m}_\kappa \in R_{v_k}$, which concludes the proof. $\square$

**Proposition 9.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN, $\rho$ be a path $r = v_0 \xrightarrow{\text{tr}_1} v_1 \xrightarrow{\text{tr}_2} \dots \xrightarrow{\text{tr}_k} v_k$ in SRT$(\mathcal{N}, \mathbf{m}_0)$ and $\mathbf{m}_\kappa \in R_{v_k}$. Then there exists a transfinite firing sequence $\sigma$ with $\text{sig}(\sigma) = ((\mathbf{m}_i)_{i\le k}, \mathbf{m}_\kappa)$. such that: $\forall 1 \le i \le k \; \mathbf{m}_i \in R_{v_i}$.

*Proof.* We build $\sigma$ by induction. When $k=0$, $\mathbf{m}_\kappa \in R_{v_0}$. By definition of $R_{v_0}$, there exists an infinite firing sequence $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}_\kappa$ and $T_{\mathbf{m}_\kappa} = T_{\mathbf{m}_0}$ which implies that the signature of $\sigma$ is $(\mathbf{m}_0, \mathbf{m}_\kappa)$.

Assume now that $k > 0$. Then there exists a border edge $\text{tr}_k = P' \xrightarrow{X} P''$ and a marking $\mathbf{m}_k \in \text{succ}(\text{tr}, R_{v_{k-1}})$ such that $[[\mathbf{m}_k]] = P''$ and $\mathbf{m}_\kappa$ is lim-reachable from $\mathbf{m}_k$ and $T_{\mathbf{m}_\kappa} = T_{\mathbf{m}_k}$.

Since $\mathbf{m}_k \in \text{succ}(\text{tr}, R_{v_{k-1}})$, there exists $\mathbf{m}_k^- \in R_{v_{k-1}}$ such that $[[\mathbf{m}_k^-]] = P'$, and $\sigma$ is a repeated discounted sequence with $[[\vec{\sigma}]] = X$ and $\mathbf{m}_k^- \xrightarrow{\sigma} \mathbf{m}_k$.

By induction hypothesis, we obtain a transfinite firing sequence from $\mathbf{m}_1^- \in R_r$ to $\mathbf{m}_\kappa$, and thus a transfinite firing sequence from $\mathbf{m}_0$ to $\mathbf{m}_\kappa$ such that its leaps are $\mathbf{m}_0, \mathbf{m}_1, \dots, \mathbf{m}_k$ as required by the proposition. $\square$

## 4.2 Terminal components of the SRT for bounded CPNs

As for marked Petri nets, a marked CPN is *bounded* if there exists a bound $B \in \mathbb{N}$ such that for all reachable markings $\mathbf{m}$, $\|\mathbf{m}\|_\infty \le B$. There is a useful characterization of (un)boundedness for marked CPN via linear programming.
**Theorem 3 ([12]).** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then $(\mathcal{N}, \mathbf{m}_0)$ is unbounded iff there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that (1) $\mathbf{C} \cdot \mathbf{v} \ge 0$ and (2) $[\mathbf{v}] \subseteq T_{\mathbf{m}_0}$.

Consider **m** a marking belonging to a strongly connected component (SCC) of the reachability graph of a bounded Petri net. Then for all **m'** reachable from **m**, **m** is reachable from **m'**. This property, which is called *reversibility* and whose proof follows from the definition of SCCs, is of crucial importance in biological applications (characterization of phenotypes, etc).

**Notation.** A terminal component of the SRT is the set of markings associated with a leaf of the SRT. Observe that by definition of the SRT for all **m**, **m'** in a terminal component, $T_{\mathbf{m}} = T_{\mathbf{m}'}$.

Here we establish reversibility inside terminal components of the SRT of a bounded marked CPN. In the context of CPNs, reversibility can be stated as follows: Let **m** be a marking of a terminal SRT component and **m'** be lim-reachable from **m**, then **m** is lim-reachable from **m'**. To prove this, let us recall the following proposition from linear programming theory about duality.

**Proposition 10.** Let $\mathbf{A}$ be a real matrix of dimension $K \times L$ and $1 \le k \le K$. Then the following statements are equivalent:

$$- \exists \mathbf{v} \in \mathbb{R}_+^K \mathbf{v} \cdot \mathbf{A} \le 0 \land \mathbf{v}[k] > 0$$

$$- \exists \mathbf{w} \in \mathbb{R}_+^L \mathbf{A} \cdot \mathbf{w} \ge 0 \land (\mathbf{A} \cdot \mathbf{w})[k] > 0$$

Let us consider $\mathbf{B} = -\mathbf{A}^t$ with dimension of $\mathbf{A}$ being now $L \times K$. Then we get another formulation for the duality property obtained by combining trans-position and additive inversion.

**Proposition 11.** Let $\mathbf{B}$ be a real matrix of dimension $L \times K$ and $1 \le k \le K$. Then the following statements are equivalent:

$$- \exists \mathbf{v} \in \mathbb{R}_+^K \mathbf{B} \cdot \mathbf{v} \ge 0 \land \mathbf{v}[k] > 0$$

$$- \exists \mathbf{w} \in \mathbb{R}_+^L \mathbf{w} \cdot \mathbf{B} \le 0 \land (\mathbf{w} \cdot \mathbf{B})[k] < 0$$

Using Proposition 10, one can reformulate the characterization of the boundedness of a marked CPN stated by Theorem 3.

**Notation.** Let $\mathcal{N}$ be a CPN, $\mathbf{C}$ be its incidence matrix and $T' \subseteq T$. Then $\mathbf{C}_{T'}$ denotes $\mathbf{C}$ reduced to the columns of $T'$.

**Theorem 4.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then $(\mathcal{N}, \mathbf{m}_0)$ is bounded iff there exists $\mathbf{w} \in \mathbb{R}_+^P$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{m_0}} \le 0 \land [[\mathbf{w}}]] = P$.

*Proof.* Let us recall the characterization of Theorem 3. $(\mathcal{N}, \mathbf{m}_0)$ is bounded iff there does not exist $\mathbf{v} \in \mathbb{R}_+^T$ such that $\mathbf{C} \cdot \mathbf{v} \ge 0$ and $[[\mathbf{v}}]] \subseteq T_{\mathbf{m}_0}$, which is equivalent to the assertion that there does not exist $\mathbf{v} \in \mathbb{R}_+^{T_{m_0}}$ such that $\mathbf{C}_{T_{m_0}} \cdot \mathbf{v} \ge 0$. This is also equivalent to: "For all $p \in P$, there does not exist $\mathbf{v} \in \mathbb{R}_+^{T_{m_0}}$ such that $\mathbf{C}_{T_{m_0}} \cdot \mathbf{v} \ge 0 \land (\mathbf{C}_{T_{m_0}} \cdot \mathbf{v})[p] > 0."

Applying Proposition 10, this is also equivalent to the following statement:

"For all $p \in P$, there exists $\mathbf{w}_p \in \mathbb{R}_+^P$ such that $\mathbf{w}_p \cdot \mathbf{C}_{T_{m_0}} \le 0 \land \mathbf{w}[p] > 0."

Setting $\mathbf{w} = \sum_{p \in P} \mathbf{w}_p$, this is equivalent to:

There exists $\mathbf{w} \in \mathbb{R}_+^P$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{m_0}} \le 0 \land [[\mathbf{w}}]] = P$. $\square$
The next lemma implies that, starting from a marking of a terminal component, the inequality of Theorem 4 is in fact an equality; that will be stated by Theorem 5 below.

**Lemma 3.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a bounded marked CPN such that for all $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, $T_{\mathbf{m}} = T_{\mathbf{m}_0}$. There does not exist $\mathbf{w} \in \mathbb{R}_+^P$ such that:

$$ \mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0. $$

*Proof.* Due to Proposition 1, there exists $\mathbf{m}_1 \in \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ such that, for all $p \in \bullet T_{\mathbf{m}_0}$, $\mathbf{m}_1(p) > 0$. Thus for all $t \in T_{\mathbf{m}_0}$, $\{t\} \in \mathbf{FS}(\mathcal{N}, \mathbf{m}_1)$. Since $\mathbf{FS}(\mathcal{N}, \mathbf{m}_1)$ is closed under union, any subset of $T_{\mathbf{m}_0}$ belongs to $\mathbf{FS}(\mathcal{N}, \mathbf{m}_1)$. Hence $\lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_1) = \{\mathbf{m} \in \mathbb{R}_+^P \mid \exists \mathbf{v} \in \mathbb{R}_+^{T_{\mathbf{m}_0}} \wedge \mathbf{m} = \mathbf{m}_1 + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}\}$.

Assume by contradiction that there exists $\mathbf{w} \in \mathbb{R}_+^P$ and $t \in T_{\mathbf{m}_0}$ such that:

$$ \mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0 \text{ and } (\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}})[t] < 0. $$

Let $\alpha = \sup(\mathbf{v}[t] \mid \mathbf{v} \in \mathbb{R}_+^{T_{\mathbf{m}_0}} \wedge \mathbf{m}_1 + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} \ge 0)$. Since $\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0$ and $(\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}})[t] < 0$, $\alpha$ is finite. Due to linear programming theory, there is some $\mathbf{v}$ such that $\mathbf{m}_1 + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} \ge 0$ and $\mathbf{v}[t] = \alpha$. Let $\mathbf{m} = \mathbf{m}_1 + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}$. Then $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_1) \subseteq \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ and $t \notin T_{\mathbf{m}}$, a contradiction. $\square$

**Theorem 5.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a bounded marked CPN such that $T_{\mathbf{m}} = T_{\mathbf{m}_0}$ for all $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$. Then there exists $\mathbf{w} \in \mathbb{R}_+^P: \mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} = 0 \wedge [[\mathbf{w}]]] = P$.

*Proof.* Since $(\mathcal{N}, \mathbf{m}_0)$ is bounded, there exists $\mathbf{w} \in \mathbb{R}_+^P$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0$ and $[[\mathbf{w}]]] = P$. By Lemma 3, there is no $\mathbf{w}$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0$.

$$ \text{Hence } \mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} = 0. \quad \square $$

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

Let $\mathbf{m}_0$ be a marking of a terminal component of the SRT of a bounded marked CPN. While Theorem 5 states that, when restricted to $T_{\mathbf{m}_0}$, there is a place invariant whose support is $P$, one has by the following theorem that there is a transition invariant whose support is $T_{\mathbf{m}_0}$.

**Theorem 6.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a bounded marked CPN such that for all $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, $T_{\mathbf{m}} = T_{\mathbf{m}_0}$. Then there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} = 0 \wedge [[\mathbf{v}]] = T_{\mathbf{m}_0}$.

*Proof.* Let $t \in T_{\mathbf{m}_0}$. Lemma 3 implies that there does not exist $\mathbf{w} \in \mathbb{R}_+^P$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0$ and $(\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}})[t] < 0$. Applying Proposition 11, there exists $\mathbf{v}_t$ such that $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}_t \ge 0$ and $\mathbf{v}_t[t] > 0$. Let $\mathbf{v} = \sum_{t \in T_{\mathbf{m}_0}} \mathbf{v}_t$. Then $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} \ge 0$ and $[[\mathbf{v}]] = T_{\mathbf{m}_0}$. If $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} \ge 0$ then, due to Theorem 3, $\mathbf{C}_{T_{\mathbf{m}_0}}$ would be unbounded, a contradiction. So $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} = 0$. $\square$

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

The next theorem establishes reversibility inside terminal components of the SRT of a bounded marked CPN.

**Theorem 7.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a bounded marked CPN such that for all $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, $T_{\mathbf{m}} = T_{\mathbf{m}_0}$. Then for all $\mathbf{m} \in \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, $\lim\mathbf{RS}(\mathcal{N}, \mathbf{m}) = \lim\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$.
**Proof.** Let $\mathbf{m}$ be an arbitrary marking in $\lim-\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, there exists $\mathbf{v} \in \mathbb{R}_+^{T_{\mathbf{m}_0}}$ such that $\mathbf{m} = \mathbf{m}_0 + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}$. Due to Theorem 6, there exists $\mathbf{v}' \in \mathbb{R}_+^T$ such that $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}' = 0 \wedge [[\mathbf{v}')] = T_{\mathbf{m}_0}$.

There exists some $n \in \mathbb{N}$ such that for all $t \in T_{\mathbf{m}_0}$, $n\mathbf{v}'[t] > \mathbf{v}[t]$. Thus $\mathbf{v}'' = n\mathbf{v}' - \mathbf{v} \ge 0$, $[[\mathbf{v}'']] = T_{\mathbf{m}_0}$ and $\mathbf{m}_0 = \mathbf{m} + \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v}''$. Since $T_{\mathbf{m}_0}$ is the maximal element of $\mathbf{FS}(\mathcal{N}, \mathbf{m})$, then using Theorem 2, $\mathbf{m}_0 \in \lim-\mathbf{RS}(\mathcal{N}, \mathbf{m})$. $\square$

One could ask whether this result could be strengthened with reachability instead of lim-reachability. The next proposition shows that this is not the case.

**Proposition 12.** There exists a bounded marked CPN such that for all $\mathbf{m} \in \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, $T_{\mathbf{m}} = T_{\mathbf{m}_0}$ and there exists $\mathbf{m}' \in \mathbf{RS}(\mathcal{N}, \mathbf{m})$ with $\mathbf{m} \notin \mathbf{RS}(\mathcal{N}, \mathbf{m}')$.

**Proof.** Consider the marked CPN of Figure 3 with $x = 2$. Any reachable marking $\mathbf{m}$ can be written as $\mathbf{m} = ap_1 + bp_2$ with $0 < a + 2b \le 1$, hence $T_{\mathbf{m}} = T$. Then $\mathbf{m} \xrightarrow{bt_2 \frac{a+b}{2} t_1} \mathbf{m}'$ with $\mathbf{m}' = \frac{a+b}{2} p_2$. Since the total number of tokens cannot increase, $\mathbf{m} \notin \mathbf{RS}(\mathcal{N}, \mathbf{m}')$. $\square$

## 4.3 Building the symbolic reachability tree

In order to build the SRT, we need to specify a finite representation of the sets $R_v$ and the intermediate sets (see section 4.1) that allows us to check emptiness. To do so, we introduce existential formulas of linear inequalities whose variables are either place markings denoted by $\mathbf{m}(p)$ for $p \in P$, or additional variables in a countable set $X$. Such a formula can be written as:

$$ \varphi = \exists x_1 \dots \exists x_n \bigvee_{i \le m} \bigwedge_{j \le n_i} \sum_{k \le n} a_{i,j,k} x_k + \sum_{p \in P} a_{i,j,p} \mathbf{m}(p) \bowtie_{i,j} b_{i,j} $$

where for all $i, j, k$ and $p$, $a_{i,j,k}, a_{i,j,p}, b_{i,j} \in \mathbb{Q}$ and $\bowtie_{i,j} \in \{\le, <, \ge, >, =\}$.

$\Phi(\mathcal{N})$ is the set of such formulas. Given a formula $\varphi$, $[[\varphi]]$ denotes the set of markings that satisfy $\varphi$. The emptiness of $[[\varphi]]$ can be decided in polynomial time w.r.t. the size of $\varphi$ by solving the $m$ linear programs corresponding to the clauses of the external disjunction.

Following the definition of the SRT, one observes that given a formula $\varphi$, our problem boils down to compute a formula $\varphi^*$ such that $[[\varphi^*]] = \text{closure}([[[\varphi]]])$ and given a border edge $tr$ to compute a formula $\varphi_{tr}$ such that $[[\varphi_{tr}]] = \text{succ}(tr, [[\varphi]])$.

**Proposition 13.** Let $\mathcal{N}$ be a CPN and $\varphi \in \Phi(\mathcal{N})$. Then one can compute a formula $\varphi^* \in \Phi(\mathcal{N})$ such that $[[\varphi^*]] = \text{closure}([[[\varphi]]])$ and given a border edge $tr$ a formula $\varphi_{tr} \in \Phi(\mathcal{N})$ such that $[[\varphi_{tr}]] = \text{succ}(tr, [[\varphi]])$.

**Proof.** Let $\varphi \in \Phi(\mathcal{N})$. Then $\varphi^*$ is defined by:

$$ \exists \mathbf{m}' \in \mathbb{R}_+^P \varphi[\mathbf{m}'/\mathbf{m}] \wedge \exists \mathbf{v} \in \mathbb{R}_+^T \mathbf{m} = \mathbf{m}' + \mathbf{C} \cdot \mathbf{v} \\ \wedge \bigvee_{P' \to *} \bigvee_{P'' \in \mathbf{FS}(\mathcal{N}, P')} [[\mathbf{m}')] = P' \wedge [[\mathbf{m}]] = P'' \wedge [[\mathbf{v}]] = T' $$
Here the new variables are $\mathbf{m}'$ that must fulfill $\mathbf{m}' \in [[\varphi]]$ and the Parikh vector $\mathbf{v}$ of an infinite sequence from $\mathbf{m}'$ to $\mathbf{m}$. The second line ensures that $T_{\mathbf{m}} = T_{\mathbf{m}'}$ and that combined with the state equation of the first line such an infinite sequence exists (by the characterization of lim-reachability).

Let $\varphi \in \Phi(\mathcal{N})$ and $tr = P' \xrightarrow{T'} P''$ be a border edge. Then $\varphi_{tr}$ is defined by:

$$ \exists \mathbf{m}' \in \mathbb{R}_+^P \varphi[\mathbf{m}'/\mathbf{m}] \wedge \exists \mathbf{v} \in \mathbb{R}_+^T \mathbf{m} = \mathbf{m}' + \mathbf{C} \cdot \mathbf{v} \\ \wedge [[\mathbf{m}')] = P' \wedge [[\mathbf{v}]] = T' \wedge \mathbf{m} = \wedge[[\mathbf{m}]] = P'' $$

The new variables are $\mathbf{m}'$ that must fulfill $\mathbf{m}' \in [[\varphi]]$ and the Parikh vector $\mathbf{v}$ of a repeated discounted sequence from $\mathbf{m}'$ to $\mathbf{m}$. The second line combined with the state equation of the first line ensures the existence of such a repetitive discounted sequence (due to their characterization). □

Using Proposition 13, we can associate with every vertex $v$ a satisfiable formula $\varphi_v \in \Phi(\mathcal{N})$ such that $R_v = [[\varphi_v]]$. The whole construction is performed in exponential time for two reasons. First the number of vertices of the SRT may be exponential. Then, due to the disjunctions indexed over some subset of places $P'$, $P''$ and over $\mathbf{FS}(\mathcal{N}, P')$, the size of the formulas may also be exponential. Fortunately these two factors are independent yielding a single exponential bound.

# 5 Conclusion

In order to analyze the qualitative behaviour of CPNs, we have focused on the mode of a marking: i.e., the subset of transitions fireable in the future. To do so, we have introduced transfinite firing sequences and two finite abstractions: trajectories (sequences of decreasing modes) and signatures (trajectories enlarged by witnessing markings). We have shown that w.r.t. these abstractions, transfinite sequences generate more behaviours than the infinite sequences but that transfinite sequences of ordinal less than $\omega^2$ were expressive enough.

To capture all possible signatures of a CPN, we have defined a symbolic reachability tree (SRT) where each vertex is labelled by a set of markings with same mode. We have established that the set of markings associated with the leafs of the SRT fulfill reversibility a desirable property which corresponds for instance to the long run behaviours of biological systems.

From an algorithmic point of view we have shown that the trajectory problem is NP-complete and we have designed an exponential time building of an effective representation of the SRT.

Future work will include the investigation of fairness properties related to transfinite sequences with infinite length (contrary to the ones studied here), relations with other existing dynamic models, and perspectives for control of the long-term behaviour (such as cellular reprogramming [16]).
References

1. Giann Karlo Aguirre-Samboní, Cédric Gaucherel, Stefan Haar, and Franck Pom-
mereau. Reset Petri net unfolding semantics for ecosystem hypergraphs. In *PNSE
2022*, volume 3170 of *CEUR*, pages 213–214, Bergen, Norway, July 2022.

2. Paolo Baldan, Martina Bocci, Daniele Brigolin, Nicoletta Cocco, Monika Heiner, and Marta Simeoni. Petri nets for modelling and analysing trophic networks. *Fundam. Informaticae*, 160(1-2):27-52, 2018.

3. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. The logi-
cal view on continuous Petri nets. *ACM Transactions on Computational Logic*,
18(3):24:1–24:28, 2017.

4. Claudine Chaouiya, Hanna Klaudel, and Franck Pommereau. A modular, qualitative modeling of regulatory networks using Petri nets. *Computational Biology*, 16:253–279, 2016.

5. Claudine Chaouiya, Aurélien Naldi, Elisabeth Remy, and Denis Thieffry. Petri net representation of multi-valued logical regulatory graphs. *Nat. Comput.*, 10(2):727–750, 2011.

6. Claudine Chaouiya, Elisabeth Remy, and Denis Thieffry. Petri net modelling of biological regulatory networks. *J. Discrete Algorithms*, 6(2):165–177, 2008.

7. Thomas Chatain, Stefan Haar, Loïg Jezequel, Loïc Paulevé, and Stefan Schwoon.
Characterization of reachable attractors using Petri net unfoldings. *Computational
Methods in Systems Biology*, 8859:129–142, 2014.

8. Thomas Chatain, Stefan Haar, Juraj Kolcák, Loïc Paulevé, and Aalok Thakkar.
Concurrency in boolean networks. *Natural Computing*, 19:91–109, 2020.

9. Thomas Chatain, Stefan Haar, Maciej Koutny, and Stefan Schwoon. Non-atomic transition firing in contextual nets. In *Petri Nets'2015*, volume 9115 of LNCS, pages 117–136, 2015.

10. Thomas Chatain, Stefan Haar, and Loïc Paulevé. Boolean Networks: Beyond Generalized Asynchronicity. In *AUTOMATA '18*, volume 10875 of LNCS, pages 29–42, Ghent, Belgium, June 2018.

11. Thomas Chatain, Stefan Haar, and Loïc Paulevé. Most permissive semantics of boolean networks. Research Report 1808.10240, Computing Research Repository, August 2018. 15 pages. URL: https://arxiv.org/abs/1808.10240.

12. Estíbaliz Fraca and Serge Haddad. Complexity analysis of continuous Petri nets. *Fundamenta Informaticae*, 137(1):1–28, 2015.

13. Jorge Júlvez, Laura Recalde, and Manuel Silva. On reachability in autonomous continuous Petri net systems. In *ICATPN 2003*, volume 2679 of LNCS, pages 221–240, 2003.

14. Fei Liu, George Assaf, Ming Chen, and Monika Heiner. A Petri nets-based frame-
work for whole-cell modeling. *Biosyst.*, 210:104533, 2021.

15. Fei Liu, Wujie Sun, Monika Heiner, and David Gilbert. Hybrid modelling of bi-
ological systems using fuzzy continuous Petri nets. *Briefings in Bioinformatics*,
22(1):438–450, 12 2019.

16. Hugues Mandon, Cui Su, Stefan Haar, Jun Pang, and Loïc Paulevé. Sequential reprogramming of boolean networks made practical. In *CMSB 2019*, volume 11773 of LNCS, pages 3–19, Trieste, France, September 2019.

17. Loïc Paulevé, Juraj Kolcák, Thomas Chatain, and Stefan Haar. Reconciling qualitative, abstract, and scalable modeling of biological networks. *Nature Communications*, 11(4256), August 2020.

18. Takako Takai-Igarashi. Ontology based standardization of Petri net modeling for signaling pathways. *In Silico Biol.*, 5(5-6):529-536, 2005.
A The NP-hardness of the trajectory problem

<figure><img src="image_9.png" /><figcaption>Fig. 6. The CPN corresponding to formula $(\neg x_1 \lor \neg x_3) \land (x_1 \lor \neg x_2 \lor x_3) \land (x_2 \lor \neg x_3)$.</figcaption></figure>

**Lemma 4.** *The trajectory problem is NP-hard.*

*Proof.* We reduce the 3SAT-problem to this problem. Let $\{x_1, x_2, \dots, x_n\}$ denote the set of propositions and $\{c_1, c_2, \dots, c_m\}$ denote the set of clauses. Every clause $c_j$ is defined by $c_j \triangleq lit_{j1} \lor lit_{j2} \lor lit_{j3}$ where for all $j, k$, $lit_{jk} \in \{x_1, \dots, x_n, \neg x_1, \dots, \neg x_n\}$.

W.l.o.g. we assume that for all $i, j$, $\{x_i, \neg x_i\} \not\subseteq \{lit_{j1}, lit_{j2}, lit_{j3}\}$ (otherwise $c_j$ is irrelevant and can be deleted) and for all $i$, $\{x_i, \neg x_i\} \subseteq \{lit_{jk} | j \le m, k \le 3\}$ (otherwise the variable $x_i$ is irrelevant and can be eliminated). The satisfiability problem of $\varphi = \bigwedge_{j \le m} c_j$ consists of the existence of an interpretation

$$ \nu: \{x_1, x_2, \dots, x_n\} \to \{\text{false, true}\} $$

such that for all clause $c_j$, $\nu(c_j) = \text{true}$.

Every proposition $x_i$ yields a place $b_i$ initially marked with a token (all other places are unmarked) and input of two transitions $t_i, f_i$ corresponding to the assignment associated with an interpretation. Every negated literal $\neg lit_{jk}$ yields a place $l_{jk}$ which is the output of transition $t_i$ if $lit_{jk} = \neg x_i$ or transition $f_i$ if $lit_{jk} = x_i$. For instance, in Figure 6, place $l_{11}$ corresponds to the first negated literal of the first clause (i.e., $x_1$) while place $l_{23}$ corresponds to the third negated literal of the second clause (i.e., $\neg x_3$). Every clause $c_j$ yields a transition $nc_j$ with
three input “literal” places corresponding to negated literals $\neg lit_{j_1}, \neg lit_{j_2}, \neg lit_{j_3}$. An additional place $suc$ is the output of every transition $nc_j$. Finally, transition back has $suc$ as a loop place and $b_i$ for all $i$ as output places. The reduction is illustrated in Fig. 6.

We claim there is a trajectory $T\emptyset$ if and only if $\varphi$ is satisfiable.

Let us do some preliminary observations. Due to our hypotheses, for all clause $c_j$, there exists some $\nu$ such that $\nu(c_j) = \text{false}$. Thus from the initial marking, after marking the input places of $nc_j$, it is possible to fire $nc_j$ and thus marking $suc$. Observe that given a marking $\mathbf{m}$ such that $\mathbf{m}(suc) > 0$ all transitions will be fireable in the future and $suc$ will never decrease thus $\mathbf{m}(suc) > 0$ for a lim-reachable marking once $suc$ is marked. As a consequence $T_{\mathbf{m}_0} = T$.

Assume that there exists $\nu$ such that for all clause $c_j$, $\nu(c_j) = \text{true}$. Then fire the following sequence $\sigma = 1t_1^* \dots 1t_n^*$ where $t_i^* = t_i$ when $\nu(x_i) = \text{true}$ and $t_i^* = f_i$ when $\nu(x_i) = \text{false}$. Consider $\mathbf{m}$ the reached marking. Since $\nu(c_j) = \text{true}$, at least one input place of $nc_j$ is empty in $\mathbf{m}$. Moreover $\mathbf{m}(suc) = \mathbf{m}(b_i) = 0$ for all $i$. So $\mathbf{m}$ is dead. However this does not necessarily provide the required trajectory. But the infinite firing sequence $\sigma' = (2^{-n}\sigma)_{n\ge 1}$ provides such a trajectory.

Assume that there does not exist $\nu$ such that for all clause $c_j$, $\nu(c_j) = \text{true}$.

Due to our preliminary observations, we only consider lim-reachable markings $\mathbf{m}$ such that $\mathbf{m}(suc) = 0$, i.e. when no transitions $nc_j$ have been fired. Our goal is to prove that from such a marking there is a sequence that marks place $suc$. Examining the remaining transitions, the following invariants hold. For all atomic proposition $x_i$, and reachable marking $\mathbf{m}$, one has

$$ \forall i \quad \mathbf{m}[b_i] + \sum_{lit_{jk} \in \{x_i, \neg x_i\}} \mathbf{m}[l_{jk}] \ge 1 \\ \forall j, k, j', k' \quad lit_{jk} = lit_{j'k'} \Rightarrow \mathbf{m}[l_{jk}] = \mathbf{m}[l_{j'k'}] $$

If for some $i$, $\mathbf{m}[b_i] > 0$, we fire $t_i$ in order to empty $b_i$. Thus the invariants become:

$$ \forall i \quad \sum_{lit_{jk} \in \{x_i, \neg x_i\}} \mathbf{m}[l_{jk}] \ge 1 \\ \forall j, k, j', k' \quad lit_{jk} = lit_{j'k'} \Rightarrow \mathbf{m}[l_{jk}] = \mathbf{m}[l_{j'k'}] $$

Now define $\nu$ by $\nu(x_i) = \text{true}$ if for some $lit_{jk} = \neg x_i$, $\mathbf{m}(l_{jk}) > 0$. Due to the hypothesis, there is a clause $c_j$ such that $\nu(c_j) = \text{false}$. Due to our choice of $\nu$ and the invariants, all inputs of $nc_j$ are marked. So firing $nc_j$ marks $suc$. This establishes that the single possible trajectory is $T$.

□