# Infinite and Transfinite Sequences for Continuous Petri Nets

Stefan Haar, Haddad Serge

► To cite this version:

Stefan Haar, Haddad Serge. Infinite and Transfinite Sequences for Continuous Petri Nets. 2026. hal-05486215

HAL Id: hal-05486215

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

Preprint submitted on 10 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
# Infinite and Transfinite Sequences for
Continuous Petri Nets

Stefan Haar¹, Serge Haddad²

¹ INRIA, France

² Université Paris-Saclay, 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. 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. 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 trans-
finite 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). 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.

The length of an infinite firing sequence, i.e. the cumulated amount of
firings, may be finite or infinite. Contrary to finite length infinite fir-
ing sequences, those with an infinite length may not converge and in fact
their study is more involved. First we introduce a notion of similarity and
show that every infinite length convergent firing sequence has a similar
finite length firing sequence. Then we provide a necessary and sufficient
condition for the existence of an infinite length firing sequence and an-
other one for the existence of a converging infinite length firing sequence
yielding polynomial time algorithms for checking such an existence.
# 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, informally stated as the possible long run behaviours of the system. These objects are crucial in several domains. For instance, in the context of cellular regulation, 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.

**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 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:

- 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. 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. This corresponds to the presence of *attractors* in the case of bounded *discrete* models. Indeed, while in general Petri nets, attractors may not exist, as soon as the net is bounded, the reachability graph is finite and must have finite terminal strongly connected components, which correspond to attractors. Boundedness is a reasonable assumption in the application domains; indeed, regulation, signaling and other biological networks are mass/energy bounded. Note that an efficient method for exhaustive attractor search via unfolding prefixes of safe discrete Petri nets was presented in [7].

In another direction we deepen the analysis of infinite firing sequences. The length of an infinite firing sequence, i.e. the cumulated amount of firings, may be finite or infinite. Contrary to finite length infinite firing sequences, those with an infinite length may not converge and in fact their study is more involved. First we introduce a notion of similarity and show that every infinite length convergent firing sequence has a similar finite length firing sequence. Then we provide a necessary and sufficient condition for the existence of an infinite length firing sequence and another one for the existence of a convergent infinite length firing sequence yielding polynomial time algorithms for checking such an existence.
**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. Section 5 is devoted to the study of infinite length firing sequences. Finally in Section 6, we conclude and give some perspectives to this work.

## 2 Continuous Petri nets

We will follow the terminology and notations of [12] where the omitted proofs of the results presented in this section can be found.

**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}$. Let $\mathbf{v} \in \mathbb{R}^X$ where $X$ is a finite set. Then $\|\mathbf{v}\|_\infty \triangleq \max_{x \in X} (|\mathbf{v}[x]|)$ and $\|\mathbf{v}\|_1 \triangleq \sum_{x \in X} |\mathbf{v}[x]|$.

### 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^\bullet \triangleq \bullet x \cup x^\bullet$. These notations are extended to sets of items: $\bullet X \triangleq \bigcup_{x \in X} \bullet x$, $X^\bullet \triangleq \bigcup_{x \in X} x^\bullet$ and $\bullet X^\bullet \triangleq \bigcup_{x \in X} \bullet x^\bullet$. The reverse CPN is defined by: $\mathcal{N}^{-1} \triangleq (P, T, \text{Post}, \text{Pre})$. Let $t \in T$, then $\mathbf{C}(t)$ (resp. $\text{Post}(t)$, $\text{Pre}(t)$) denotes the column vector indexed by $t$ of matrix $\mathbf{C}$ (resp. $\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.

When we will study the existence and complexity of algorithms for solving problems of marked CPNs, we require that $\mathbf{m}_0 \in \mathbb{N}^P$.
**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} \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} \mathcal{N} \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 $\kappa$ be an ordinal with $\kappa \le \omega$ and $\sigma = (\alpha_i t_i)_{i<\kappa}$ be a finite or infinite sequence over $\mathcal{Z}$. Then $|\sigma| \in \mathbb{R}_+ \cup \{\infty\}$, the length of $\sigma$, is defined by $|\sigma| = \sum_{i<\kappa} \alpha_i$.

**Definition 5.** 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}$. Then $\sigma$ is an infinite firing sequence from $\mathbf{m}_0$ if there exists an infinite family of markings $(\mathbf{m}_i)_{i \in \mathbb{N}}$ such that for all $i \in \mathbb{N}$, $\mathbf{m}_i \xrightarrow{\alpha_i t_i} \mathbf{m}_{i+1}$.

**Observation and notations.** Let $\sigma = (\alpha_i t_i)_{i \in \mathbb{N}}$ be an infinite firing sequence with $|\sigma| < \infty$. The finite length of $\sigma$ ensures the existence of $\lim_{i \to \infty} \mathbf{m}_i$ denoted by $\mathbf{m}_\omega$ and we write $\mathbf{m}_0 \xrightarrow{\sigma} \mathcal{N} \mathbf{m}_\omega$.

When there is no ambiguity about $\mathcal{N}$, $\mathbf{m} \xrightarrow{\sigma} \mathcal{N} \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} \mathbf{m}'$ 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 with finite length). Then $\bar{\sigma} \in \mathbb{R}_+^T$, the Parikh vector of $\sigma$, is defined by $\bar{\sigma}[t] \triangleq \sum_{t_i=t} \alpha_i$. Let $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$. Then the state equation $\mathbf{m} = \mathbf{m}_0 + \mathbf{C}\bar{\sigma}$ can be established by recurrence and possibly taking limits.

**Definition 6.** 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 | \sigma| < \infty \wedge \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 infinite 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 in general 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 7 (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}] | \exists \sigma \in \mathbb{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}'$.

**Definition 8.** 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 characterization of Theorem 2 is obtained by drop-
ping Condition (3) from Theorem 1. The structure of a finite firing sequence
witnessing the membership in $\mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$ was established in the proof but not
stated in the previous version of the following theorem.

**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})$.

Furthermore if $\mathbf{m} \in \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$, then there exist finite sequences $\sigma_0, \sigma_1$ such that for all $0 < \varepsilon \le 1$, there exists a finite sequence $\sigma_\varepsilon$ fulfilling:

$$
\mathbf{m}_0 \xrightarrow{\varepsilon\sigma_0} \mathbf{m}_{1,\varepsilon} \xrightarrow{\sigma_\varepsilon} \mathbf{m}_{2,\varepsilon} \xrightarrow{\varepsilon\sigma_1} \mathbf{m}
$$

with $[[\vec{\sigma}_0]] = [[\vec{\sigma}_1]] = [[\vec{\sigma}_\varepsilon]] = [[\mathbf{v}]]$

and $[[\mathbf{m}_0]] \cup \mathbf{\bullet}[[\mathbf{v}]]^\bullet = [[\mathbf{m}]] \cup \mathbf{\bullet}[[\mathbf{v}]]^\bullet = [[\mathbf{m}_{1,\varepsilon}]] = [[\mathbf{m}_{2,\varepsilon}]]$.

The structure of an infinite firing sequence witnessing the membership in
lim-**RS**(N, **m*₀) 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 for all $\varepsilon > 0$, there exist finite sequences

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

with $[[\vec{\sigma}_0]] = [[\vec{\sigma}_{1,\varepsilon}]] = [[\mathbf{v}]]$ and $[[\mathbf{m}_0]] \cup \bullet[[\vec{\sigma}_{1,\varepsilon}]] \bullet = [[\mathbf{m}_{1,\varepsilon}]]$.

Theorem 2 and its applications here motivate the following definition.

**Definition 9.** 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}]] \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}]] \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}]] \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}'$. $\square$

## 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. Its 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 a 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\ge1}$, 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_12^{-n}t_3)_{n\ge1}$. 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\ge1}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 \mathbb{Z}$, is a $\kappa$-transfinite sequence. Its length is defined by $|\sigma| = \sum_{i<\kappa} \alpha_i$. Let $\sigma = (\alpha_i t_i)_{i<\kappa}$ be a $\kappa$-transfinite sequence and $i < l' \le \kappa$. Then $\sigma_{i,l'} = (\alpha_{l''} t_{l''})_{l\le l''<l'}$.

**Definition 10.** 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 $\mathbb{Z}$ with finite length. 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'}$;

**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 11.** 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 with finite length, the Parikh vector $\vec{\sigma}$ of $\sigma = ((\alpha_i t_i)_{i<\kappa}, (\mathbf{m}_i)_{i\le\kappa})$, a transfinite firing sequence, 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}\|_{\infty} \le B\varepsilon$.

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}\|_{\infty} \le B\varepsilon$.

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

Combining Proposition 3 with Theorem 2, we obtain the following corollary.
**Corollary 1.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_l t_l)_{l<\kappa}, (\mathbf{m}_l)_{l\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{\substack{(2^{-n}\sigma_1)_{n\ge 1} \\ (2^{-n}\sigma_1)_{n<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_l t_l)_{l<\kappa}, (\mathbf{m}_l)_{l\le\kappa} \rangle$ be a $\kappa$-transfinite firing sequence. Then for all $l < l'$, $T_{\mathbf{m}_{l'}} \subseteq T_{\mathbf{m}_l}$.

*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_{l<\kappa} \mathbf{m}_l$, 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 12.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_l t_l)_{l<\kappa}, (\mathbf{m}_l)_{l\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 | 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_l t_l)_{l<\kappa}, (\mathbf{m}_l)_{l\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{\substack{(2^{-n}\sigma_{i,1})_{n\ge 1} \\ (2^{-n}\sigma_{i,1})_{n<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}]] = [[\mathbf{m}_{i,1}}]$;

- $\mathrm{sig}(\sigma') = \mathrm{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$, ..., $k\omega$.

*Proof.* We establish the result by induction 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}'} \supseteq 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_t t_t)_{t \le \kappa}, (\mathbf{m}_t)_{t \le \kappa} \rangle$ be a transfinite firing sequence with signature $((\mathbf{m}_{t_i})_{i \le k}, \mathbf{m}_{\kappa})$. Let $\sigma = \sigma_1\sigma_2$ where $\sigma_1$ leads from $\mathbf{m}_0$ to $\mathbf{m}_{t_1}$ (the second leap of $\sigma$) and $\sigma_2$ leads from $\mathbf{m}_{t_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}_{t_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}_{t_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}_{t_1}$ visited by $\sigma'$, there exists some $\mathbf{m}_{1,i}$ visited later and so $T_{\mathbf{m}'} \supseteq T_{\mathbf{m}_{1,i}} = T_{\mathbf{m}_0}$. So the only leaps of $\sigma'$ are $\mathbf{m}_0$ and $\mathbf{m}_{t_1}$ which concludes the proof. □

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 13.** 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$.

**Lemma 2.** 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 \text{lit}_{j1} \lor \text{lit}_{j2} \lor \text{lit}_{j3}$ where for all $j, k$, $\text{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 \{\text{lit}_{j1}, \text{lit}_{j2}, \text{lit}_{j3}\}$ (otherwise $c_j$ is irrelevant and can be deleted) and for all $i$, $\{x_i, \neg x_i\} \subseteq \{\text{lit}_{jk} \mid 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}, \text{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
<figure><img src="image_3.png" /><figcaption>**Fig. 2.** 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>

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 2, 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_{j1}, \neg lit_{j2}, \neg lit_{j3}$. 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. 2.

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) = \mathbf{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) = \mathbf{true}$. Then fire the following sequence $\sigma = 1t_1^* \dots 1t_n^*$ where $t_i^* = t_i$ when $\nu(x_i) = \mathbf{true}$ and $t_i^* = f_i$ when $\nu(x_i) = \mathbf{false}$. Consider $\mathbf{m}$ the reached marking. Since $\nu(c_j) = \mathbf{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) = \mathbf{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}] \geq 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}] \geq 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) = \mathbf{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) = \mathbf{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$.

□

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

*Proof.* The NP-hardness has been proved in Lemma 2. For the membership in NP, let us consider a marked CPN $(\mathcal{N}, \mathbf{m}_0)$ and a sequence $\tau = T_0...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$,

$$ \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} $$

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

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

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

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

* $\mathcal{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 $\mathcal{A}$ checks whether for all $i < K$ $P_{i,0} \cup \bullet X_i \cdot = P_{i,1}$.

* Afterwards $\mathcal{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 $\mathcal{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, $\mathcal{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} \\
\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 $\mathcal{A}$ checks in polynomial time if this linear program is satisfiable. $\square$

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

# 4 A symbolic reachability tree

In the previous section, we have studied several abstractions for a transfinite firing sequence including its signature (the finite sequence of markings starting from the initial one, ending in the final one and including the intermediate markings where the mode is decreasing). Here we generalize this approach by considering an effective abstraction of the behaviour of the CPN that captures all the possible abstract signatures. More precisely, we will formalize this abstraction in the form of a symbolic reachability tree, introduced in Subsection 4.1. In Subsection 4.2, the “reversibility” of the leaves of these trees will be established when the CPN is bounded, 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 represent 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 reachability 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 \bullet[[\vec{\sigma}_1]]\bullet$. 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'^{\bullet}$, since those are the only places that may be marked after the firing of an infinite sequence whose support is $T'$ and $P' \setminus \bullet T' \subseteq P''$ since these places remain marked after such a firing. When $P'' \not\subseteq P$ and $T_{P''} \subseteq T_{P'}$ there is an edge labelled by some $T' \subseteq T$ with (1) $\bullet T'^{\bullet} \subseteq P'$ and (2) $P' \setminus \bullet 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 14 (Abstract reachability graph).** Let $\mathcal{N}$ be a CPN. Then its abstract reachability graph $\mathbf{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 \bullet T' \subseteq P'' \subseteq P' \cup T'^{\bullet}$.

- 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) $\bullet T'^{\bullet} \subseteq P'$ and (2) $P' \setminus \bullet T' \subseteq P''$.

Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. Then its abstract reachability graph $\mathbf{ARG}(\mathcal{N}, \mathbf{m}_0)$ is the restriction of $\mathbf{ARG}(\mathcal{N})$ to the vertices reachable from $[[\mathbf{m}_0]]$.

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

*Proof.* Let $P_1 \to P_2 \to P_3$ with $P_3 \neq P_1$. So for $i \in \{1, 2\}$, there exists $T_i$ with $T_i \in \mathbf{FS}(\mathcal{N}, P_i)$ and $P_i \setminus \bullet T_i \subseteq P_{i+1} \subseteq P_i \cup T_i \bullet$. Let $T' = T_1 \cup T_2$. Then: $P_1 \setminus \bullet T' = (P_1 \setminus \bullet T_1) \setminus \bullet T_2 \subseteq P_2 \setminus \bullet T_2 \subseteq P_3 \subseteq P_2 \cup T_2 \bullet \subseteq P_1 \cup T_1 \bullet \cup T_2 \bullet = P_1 \cup T'^{\bullet}$. 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 \bullet T_1 \bullet$.

Thus $[[\mathbf{m}')] \supseteq P_2$. Since $T_2 \in \mathbf{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 \mathbf{FS}(\mathcal{N}, P_1)$. Thus $P_1 \to P_3$.

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

**Definition 15.** Let ($\mathcal{N}$, $\mathbf{m}_0$) be a marked CPN, $s = (P_i^{-} \xrightarrow{X_i} P_i^{+})_{0<i\le 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]] \to^* P_f$ when $s = \varepsilon$, and $s \neq \varepsilon$ implies
- $[[\mathbf{m}_0]] \to^* P_1^{-}$ and $P_k^{+} \to^* P_f$;
- for all $0 < i < k$, $P_i^{+} \to^* P_{i+1}$.

**Definition 16.** 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\le k}$ and $\sigma$ be a transfinite firing sequence with $\text{sig}(\sigma) = ((\mathbf{m}_i)_{i\le k}, \mathbf{m}_f)$. Then $\text{sig}(\sigma)$ is accepted by $(s, P_f)$ if for all $i \le k$, $P_i^{+} = [[\mathbf{m}_i]]$ and $P_f = [[\mathbf{m}_f]]$.

*Example 3.* Figure 3 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$). Observe that $\{p_1\} \to^* \{p_1, p_2\}$ but there is no border edge from $\{p_1\}$ to $\{p_2\}$ since $\{p_2\}$ is not included in $\{p_1\}$.

The firing sequence $\sigma = \mathbf{m}_0 \xrightarrow{t_1 t_2} \mathbf{0}$ with $\text{sig}(\sigma) = (\mathbf{m}_0 \ 1p_2 \ \mathbf{0}, \mathbf{0})$ is accepted by the following symbolic path in $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$: $c = (\{p_1, p_2\} \xrightarrow{\{t_1\}} \{p_2\} \{p_2\} \xrightarrow{\{t_2\}} \emptyset, \emptyset)$. The firing sequence $\sigma' = \mathbf{m}_0 \xrightarrow{(2^{-n}t_1 2^{-n}t_2)_{n\ge 1}} \mathbf{0}$ with $\text{sig}(\sigma') = (\mathbf{m}_0 \ \mathbf{0}, \mathbf{0})$ is accepted by $c' = (\{p_1, p_2\} \xrightarrow{\{t_1, t_2\}} \emptyset, \emptyset)$ in $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$.

Figure 4 depicts another marked CPN ($\mathcal{N}', \mathbf{m}'_0$) and its abstract reachability graph. Her again $\{p_1\} \to^* \{p_1, p_2\}$. 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{m}$, $\|\mathbf{m}\|_1 = 1$. On the other hand, if $x=2$, then $\sigma'' = \mathbf{m}_0 \xrightarrow{(2^{-n}(1t_1 1t_2))_{n\ge 1}} \mathbf{0}$ fulfills $\text{sig}(\sigma'') = (\mathbf{m}_0 \ \mathbf{0}, \mathbf{0})$.

<figure><img src="image_5.png" /><figcaption>**Fig. 3.** A marked CPN and its ARG.</figcaption></figure>
<figure><img src="image_6.png" /><figcaption>**Fig. 4.** Another marked CPN and its ARG.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>**Fig. 5.** The symbolic reachability tree of the marked CPN of Figure 3.</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 4).
Its proof is an immediate consequence of Proposition 5 and the definition of the
edges.

**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 introduce two operators on sets of markings of CPN.

**Definition 17.** 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}]] \xrightarrow{*} [[\mathbf{m}')] \wedge \mathbf{m}' \in \lim-\mathbf{RS}(\mathcal{N}, \mathbf{m})\}. $$

Let $\text{tr} = P' \xrightarrow{T'} P''$ be a border edge of $\text{ARG}(\mathcal{N})$. Then $\text{succ}(\text{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 18 (Symbolic reachability tree).** Let ($\mathcal{N}$, $\mathbf{m}_0$) be a marked CPN.
The symbolic reachability tree $\text{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 $\text{ARG}(\mathcal{N}, \mathbf{m}_0)$, inductively defined
by:
- The root $r$ is labelled by $T_r = T_{\mathbf{m}_0}$ and $R_r = \text{closure}(\{\mathbf{m}_0\})$.

- Let $v$ be a vertex labelled by $T_v$ and $R_v$. For all border edge $tr = P' \xrightarrow{T'} P''$ such that $\text{succ}(tr, R_v) \neq \emptyset$ there is a vertex $v'$ and an edge $v \xrightarrow{tr} v'$ with $T_{v'} = T_{P''}$ and $R_{v'} = \text{closure}(\text{succ}(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 3 is depicted in Figure 5. 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 vertex $v_1$ whose set of markings is such that $p_1$ is unmarked and the marking of $p_2$ lies in $[0, 1]$, and thus their common mode is $\{t_2\}$. Using the border edge $P \xrightarrow{\{t_1, t_2\}} \{p_2\}$, one reaches vertex $v_2$ whose set of markings is such that $p_1$ is unmarked and the marking of $p_2$ lies in $[0, 1[$, and thus their common mode is $\{t_2\}$. However since $t_2$ has been fired, it means that the global marking of $P$ has decreased leading to the semi-open interval $[0, 1[$ when $p_1$ becomes unmarked. 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 4 when $x = 2$ is depicted in Figure 6. 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 abstract signatures of the CPN.

<figure><img src="image_8.png" /><figcaption>**Fig. 6.** The symbolic reachability tree of the marked CPN of Figure 4 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_k}$.

*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}]]$;

- $\mathrm{sig}(\sigma') = \mathrm{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 = \mathrm{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 = [[\vec{\sigma}_{0,1}]]$. Note that $\mathrm{tr}_1 = P' \xrightarrow{X} P''$ is a border edge of $\mathrm{ARG}(\mathcal{N}, \mathbf{m}_0)$ and $\mathbf{m}_{1,0} \in \mathrm{succ}(\mathrm{tr}_1, R_r)$. Thus $\mathrm{succ}(\mathrm{tr}_1, R_r) \ne \emptyset$, and there is a vertex $v_1$ and a transition $r \xrightarrow{\mathrm{tr}_1} v_1$ with $\mathbf{m}_{1,0} \in \mathrm{succ}(\mathrm{tr}_1, R_r)$ and $\mathbf{m}_{1,1} \in \mathrm{closure}(\mathrm{succ}(\mathrm{tr}_1, R_r)) = R_{v_1}$.

By induction hypothesis, one gets a path $r \xrightarrow{\mathrm{tr}_1} v_1 \cdots \xrightarrow{\mathrm{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{\mathrm{tr}_1} v_1 \xrightarrow{\mathrm{tr}_2} \dots \xrightarrow{\mathrm{tr}_k} v_k$ in $\mathrm{SRT}(\mathcal{N}, \mathbf{m}_0)$ and $\mathbf{m}_\kappa \in R_{v_k}$. Then there exists a transfinite firing sequence $\sigma$ with $\mathrm{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 a 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 $\mathrm{tr}_k = P' \xrightarrow{X} P''$ and a marking $\mathbf{m}_k \in \mathrm{succ}(\mathrm{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 \mathrm{succ}(\mathrm{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 $\mathbf{m}$ a marking belonging to a strongly connected component (SCC) of the reachability graph of a bounded Petri net. Then for all $\mathbf{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}] = \mathbf{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_{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 \mathbf{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 \mathbf{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 \mathbf{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}] = \mathbf{P}$.

□

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 4.** 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 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 | \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] | \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 4, there is no $\mathbf{w}$ such that $\mathbf{w} \cdot \mathbf{C}_{T_{\mathbf{m}_0}} \le 0$.

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

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 4 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$

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_{m_0}$, $nv'[t] > v[t]$. Thus $v'' = nv' - v \ge 0$, $[v''] = T_{m_0}$ and $m_0 = m + C_{T_{m_0}} \cdot v''$. Since $T_{m_0}$ is the maximal element of $\mathbf{FS}(\mathcal{N}, m)$, then using Theorem 2, $m_0 \in \lim-\mathbf{RS}(\mathcal{N}, 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 4 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_m = T_{m'}$ and that combined with the state equation of the first line such an infinite sequence exists (due to the characterization of lim-reachability by Theorem 2).

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 \quad \varphi[\mathbf{m}'/\mathbf{m}] \wedge \exists \mathbf{v} \in \mathbb{R}_+^T \quad \mathbf{m} = \mathbf{m}' + \mathbf{C} \cdot \mathbf{v} \\ \wedge [[\mathbf{m}')] = P' \wedge [[\mathbf{v}]] = T' \wedge [[\mathbf{m}]] = P'' \wedge \bullet [[\mathbf{v}]] \subseteq [[\mathbf{m}')] $$

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 by Lemma 1). □

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 Infinite length firing sequences

In the previous sections we have addressed infinite (and transfinite) firing sequences with finite length. One main consequence is that such firing sequences are convergent. However infinite firing sequences with infinite length may also be convergent.

<figure><img src="image_9.png" /><figcaption>Fig. 7. A marked CPN.</figcaption></figure>

*Example 5.* Consider the marked CPN of Figure 7. $\sigma = ((\frac{1}{2n+1}t_1\frac{1}{2n+2}t_2)_{n \in \mathbb{N}}$ is an infinite convergent sequence with infinite length and limit $(1 - \log(2))p_1 + \log(2)p_2$. This limit can also be reached by the finite sequence $\sigma' = \log(2)t_1$ or by the infinite sequence $\sigma'' = (\frac{1}{(2n+1)(2n+2)}t_1)_{n \in \mathbb{N}}$ with finite length. Denoting
$(\mathbf{m}_n)_{n \in \mathbb{N}}$ the markings visited by $\sigma$, observe that $(\mathbf{m}_{2n})_{n \in \mathbb{N}}$ are exactly the markings visited by $\sigma''$. Thus in a sense that will be made precise later on, $\sigma''$ is similar to $\sigma$.

So we introduce the notion of convergence for infinite firing sequences.

**Definition 19 (infinite convergent sequences).** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = (\alpha_i t_i)_{i \in \mathbb{N}}$ be an infinite sequence over $\mathcal{Z}$. Then $\sigma$ is an infinite convergent firing sequence from $\mathbf{m}_0$ if there exists an infinite family of markings $(\mathbf{m}_i)_{i \le \omega}$ such that (1) for all $i \in \mathbb{N}$, $\mathbf{m}_i \xrightarrow{\alpha_i t_i} \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} \mathcal{N} \mathbf{m}_\omega$.

## 5.1 Similarity

In [12], the characterization of lim-reachability stated in Theorem 2 was established without requiring finite length of infinite sequences. Thus as a consequence of this theorem, for any infinite convergent sequence $\sigma$ with infinite length, there is an infinite firing sequence $\sigma'$ with same limit and finite length. However there is a priori no relation between the markings visited by $\sigma$ and $\sigma'$. Thus below we investigate what can be required for $\sigma'$ in relation with $\sigma$ formalizing the notion of similarity.

**Definition 20.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_n t_n)_{n < \omega}, (\mathbf{m}_n)_{n \le \omega} \rangle$ and $\sigma' = \langle (\alpha'_n t'_n)_{n < \omega}, (\mathbf{m}'_n)_{n \le \omega} \rangle$ be convergent infinite firing sequences. Then $\sigma$ and $\sigma'$ are similar if there exist $f, g$ increasing functions from $\mathbb{N}$ to $\mathbb{N}$ such that for all $n \in \mathbb{N}$, $\mathbf{m}_{f(n)} = \mathbf{m}'_{g(n)}$.

An immediate consequence of this definition is that two similar convergent infinite firing sequences converge to the same limit. The next lemmas will establish a bound on the length of a finite sequence witnessing the reachability of a marking.

**Lemma 5 (Lemma 13 in [12]).** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN, $\mathbf{m}$ be a marking and $\mathbf{v} \in \mathbb{R}_+^T$ that fulfill:

$$- \mathbf{m} = \mathbf{m}_0 + \mathbf{C} \cdot \mathbf{v};$$

$$- \forall p \in \bullet[[\mathbf{v}]], \mathbf{m}_0[p] > 0;$$

$$- \forall p \in [[\mathbf{v}]], \bullet, \mathbf{m}[p] > 0.$$

Then there exists a finite sequence $\sigma$ with $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$ and $\vec{\sigma} = \mathbf{v}$.

**Notations.** Let $A$ be a $I \times J$ matrix, then $\|\mathbf{A}\|_\infty \triangleq \max_{i \in I} (\sum_{j \in J} |A[i, j]|)$. Let $\mathbf{C}$ be the incidence matrix of a CPN, we introduce $B_{\mathbf{C}}$ as follows. Let $r$ be the rank of $\mathbf{C}$. If $r = 0$ (meaning $\mathbf{C} = \mathbf{0}$) then $B_{\mathbf{C}} = 1$. Otherwise $B_{\mathbf{C}}$ is the maximum of $\|\mathbf{A}^{-1}\|_\infty$ over invertible square submatrices $\mathbf{A}$ of $\mathbf{C}$.

**Lemma 6.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN, $\mathbf{m}$ be a marking and $\sigma$ be a finite sequence that fulfill:

$$- \mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m};$$
$$ - \forall p \in \bullet[[\vec{\sigma}]], \mathbf{m}_0[p] > 0; $$

$$ - \forall p \in [[\vec{\sigma}]]^{\bullet}, \mathbf{m}[p] > 0. $$

Then there exists $\sigma'$ that fulfills $|\sigma'| \le |T|B_C||\mathbf{m} - \mathbf{m}_0||_\infty$ and $\mathbf{m}_0 \xrightarrow{\sigma'} \mathbf{m}$.

*Proof.* $\mathbf{m} - \mathbf{m}_0 = \mathbf{C}_{[[v]]} \cdot \mathbf{v}_{[[v]]}$. Let $r$ be the rank of $\mathbf{C}_{[[v]]}$. If $r = 0$, the proof is immediate since $\mathbf{m} = \mathbf{m}_0$ and $\sigma'$ is the empty sequence. Assume $r > 0$ and let $\mathbf{v} = \vec{\sigma}$.

Due to linear programming theory, there exists a $P' \times T'$ invertible submatrix $\mathbf{A}$ of $\mathbf{C}_{[[v]]}$ with $|P'| = |T'| = r$ such that $\mathbf{w}$ defined by $\mathbf{A}^{-1} \cdot (\mathbf{m} - \mathbf{m}_0)[P']$ on $T'$ and $\mathbf{0}$ on $T \setminus T'$ is non negative and fulfills $\mathbf{C} \cdot \mathbf{w} = \mathbf{m} - \mathbf{m}_0$. Thus $||\mathbf{w}||_\infty \le ||\mathbf{A}^{-1}||_\infty ||\mathbf{m} - \mathbf{m}_0||_\infty \le B_C ||\mathbf{m} - \mathbf{m}_0||_\infty$ implying $||\mathbf{w}||_1 \le |T|B_C||\mathbf{m} - \mathbf{m}_0||_\infty$.
Since $[[\mathbf{w}]] \subseteq T' \subseteq [[\mathbf{v}]]$, the hypotheses of Lemma 5 are satisfied and there exists $\sigma'$ with $\vec{\sigma}' = \mathbf{w}$ such that $\mathbf{m}_0 \xrightarrow{\sigma'} \mathbf{m}$ and $|\sigma'| = ||\mathbf{w}||_1 \le |T|B_C||\mathbf{m} - \mathbf{m}_0||_\infty$.

**Lemma 7.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\mathbf{m} \in \mathbf{RS}(\mathcal{N}, \mathbf{m}_0)$. Then there exists $\sigma$ such that $|\sigma| \le (3|T|B_C + 2)||\mathbf{m} - \mathbf{m}_0||_\infty$ and $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$.

*Proof.* Let us apply Theorem 1 and select $\varepsilon$ such that:

$$ \max(||\mathbf{m}_{1,\varepsilon} - \mathbf{m}_0||_\infty, ||\mathbf{m}_{2,\varepsilon} - \mathbf{m}||_\infty, \varepsilon|\vec{\sigma}_0|, \varepsilon|\vec{\sigma}_1|) \le ||\mathbf{m} - \mathbf{m}_0||_\infty $$

Then $||\mathbf{m}_{2,\varepsilon} - \mathbf{m}_{1,\varepsilon}||_\infty \le 3||\mathbf{m} - \mathbf{m}_0||_\infty$. Applying Lemma 6, there exists $\sigma'$ with $|\sigma'| \le 3|T|B_C||\mathbf{m} - \mathbf{m}_0||_\infty$ and $\mathbf{m}_1 \xrightarrow{\sigma'} \mathbf{m}_2$.

Define $\sigma = \varepsilon\sigma_0\sigma'\varepsilon\sigma_1$. Thus $|\sigma| \le (3|T|B_C||\mathbf{m} - \mathbf{m}_0||_\infty + 2)||\mathbf{m} - \mathbf{m}_0||_\infty$ and $\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}$. $\square$

**Theorem 8.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN. For all $\sigma$ convergent infinite firing sequence there exists $\sigma'$ convergent infinite firing sequence with finite length similar to $\sigma$.

*Proof.* Let $\sigma = \langle (\alpha_n t_n)_{n<\omega}, (\mathbf{m}_n)_{n\le\omega} \rangle$. Define inductively $f$ as follows. $f(0) = 0$ and for all $n > 0$, $f(n)$ is the smallest $k > f(n-1)$ fulfilling $||\mathbf{m}_{f(n)} - \mathbf{m}_\omega||_\infty \le 2^{-n}$. Observe that for all $n > 0$, $||\mathbf{m}_{f(n+1)} - \mathbf{m}_{f(n)}||_\infty \le 2^{-n+1}$.

Since $\mathbf{m}_{f(n+1)}$ is reachable from $\mathbf{m}_{f(n)}$ for all $n > 0$, using Lemma 7, there exists $\sigma_n$ such that $|\sigma_n| \le 2^{-n+1}(3|T|B_C + 2)$. Define $\sigma_0 = (\alpha_i t_i)_{i<f(1)}$. Then the infinite sequence $(\sigma_n)_{n\in\mathbb{N}}$ converges to $\mathbf{m}_\omega$, has finite length and is similar to $\sigma$ by defining the function $g$ by $g(0) = 0$ and $g(n)$ as the length of the sequence $\sigma_0...\sigma_{n-1}$. $\square$

## 5.2 Length-divergence

When an infinite sequence has infinite-length, it means that the amount of firings of some transition(s) is infinite and we want to study what can be said about this subset of transitions. This motivates the next definition.
**Definition 21.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = (\alpha_n t_n)_{n \in \mathbb{N}}$ be an infinite sequence. Then $\mathrm{Div}(\sigma) \triangleq \{t \in T \mid \sum_{n|t_n=t} \alpha_n = \infty\}$.

**Notation.** A positive T-semiflow is a vector $\mathbf{v} \in \mathbb{R}_+^T$ such that $\mathbf{C} \cdot \mathbf{v} = 0$.

**Theorem 9.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma = \langle (\alpha_n t_n)_{n<\omega}, (\mathbf{m}_n)_{n<\omega} \rangle$ be an infinite firing sequence. Assume that there exists a increasing function from $\mathbb{N}$ to $\mathbb{N}$ such that $(\mathbf{m}_{f(n)})_{n \in \mathbb{N}}$ is convergent. Then there is a positive T-semiflow $\mathbf{v}$ fulfilling $[[\mathbf{v}]] = \mathrm{Div}(\sigma)$.

*Proof.* Let $\sigma = (\alpha_n t_n)_{n \in \mathbb{N}}$. If $\mathrm{Div}(\sigma) = \emptyset$ then $\mathbf{v} = \mathbf{0}$. Assume that $\mathrm{Div}(\sigma) \neq \emptyset$ and pick some $t \in \mathrm{Div}(\sigma)$. Let $g$ an increasing function from $\mathbb{N}$ to $\mathbb{N}$ such that such that for all $n \in \mathbb{N}$, $\sum_{g(f(n+1)) \le i < g(f(n))|t_i=t} \alpha_i \ge 1$.

For all $t' \in T$, denote $\lambda_n(t') = \sum_{g(f(n)) \le i < g(f(n+1))|t_i=t'} \alpha_i$.

Thus for all $n$, $\lambda_n(t) \ge 1$.

Observe that

$$-\mathbf{C}(t) = \frac{1}{\lambda_n(t)} \left( \mathbf{m}_{g(f(n+1))} - \mathbf{m}_{g(f(n))} + \sum_{t_i \in \mathrm{Div}(\sigma) \setminus \{t\}} \lambda_n(t_i) \mathbf{C}(t_i) + \sum_{t_i \notin \mathrm{Div}(\sigma)} \lambda_n(t_i) \mathbf{C}(t_i) \right)$$

Letting $n$ got to $\infty$ one gets:

$$-\mathbf{C}(t) = \lim_{n \to \infty} \sum_{t_i \in \mathrm{Div}(\sigma) \setminus \{t\}} \frac{\lambda_n(t_i)}{\lambda_n(t)} \mathbf{C}(t_i)$$

Thus $-\mathbf{C}(t)$ belongs to the closure of $\{\mathbf{C} \cdot \mathbf{v} \mid [[\mathbf{v}]] \subseteq \mathrm{Div}(\sigma) \setminus \{t\}\}$. Due to linear programming theory, this set is closed, thus there exists $\mathbf{v}_t$ with $[[\mathbf{v}_t]] \subseteq \mathrm{Div}(\sigma) \setminus \{t\}$ such that $-\mathbf{C}(t) = \mathbf{C} \cdot \mathbf{v}_t$. Let $\mathbf{w}_t = \mathbf{v}_t + 1 \cdot t$, $\mathbf{w}_t$ is a positive T-semiflow with $t \in [[\mathbf{w}_t]] \subseteq \mathrm{Div}(\sigma)$. So $\mathbf{v} = \sum_{t \in \mathrm{Div}(\sigma)} \mathbf{w}_t$ is the required vector. $\square$

**Corollary 2.** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $\sigma$ be an infinite convergent sequence. Then there is a positive T-semiflow $\mathbf{v}$ fulfilling $[[\mathbf{v}]] = \mathrm{Div}(\sigma)$.

*Example 6.* Consider the marked CPN of Figure 7 and $\sigma = ((\frac{1}{2n+1}t_1 \frac{1}{2n+2}t_2)_{n \in \mathbb{N}}$ a convergent infinite sequence with $\mathrm{Div}(\sigma) = \{t_1, t_2\}$. $\mathbf{v} = 1 \cdot t_1 + 1 \cdot t_2$ is a positive T-semiflow.

The following proposition will be useful to characterize the existence of an infinite-length (convergent) firing sequence.

**Proposition 14 (a statement of Proposition 18 in [12]).** Let $(\mathcal{N}, \mathbf{m}_0)$ be a marked CPN and $U \in \mathrm{FS}(\mathcal{N}, \mathbf{m}_0)$. Then there exists $\sigma = \alpha_1 t_1 \cdots \alpha_k t_k$ with $U = \{t_1, \dots, t_k\}$ and $\mathbf{m}_1$ such that:

$$\mathbf{m}_0 \xrightarrow{\sigma} \mathbf{m}_1 \text{ and } [[\mathbf{m}_1]] = [[\mathbf{m}_0]] \cup \bullet \bullet \bullet$$
**Theorem 10.** A marked CPN ($\mathcal{N}$, $\mathbf{m}_0$) admits an infinite-length convergent firing sequence if and only if there exists $\mathbf{v} \in \mathbb{R}_+^{T_{\mathbf{m}_0}}$ such that $\mathbf{v} \neq \mathbf{0}$ and $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} = \mathbf{0}$.

*Proof.*

**Necessity.** Assume there exists $\sigma$ an infinite length convergent sequence. Due to Corollary 2, there exists $\mathbf{v} \in \mathbb{R}_+^T$ such that $[[\mathbf{v}]] = \text{Div}(\sigma)$ and $\mathbf{C} \cdot \mathbf{v} = \mathbf{0}$. Since $\text{Div}(\sigma) \neq \emptyset$ and $\text{Div}(\sigma) \subseteq T_{\mathbf{m}_0}$, the necessity is established.

**Sufficiency.** By definition of $T_{\mathbf{m}_0}$ and Proposition 14, there exists a firing sequence $\sigma_0$ such that $\mathbf{m}_0 \xrightarrow{\sigma_0} \mathbf{m}_1$ with $[[\mathbf{m}_1]] = [[\mathbf{m}_0]] \cup \mathbf{T}_{\mathbf{m}_0}$. Let $T_{\mathbf{m}_0} = \{t_1, \dots, t_k\}$ and $\mathbf{v} = \sum_{i \le k} \alpha_i t_i$ and for $n > 0$, $\sigma_n = \frac{\alpha_1}{n} t_1 \cdots \frac{\alpha_k}{n} t_k$. There exists some $n_0$ such that for all $n \ge n_0$, this sequence is fireable in $\mathbf{m}_1$ and $\mathbf{m}_1 \xrightarrow{\sigma_n} \mathbf{m}_1$. Let $\sigma = \sigma_0(\sigma_n)_{n \ge n_0}$. $\sigma$ is an infinite firing sequence with $|\sigma| = |\sigma_0| + (\sum_{1 \le i \le k} \alpha_i)(\sum_{n \ge n_0} \frac{1}{n}) = \infty$. For all $\varepsilon > 0$, there exists $n_1 \ge n_0$ such that $\|\mathbf{C}\|_{\infty} \|\vec{\sigma}_n\|_{\infty} \le \varepsilon$. Thus for all $\sigma'$, finite prefix of $\sigma$ and suffix of $\sigma_0(\sigma_n)_{n \le n_1}$ and $\mathbf{m}'$ such that $\mathbf{m}_0 \xrightarrow{\sigma'} \mathbf{m}'$, $\|\mathbf{m}' - \mathbf{m}_1\|_{\infty} \le \varepsilon$. So $\sigma$ is an infinite-length convergent firing sequence.

□

**Corollary 3.** The existence of an infinite-length convergent firing sequence in a marked CPN ($\mathcal{N}$, $\mathbf{m}_0$) is decidable in polynomial time.

*Proof.* $T_{\mathbf{m}_0}$ is computable in polynomial time (Corollary 19 in [12]). Thus the existence is decided by solving the linear program:

$$ \max \left( \sum_{t \in T_{\mathbf{m}_0}} \mathbf{v}[t] \mid \mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} = \mathbf{0} \wedge \mathbf{v} \ge \mathbf{0} \right) $$

which can be done in polynomial time and checking whether this maximum is null.

□

Omitting the convergence for infinite-length firing sequence, one gets a similar characterization:

**Theorem 11.** A marked CPN ($\mathcal{N}$, $\mathbf{m}_0$) admits an infinite-length firing sequence if and only if there exists $\mathbf{v} \in \mathbb{R}_+^{T_{\mathbf{m}_0}}$ such that $\mathbf{v} \neq \mathbf{0}$ and $\mathbf{C}_{T_{\mathbf{m}_0}} \cdot \mathbf{v} \ge \mathbf{0}$.

*Proof.*

**Necessity.** Assume there exists $\sigma = \langle (\alpha_n t_n)_{n < \omega}, (\mathbf{m}_n)_{n < \omega} \rangle$ an infinite length firing sequence. Observe that $(\mathbb{R}_+ \cup \{\infty\})^P$ is a compact set using Alexandroff extension. Thus by compactness, there exist a increasing function $f$ from $\mathbb{N}$ to $\mathbb{N}$ with $f(0) = 0$ and a decomposition of $P$ in $P_1 \uplus P_2$ such that $\sigma = (\sigma_n)_{n \in \mathbb{N}}$ with $\sigma_n = (\alpha_i t_i)_{f(n) \le i < f(n+1)}$ a finite sequence fulfilling $\mathbf{m}_{f(n)} \xrightarrow{\sigma_n} \mathbf{m}_{f(n+1)}$ and for all $p \in P_1$, $(\mathbf{m}_{f(n)}(p))_{n \in \mathbb{N}}$ is convergent, and for all $p \in P_2$ and all $n$, $\mathbf{m}_{f(n+1)}(p) \ge \mathbf{m}_{f(n)}(p) + 1$.
If $P_2 = \emptyset$ then $\sigma$ fulfills the hypotheses of Theorem 9 which implies the existence of $\mathbf{v} \in \mathbb{R}_+^{T_{m_0}}$ such that $\mathbf{v} \neq \mathbf{0}$ and $\mathbf{C}_{T_{m_0}} \cdot \mathbf{v} = \mathbf{0}$.

Assume that $P_2 \neq \emptyset$. Denote $\lambda_n = \sum_{p \in P_2} \mathbf{m}_{n+1}(p) - \mathbf{m}_n(p)$. Observe that $\lambda_n \ge 1$. Define $\mathbf{w}_n = \frac{1}{\lambda_n} \mathbf{C} \cdot \vec{\sigma}_n$. Observe that $\sum_{p \in P_2} \mathbf{w}_n(p) = 1$, for all $p \in P_2$, $\mathbf{w}_n(p) \ge 0$ and for all $p \in P_1$, $\lim_{n \to \infty} \mathbf{w}_n(p) = 0$ (since $\lambda_n \ge 1$). Focusing on $P_2$, we can extract a subsequence $f(n)$ such that for all $p \in P_2$, $(\mathbf{w}_{f(n)}(p))_{n \in \mathbb{N}}$ is convergent. Thus $\mathbf{w}_{f(n)}$ converges to a non negative vector say $\mathbf{w}_{\infty}$ null on $P_1$ and fulfilling $\sum_{p \in P_2} \mathbf{w}_{\infty}(p) = 1$. Since $\{\mathbf{C}_{T_{m_0}} \cdot \mathbf{v} | \mathbf{v} \in \mathbb{R}_+^{T_{m_0}}\}$ is a closed set, there exists $\mathbf{v} \in \mathbb{R}_+^{T_{m_0}}$ such that $\mathbf{C}_{T_{m_0}} \cdot \mathbf{v} = \mathbf{w}_{\infty} \ge \mathbf{0}$ implying $\mathbf{v} \neq \mathbf{0}$.

**Sufficiency.** By definition of $T_{m_0}$ and Proposition 14, there exists a firing sequence $\sigma_0$ such that $\mathbf{m}_0 \xrightarrow{\sigma_0} \mathbf{m}_1$ with $[[\mathbf{m}_1]] = [[\mathbf{m}_0]] \cup \bullet T_{m_0}$. Let $T_{m_0} = \{t_1, \dots, t_k\}$ and $\mathbf{v} = \sum_{i \le k} \alpha_i t_i$ and for $n > 0$, $\sigma_n = \frac{\alpha_1}{n} t_1 \cdots \frac{\alpha_k}{n} t_k$. There exists some $n_0$ such that for all $n \ge n_0$, this sequence is fireable in $\mathbf{m}_1$. So $\mathbf{m}_1 \xrightarrow{\sigma_{n_0}} \mathbf{m}_2$ with $\mathbf{m}_2 \ge \mathbf{m}_1$. Thus the sequence $\sigma_0(\sigma_{n_0})^\omega$ is an infinite-length firing sequence. $\square$

**Corollary 4.** *The existence of an infinite-length firing sequence in a marked CPN $(\mathcal{N}, \mathbf{m}_0)$ is decidable in polynomial time.*

*Proof.* $T_{m_0}$ is computable in polynomial time (Corollary 19 in [12]). Thus the existence is decided by solving the linear program:

$$ \max \left( \sum_{t \in T_{m_0}} \mathbf{v}[t] \mid \mathbf{C}_{T_{m_0}} \cdot \mathbf{v} \ge \mathbf{0} \wedge \mathbf{v} \ge \mathbf{0} \right) $$

which can be done in polynomial time and checking whether this maximum is null. $\square$

# 6 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 infinite sequences, but within transfinite sequences, those of ordinal less than $\omega^2$ were expressive enough.

The symbolic reachability tree (SRT) we have introduced captures all possible signatures of a CPN. We have established that for bounded CPNs the set of markings associated with the leafs of the SRT satisfy reversibility, a desirable property corresponding e.g. to attractors of biological systems.
From an algorithmic point of view, we have shown that the trajectory problem is NP-complete. In addition, we have designed an exponential time building of an effective representation of the SRT.

We have introduced a notion of similarity and shown that every infinite length converging firing sequence has a similar finite length firing sequence. Finally we have provided a necessary and sufficient condition for the existence of an infinite length firing sequence and another one for the existence of a converging infinite length firing sequence yielding polynomial time algorithms for checking such an existence.

Several lines of future work remain to be explored. From a theoretical point of view, we plan to enlarge the study of infinite and transfinite sequences: investigation of *fairness* properties, transfinite sequences with multiple accumulation points, etc. On a more abstract level, the relations between CPN models with other existing dynamic models for biological networks are a major issue; we also hope to gain new perspectives for the *control* of the long-term behaviour (e.g. in *cellular reprogramming* [16] and medical therapies).
## References

1. Giann Karlo Aguirre-Samboní, Cédric Gaucherel, Stefan Haar, and Franck Pommereau. 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 logical 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 framework for whole-cell modeling. *Biosyst.*, 210:104533, 2021.

15. Fei Liu, Wujie Sun, Monika Heiner, and David Gilbert. Hybrid modelling of biological 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.