# Home Spaces and Semiflows for the Analysis of Parameterized Petri Nets

Gerard Memmi

► To cite this version:

Gerard Memmi. Home Spaces and Semiflows for the Analysis of Parameterized Petri Nets. PNSE'25: 46th International Conference on Application and Theory of Petri Nets and Concurrency: Petri Nets and Software Engineering, SAFER team from Laboratoire d'Informatique de Paris Nord (LIPN), Université Sorbonne Paris; MeFoSyLoMa group, Jun 2025, PARIS, France. pp.97-113. hal-05236348

HAL Id: hal-05236348

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

Submitted on 2 Sep 2025

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
# Home Spaces and Semiflows for the Analysis of Parameterized Petri Nets

Gerard Memmi¹,*

¹LTCI, Telecom-Paris, Institut polytechnique de Paris, Palaiseau, France

**Abstract**

After briefly recalling basic notations of Petri Nets, home spaces, and semiflows, we focus on $F^+$, the set of semiflows with non-negative coordinates where the notions of minimality of semiflows and minimality of supports are particularly critical to develop an effective analysis of invariants and behavioral properties of Petri Nets such as boundedness or even liveness. We recall known behavioral properties attached to the notion of semiflows that we associate with extremums. We also recall three known decomposition theorems considering $N, Q^+$, and $Q$ respectively where the decomposition over $N$ is being improved with a necessary and sufficient condition.

Then, we regroup a number of properties (old and new) especially around the notions of home spaces and home states which, in combination with semiflows, are used to efficiently support the analysis of behavioral properties.

We introduce a new result on the decidability of liveness under the existence of a home state. We introduce new results on the structure and behavioral properties of Petri Nets, illustrating again the importance of considering generating sets of semiflows with non-negative coordinates.

As examples, we present two related Petri Net modeling arithmetic operations (one of which represents an Euclidean division), illustrating how results on semiflows and home spaces can be methodically used in analyzing the liveness of the parameterized model and underlining the efficiency brought by the combination of these results to the verification engineer.

**Keywords**

Semiflows, Home spaces, Home states, Petri Nets, Generating Sets, Invariants, Boundedness, Liveness

# 1. Introduction

## 1.1. Motivations

Parallel programs, distributed digital systems, telecommunication networks, or cyber-physical systems are entities that are complex to design, model, and verify. Using formal verification at different stages of the system development life cycle is a strong motivation and provides us with the rationale for revisiting the notions of semiflows and home spaces and illustrate through examples how they can be combined to analyze behavioral properties of Petri Nets. In this regard, invariants are of paramount importance as they are almost systematically used in system specifications to describe specific behavioral properties. One can argue that properties such as liveness, deadlock freeness, or boundedness are in some way invariants since they must hold regardless of the evolution of the digital system under study.

Often, engineers and researchers will try to prove that a formula belonging to a system specification is an invariant, meaning that the formula holds during any possible evolution of their model. But, can we find a way by which invariants or at least a meaningful subset of invariants can be organized and concisely described, and some of them can be discovered by computation? Such invariants that do not belong in the system specification, can just express a sub-property of a more complex known one; however, they also can reveal an under-specified model or an unsuspected function of the system under study (which in turn, could constitute a component of a security breach). In this paper, we provide some elements to answer this question especially through the notions of generating sets and minimality.

PNSE'25, *International Workshop on Petri Nets and Software Engineering*, 2025

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

gerard.memmi@telecom-paris.fr (G. Memmi)

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

0000-0002-3380-8394 (G. Memmi)

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

© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

<footnote>* Corresponding author.</footnote>
Then, we show how basic arithmetic, linear algebra, or algebraic geometry can efficiently support invariant calculus.

One of our motivations is to go beyond regrouping and rewriting in a unified manner a number of known algebraic results dispersed throughout the Petri Nets literature and introduce improved or new results. How can invariants be combined to represent meaningful behaviors? We will address this question by combining results on home spaces and invariants and illustrate how engineers can proceed through two examples.

This paper can be considered as a continuation of the work started in [1], providing new results particularly on home spaces as well as new examples. We want to show how linear algebra or algebraic geometry can efficiently sustain invariant calculus and can be applied and utilized to prove a large variety of behavioral properties, sometimes with simple arithmetic reasoning. When Petri Net or colored Petri Nets ([2]) are parameterized, this type of reasoning can be useful to determine in which domain of these parameters, behavioral properties can be satisfied.

## 1.2. Outline and contributions

After providing basic notations in Section 2 and grouping a first set of classic properties for semiflows (in $Z$ or $N$) and introducing two extremums in Section 3, the notions of generating sets and minimality are briefly recalled from [1] in Section 4.

The three decomposition theorems of Section 4.2 have been first published in [3] then improved in [1]. Here, the first theorem is extended once more into a necessary and sufficient condition (instead of just a necessary condition in our previous papers) to fully characterize minimal semiflows and generating sets over $N$. The other two theorems are just recalled for completeness.

Then, the notion of home space is described Section 5 with a set of old and new results linked to their structure and later to their key relation with liveness in Section 5.2. In particular, a new decidability result is provided for Petri Nets with home states linked to Karp and Miller's coverability tree finite construction.

Subsequently, Theorem 5 is using a generating set to compute three extremums. This result does not depend on the chosen generating set. These important details were never stressed out before despite their importance from a computational point of view, and their impact in supporting the analysis of parameterized models.

These results are used in the analysis of two examples presented in Section 6 where two parameterized examples are given to illustrate how invariants and home spaces can be associated with basic arithmetic reasoning to methodically prove behavioral properties of a Petri Net (described section 6.1).

Section 7 concludes and provides a possible avenue for future research.

## 2. Basic notations

In this section, we briefly recall Petri Nets, including the notion of potential state space that is usual in Transition Systems, introducing notations that will be used in this paper. Then, we define semiflows in $Z$ and basic properties in $N$ highlighting why semiflows in $N$ may be considered more useful to analyze behavioral properties.

A Petri Net is a tuple $PN = \langle P, T, Pre, Post \rangle$, where $P$ is a finite set of *places* and $T$ a finite set of *transitions* such that $P \cap T = \emptyset$. A transition $t$ of $T$ is defined by its $Pre(\cdot, t)$ and $Post(\cdot, t)$ conditions[^1]: $Pre: P \times T \to N$ is a function providing a weight for pairs ordered from places to transitions, while $Post: P \times T \to N$ is a function providing a weight for pairs ordered from transitions to places. Here, $d$ will denote the number of places: $d = |P|$.

A marking (or state in Transition Systems) $q: P \to N$ allows representing the evolution of the system along the execution (or firing) of a transition $t$ or of a sequence of transitions $\sigma$ (i.e., a word in

<footnote>[^1]: We use here the usual notation: $Pre(\cdot, t)(p) = Pre(p, t)$ and $Post(\cdot, t)(p) = Post(p, t)$.</footnote>
$T^*$). We say that $t$ is enabled at marking $q$ if and only if $q \ge Pre(\cdot, t)$, and as an enabled transition at $q$ (we write that $q \in Dom(t)$), $t$ can be executed, reaching a marking $q'$ from $q$ such that:

$$q' = q + Post(\cdot, t) - Pre(\cdot, t).$$

This is also denoted as $q' = t(q)$ or more traditionally $q \xrightarrow{t} q'$ (we also write $q' \in Im(t)$). Similarly, for a sequence of transitions $\sigma$ allowing to reach a marking $q'$ from a marking $q$, we write $q \xrightarrow{\sigma} q'$. When the sequence of transitions allowing to reach a marking $q'$ from a marking $q$ is unknown, we may write $q \xrightarrow{*} q'$. Given a marking $q$, a place $p$ is said to contain $k$ tokens as $q(p) = k$.

We also define $Q$, the set of all potential markings (also known as state space in Transition Systems). Without additional information on the domain in which markings may vary, we assume $Q = \mathbb{N}^d$.

$RS(PN, Init)$ denotes the set of reachability of a Petri Net $PN$ from a subset $Init$ of $Q$: $RS(PN, Init) = \{q \in Q | \exists a \in Init, a \xrightarrow{*} q\}$.

$RG(PN, Init)$, and $LRG(PN, Init)$ denote the reachability graph without labels (as in Figure 2) and with labels in $T$ respectively; while $LCT(PN, q_0)$ denote the labeled coverability tree given an initial marking $q_0$.

### 3. Petri Nets and Semiflow basic properties

The concept of semiflows over non negative integers were first described by Y.E. Lien [4] and independently by K. Lautenbach and H. A. Schmid [5]. The algebraic calculus underneath can be find in [6]. Then, M. Silva [7] extended the definition to semiflows over integers. After recalling the definition of semiflows, we gather four properties illustrating their link with behavioral properties.

In this section, we consider a Petri Net $PN$ with its initial marking $q_0$ and the set of reachable markings from $q_0$ through all sequences of transitions denoted by $RS(PN, q_0)$.

**definition 1 (Semiflow).** A Semiflow $f$ is a solution of the following homogeneous system of $|T|$ diophantine equations:

$$f^{\top} Post(\cdot, t) = f^{\top} Pre(\cdot, t), \quad \forall t \in T, \qquad (1)$$

where $x^{\top}y$ denotes the scalar product of the two vectors $x$ and $y$, since $f, Pre(\cdot, t)$ and $Post(\cdot, t)$ can be considered as vectors once the places of $P$ have been ordered.

$\mathcal{F}$ and $\mathcal{F}^+$ denote the sets of solutions of the system of equations (1) that have their coefficients in $\mathbb{Z}$ and in $\mathbb{N}$, respectively.

Any non-null solution $f$ of the homogeneous system of equations (1) allows to directly deduce the following invariant of $PN$ defined by its $Pre$ and $Post$ functions (used in the system of equations (1) that $f$ satisfies):

$$\forall q \in RS(PN, q_0) : f^{\top} q = f^{\top} q_0. \qquad (2)$$

In the rest of the paper, we abusively use the same symbol '0' to denote $(0, ..., 0)^{\top}$ of $\mathbb{N}^n$, for all $n$ in $\mathbb{N}$. The support of a semiflow $f$ is denoted by $\|f\|$ and is defined by

$$\|f\| = \{x \in P | f(x) \neq 0\}.$$

We will use the usual component-wise partial order in which $(x_1, x_2, ..., x_d)^{\top} \le (y_1, y_2, ..., y_d)^{\top}$ if and only if $x_i \le y_i$, for all $i \in \{1, ..., d\}$.

The most interesting set of semiflows, from a behavioral analysis standpoint, is $\mathcal{F}^+$, defined over natural numbers. This can be seen through the following three properties. First, we define the positive and negative supports of a semiflow $f \in \mathcal{F}$ as:

$$\|f\|_{+} = \{p \in P | f(p) > 0\}$$

and

$$\|f\|_{-} = \{p \in P | f(p) < 0\},$$
with $||f|| = ||f||_{-} \cup ||f||_{+}$. We can then rewrite Equation (2) as:

$$f^{\top} q = \left| \sum_{p \in ||f||_{+}} f(p) q(p) \right| - \left| \sum_{p \in ||f||_{-}} f(p) q(p) \right| = f^{\top} q_{0}. \quad (3)$$

As we can see, the formulation of Equation (3) is a subtraction between the weighted number of tokens in the places belonging to the positive support and the weighted number of tokens in the places belonging to the negative support of $f$. This expression allows deducing an invariant since, by Equations (3), it remains constant during the evolution of the Petri Net. A first general property can be immediately deduced by recalling that any marking $q$ belongs to $\mathbb{N}^d$ and that a subset $A$ of places is bounded.

**property 1.** For any semiflow $f \in \mathcal{F}$, $||f||_{+}$ is bounded if and only if $||f||_{-}$ is bounded.

Of course, if $||f||_{-} = \emptyset$, then $f \in \mathcal{F}^{+}$ and $||f||$ is necessarily *structurally bounded* (i.e., bounded from any initial marking) and is sometime called *conservative component* as in [8]. More generally, considering a weighting function $f$ over $P$ being defined over non-negative integers and verifying the following system of inequalities:

$$f^{\top} Post(\cdot, t) \le f^{\top} Pre(\cdot, t), \quad \forall t \in T, \quad (4)$$

the following properties can be easily proven [3]:

**property 2.** If $f \ge 0$ is such that it verifies Equation (4), then the set of places of $||f||$ is *structurally bounded*.

Moreover, the marking of any place $p$ of $||f||$ has an upper bound:

$$q(p) \le \frac{f^{T} q_{0}}{f(p)}, \quad \forall q \in RS(PN, q_{0}).$$

If $f > 0$, then $||f||_{+} = ||f|| = P$, and the Petri Net is also *structurally bounded*. The reverse is also true: if the Petri Net is *structurally bounded*, then there exists a strictly positive solution for the system of inequalities above (see [9] or [10]). This property is actually false for a semiflow that satisfies Equation (1) but would have at least one negative coordinate, and constitutes a first reason for particularly considering weight functions $f$ over $P$ being defined over non-negative integers including $\mathcal{F}^{+}$. We can then define $\Lambda$, the set of all possible bounds generated by semiflows:

$$\Lambda(p, q_0) = \{x \in \mathbb{Q}^{+} \mid \exists f \in \mathcal{F}^{+}, x = \frac{f^{T} q_0}{f(p)}\}$$

and its extremum (and more useful element):

$$\lambda(p, q_0) = \min_{\{f \in \mathcal{F}^{+} \mid f(p) \neq 0\}} \frac{f^{\top} q_0}{f(p)}$$

The following corollary can be directly deduced from the fact that any semiflow in $\mathcal{F}^{+}$ satisfies the system of inequalities (4); therefore, Property 2 can apply:

**corollary 1.** For any place $p$ belonging to at least one support of a semiflow of $\mathcal{F}^{+}$, an upper bound $\lambda$ can be defined for the marking of $p$ relatively to an initial marking $q_0$ such that:

$$\forall q \in RS(PN, q_0), \quad q(p) \le \lambda(p, q_0) = \min_{\{f \in \mathcal{F}^{+} \mid f(p) \ne 0\}} \frac{f^{\top} q_0}{f(p)}.$$

We will see with Theorem 5 that this bound is computable as a consequence of Theorems 1 and 3.
**definition 2.** Given a transition t and a semiflow f in $\mathcal{F}^+$, the scalar product $f^T Pre(\cdot, t)$ is called the f-enabling threshold oft.

Sometimes, when there is no ambiguity, $f^T Pre(\cdot, t)$ is more simply called the enabling threshold of t as in [10]. In [11] P-290, we can find, through an example, a similar notion named as “non-fireability condition”.

This gives us a second reason for particularly considering a semiflow f as being defined over non-negative integers is that the system of inequalities

$$f^T q_0 \geq f^T Pre(\cdot, t), \quad \forall t \in T, \qquad (5)$$

becomes a necessary condition for any transition t to stand a chance to be enabled from any reachable marking from $q_0$, then to be live. Equation (5) motivates the definition 2.

**property 3.** If t is a transition and $f \in \mathcal{F}^+ \setminus \{0\}$ such that $f^T q_0 < f^T Pre(\cdot, t)$, then t cannot be executed from $\langle PN, q_0 \rangle$.

More generally, a necessary condition for a transition t to be executed at least once from $\langle PN, q_0 \rangle$ is

$$1 \leq \min_{\{f \in \mathcal{F}^+ | f^T Pre(\cdot, t) \neq 0\}} \frac{f^T q_0}{f^T Pre(\cdot, t)}$$

We can define $\Theta$ stemming from property 3 the same way we defined $\Lambda$ stemming from property 2:

$$\Theta(t, q_0) = \{x \in \mathbb{Q}^+ | \exists f \in \mathcal{F}^+, x = \frac{f^T q_0}{f^T Pre(\cdot, t)}\}$$

with its extremum $\theta$ the inequality of property 3 can rewritten such that:

$$1 \leq \theta(t, q_0) = \min_{\{x \in \Theta\}} x$$

Property 3 is not a sufficient condition for a transition to be enabled, see figure 1.

<figure><img src="image_5.png" /><figcaption>**Figure 1:** $\mathcal{F}^+ = \mathbb{N}^2$, $Pre(A, t1) = 2$, $q_0(A) = 1$, $q_0(B) = 2$. We can verify that $1 \leq \theta(t1, q_0) = 3/2$ yet $t1$ cannot be executed from $q_0$.</figcaption></figure>

Property 3 is of interest when the model is defined with parameters, since some values of these parameters for which the model is not live can be rapidly pruned away (see example Figure 3). Moreover, it also says that the only way (without changing the structure of the model) to make the execution of t possible is by adding tokens in $\|f\|$ for any semiflow f for which inequality (5) is not satisfied. We conjecture that the notion of siphon [11] could be useful here to improve property 2.

At last, the following known property ([3], [10], or [12]) can easily be proven true in $\mathcal{F}^+$ and not true in $\mathcal{F}$:

**property 4.** If f and g are two semiflows with non-negative coefficients, then we have: $\|f + g\| = \|f\| \cup \|g\|$.

If $\alpha$ is a non-null integer then $\|\alpha f\| = \|f\|$.

This property is used to prove theorem 3 section 4.2 and theorem 5 section 5.3. These results have been cited and utilized many times in various applications going beyond computer science, electrical engineering, or software engineering. For instance, they have been used in domains such as population protocols [13] or biomolecular chemistry relative to chemical reaction networks [14], which brings us back to the C. A. Petri's original vision, when he highlighted that his nets could be used in chemistry. Many other applications can be found in the literature.
# 4. Generating sets and minimality

The notion of generating sets for semiflows is well known and efficiently supports the handling of an important class of invariants. Several results have been published, starting from the initial definition and structure of semiflows [6] to a wide array of applications used especially to analyze Petri Nets [11, 15, 14, 16].

Minimality of semiflows and minimality of their supports are critical to understand how to best decompose semiflows. Invariants directly deduced from minimal semiflows relate to smaller weighted quantities of resources, simplifying the analysis of behavioral properties. Furthermore, the smaller the support of semiflows, the more local their footprint (i.e., the more constrained the potential exchanges between resources is). In the end, these two notions of minimality will foster analysis optimization.

## 4.1. Three definitions

**definition 3 (Generating set).** A subset $\mathcal{G}$ of $\mathcal{F}^+$ is a generating set over a set $\mathcal{S}$ (where $\mathcal{S} \in \{\mathbb{N}, \mathbb{Q}^+, \mathbb{Q}\}$ with $\mathbb{Q}^+$ denoting the set of non-negative rational numbers) if and only if for all $f \in \mathcal{F}^+$, we have $f = \sum_{g_i \in \mathcal{G}} \alpha_i g_i$, where $\alpha_i \in \mathcal{S}$ and $g_i \in \mathcal{G}$.

Since $\mathbb{N} \subset \mathbb{Q}^+ \subset \mathbb{Q}$, a generating set over $\mathbb{N}$ is also a generating set over $\mathbb{Q}^+$, and a generating set over $\mathbb{Q}^+$ is also a generating set over $\mathbb{Q}$. However, the reverse is not true and is, in our opinion, a source of some inaccuracies that can be found in the literature (see [17], for instance). Therefore, it is important to specify over which set of $\{\mathbb{N}, \mathbb{Q}^+, \mathbb{Q}\}$ the coordinates (used for the decomposition of a semiflow) vary.

Several definitions around the concept of minimal semiflow were introduced in [12], p. 319, in [18], p. 68, [19], [20], or in [3, 21]. However, we will only consider two basic notions in order theory: minimality of support with respect to set inclusion and minimality of semiflow with respect to the component-wise partial order on $\mathbb{N}^d$, since the various definitions found in the literature as well as the results of this paper can be described in terms of these two classic notions.

**definition 4 (Minimal support).** A nonempty support $\|f\|$ of a semiflow $f$ is minimal with respect to set inclusion if and only if $\mathcal{F} \notin \mathcal{F}^+ \setminus \{0\}$ such that $\|g\| \subset \|f\|$.

**definition 5 (Minimal semiflow).** A non-null semiflow $f$ is minimal with respect to $\le$ if and only if $\mathcal{F} \notin \mathcal{F}^+ \setminus \{0, f\}$ such that $g \le f$.

A minimal semiflow cannot be decomposed as the sum of another semiflow and a non-null non-negative vector. This remark yields an initial insight into the foundational role of minimality in the decomposition of semiflows. We are looking for characterizing generating sets such that they allow analyzing various behavioral properties as efficiently as possible. That is to say that we want generating sets as small as possible and, at the same time, able to easily handle semiflows in $\mathcal{F}^+$. First, the number of minimal semiflows over $\mathbb{N}$ can be quite large. Second, considering a basis over $\mathbb{Q}$ is of course relevant to handle $\mathcal{F}$, while less relevant when it is about $\mathcal{F}^+$, and may not capture behavioral constraints as easily. We will have to consider $\mathbb{Q}^+$.

## 4.2. Three decomposition theorems

Generating sets can be characterized thanks to three decomposition theorems. A first version of them can be found in [3] with their proofs. A second version can be found in [1] with improvements. Here, Theorem 1, which is valid over $\mathbb{N}$, is extended to a necessary and sufficient condition that characterizes a minimal semiflow and generating sets over $\mathbb{N}$. This result is provided with a new proof using Gordan's lemma (see Lemma 1). Theorems 2 and 3 are recalled for completeness and are unchanged from [1].
### 4.2.1. Decomposition over non-negative integers

The fact that there exists a finite generating set over $\mathbb{N}$ is non-trivial and is often taken for granted in the literature on semiflows. In fact, this result was proven by Gordan, circa 1885, then Dickson, circa 1913. Here, we directly rewrite Gordan's lemma [22] by adapting it to our notations.

**lemma 1. (Gordan)** Let $\mathcal{F}^+$ be the set of non-negative integer solutions of the System of equations (1). Then, there exists a finite generating set over $\mathbb{N}$ of semiflows in $\mathcal{F}^+$.

The question of the existence of a finite generating set being solved for $\mathbb{N}$, is necessarily solved for $\mathbb{Q}^+$ and $\mathbb{Q}$. Lemma 1 is necessary not only to prove the decomposition theorem but also to claim the computability of the extremums described in Theorem 5.

**theorem 1. (Decomposition over $\mathbb{N}$)** A semiflow is minimal if and only if it belongs to all generating sets over $\mathbb{N}$.

The set of minimal semiflows of $\mathcal{F}^+$ is a finite generating set over $\mathbb{N}$.

Let's consider a semiflow $f \in \mathcal{F}^+ \setminus \{0\}$ and its decomposition over any family of $k$ non-null semiflows $f_i, 1 \le i \le k$. Then, there exist $a_1, ..., a_k \in \mathbb{N}$ such that $f = \sum_{i=1}^{i=k} a_i f_i$. Since $f \ne 0$ and all coefficients $a_i$ are in $\mathbb{N}$, there exists $j \le k$ such that $0 \le f_j \le a_j f_i \le f$. If $f$ is minimal, then $a_j = 1$ and $f_j = f$. Hence, if a semiflow is minimal, then it belongs to any generating set over $\mathbb{N}$. The reverse will become clear once the second statement of the theorem is proven.

Applying Gordan's lemma, there exists a finite generating set, $\mathcal{G}$. Since any minimal semiflow is in $\mathcal{G}$, the subset of all minimal semiflows is included in $\mathcal{G}$ and therefore finite. Let $\mathcal{E} = \{e_1, ...e_n\}$ be this subset and prove by construction that $\mathcal{E}$ is a generating set.

For any semiflow $f \in \mathcal{F}^+$, we build the following sequence leading to the decomposition of $f$ over $\mathcal{E}$:

i) $r_0 = f$,

ii) $r_i = r_{i-1} - k_i e_i$ such that $r_i \in \mathcal{F}^+$ and $r_{i-1} - (k_i + 1)e_i \notin \mathcal{F}^+$.

By construction of the non-negative integers $k_i$, we have $r_n = f - \sum_{i=1}^{n} k_i e_i \in \mathcal{F}^+$ and $\forall e_i \in \mathcal{E}$, $r_n - e_i \notin \mathcal{F}^+$ therefore, $\forall e_i \in \mathcal{E}$, $\exists j, (r_n)_j - (e_i)_j < 0$; therefore $\nexists e_i \in \mathcal{E}$ such that $e_i \le r_n$. This means that $r_n$ is either minimal or null. Since $\mathcal{E}$ includes all minimal semiflows, therefore $r_n = 0$, and any semiflow can be decomposed as a linear combinations of minimal semiflows; in other words, $\mathcal{E}$ is a finite generating set<fnref n="2" />.

It is now clear that if a semiflow $f$ belongs to any generating set, then it belongs in particular to $\mathcal{E}$; therefore, $f$ is a minimal semiflow. $\square$

Let's point out that since $\mathcal{E}$ is not necessarily a basis, the decomposition is not unique in general and depends on the order in which the minimal semiflows of $\mathcal{E}$ are considered to perform the decomposition.

However, a minimal semiflow does not necessarily belong to a generating set over $\mathbb{Q}^+$ or $\mathbb{Q}$.

### 4.2.2. Decomposition over semiflows of minimal support

These two theorems can already be found in [1].

**theorem 2. (Minimal support)** If $I$ is a minimal support, then

i) there exists a unique minimal semiflow $f$ such that $I = \|f\|$ and, for all $g \in \mathcal{F}^+$ such that $\|g\| = I$, there exists $k \in \mathbb{N}$ such that $g = kf$, and

ii) any non-null semiflow $g$ such that $\|g\| = I$ constitutes a generating set over $\mathbb{Q}^+$ or $\mathbb{Q}$ for $\mathcal{F}_I^+ = \{g \in \mathcal{F}^+ | \|g\| = I\}$.

In other words, $\{f\}$ is a unique generating set over $\mathbb{N}$ for $\mathcal{F}_I^+ = \{g \in \mathcal{F}^+ | \|g\| = I\}$. Indeed, this uniqueness property is lost in $\mathbb{Q}^+$ or in $\mathbb{Q}$, since any element of $\mathcal{F}_I^+$ is a generating set of $\mathcal{F}_I^+$ over $\mathbb{Q}^+$ or $\mathbb{Q}$.

<footnote n="2">²If $\mathcal{E}$ were to be infinite, the construction could still be used, since the monotonically decreasing sequence $r_i$ is bounded by 0 and $\mathbb{N}$ is nowhere dense, so we would have $\lim_{n \to \infty} (f - \sum_{j=1}^{n} k_j e_j) = 0$, with the same definition of the coefficients $k_j$ as in ii).</footnote>
**theorem 3.** (*Decomposition over $Q^+$*) Any support $I$ of semiflows is covered by the finite subset $\{I_1, I_2, \dots, I_N\}$ of minimal supports of semiflows included in $I: I = \bigcup_{i=1}^{I=N} I_i$.

Moreover, for all $f \in \mathcal{F}^+$ such that $\|f\| \le I$, one has $f = \sum_{i=1}^{I=N} \alpha_i g_i$, where, for all $i \in \{1, 2, \dots, N\}$, $\alpha_i \in \mathcal{Q}^+$ and the semiflows $g_i$ are such that $\|g_i\| = I_i$.

A sketch of the proof of Theorem 3 using Property 4 can be found in [23], and a complete proof, in [3]. This last theorem says that one cannot have a generating set with less than $n$ semiflows where $n$ is the number of minimal supports included in $P$.

# 5. Home spaces and home states

The notion of home space was first defined in [21] for Petri Nets relatively to a single initial marking. Here, we effortlessly extend its definition relatively to a nonempty subset of markings. Early descriptions of properties 6, 7, 8 can be found in [21, 24, 25] (in french). Here, they are generalized by extension or addition of a sub-property.

Home spaces are extremely useful to analyze liveness (see [26]) or resilience (see [27]). Any behavioral property requiring to eventually become satisfied after executing a sequence of transitions can be supported by a home space (a property satisfied for any reachable marking would be an invariant).

## 5.1. Definitions and basic properties

Given a Petri Net $PN$, its associated set $Q$ of all potential markings and a subset $Init$ of $Q$, we say that a set $HS$ is an $Init$-home space if and only if, for any progression (i.e. sequence of transitions) from any element of $Init$, there exists a way of prolonging this progression and reach an element of $HS$. In other words:

**definition 6 (Home space).** Given a nonempty subset $Init$ of $Q$, a set $HS$ is an $Init$-home space if and only if, for all $q \in RS(PN, Init)$, $RS(PN, q) \cap HS \neq \emptyset$, in other words, there exists $h \in HS$ such that $h$ is reachable from $q$, (i.e. $q \xrightarrow{*} h$).

This definition is general and can be applied to any Transition System. In [28], we can find, for Petri Nets, an equivalent definition: $HS$ is an $Init$-home space if and only if $RS(PN, Init) \subseteq RS^{-1}(PN, HS \cap Q)$.

**definition 7 (Home state).** Given a nonempty subset $Init$ of $Q$, a marking $s$ is an $Init$-home state if and only if $\{s\}$ is an $Init$-home space.

If $s$ is an $Init$-home state, then it is straightforwardly an $\{s\}$-home state, and we simply say that $s$ is a home state when there is no ambiguity. This is the usual notation that can be found in [10], p.59, or in [17], p. 63, in [29] and in many other papers.

In many systems, the initial marking $q_0$ represents an *idle* state from which the various capabilities of the system can be executed. In this case, it is important for $q_0$ to be a home state. This property is usually guaranteed by a reset function that can be modeled in a simplistic way by adding a transition $r$ such that $RS(M, q_0) \subseteq \text{Dom}(r)$ and $\{q_0\} = \text{Im}(r)$ (which means that $r$ is executable from any reachable marking and that its execution reaches $q_0$). However, by requiring to add too much complexity to *RG* (one edge per node), this function is most of the time abstracted away when building *RG* up.

It is not always easy to prove that a given set is an $Init$-home space. This question is addressed in [28] and is proven decidable for home states for Petri Nets but is still open in a more complex conceptual model. Furthermore, a corpus of decidable properties can be found in [24, 30, 27], or [28].

It may be worth mentioning the straightforward following properties, given two subsets $A$ and $B$ of markings.

**property 5.** If $HS$ is an $A$-home space, it is a $B$-home space for any nonempty subset $B$ of $A$. If $HS_1$ is an $A_1$-home space and $HS_2$ is an $A_2$-home space, then $HS_1 \cup HS_2$ is an $(A_1 \cup A_2)$-home space.
However, the intersection of two home spaces is not necessarily a home space. Figure 2 represents the reachability graph of a Transition System with eight markings. $HS_1, HS_2$ and $HS_3$, as defined Figure 2, are three $\{q_0\}$-home spaces. While $HS_1 \cap HS_3 = \{q_1, q_3\}$ is a $\{q_0\}$-home space, $HS_1 \cap HS_2 = \{q_1\}$ is not a $\{q_0\}$-home space (even if it is a $\{q_1\}$-home state).

<figure><img src="image_6.png" /><figcaption>**Figure 2:** With $Q = \{q_0, q_1, q_2, q_3, q_4, q_5, q_6, q_7\}$, $HS_1 = \{q_1, q_3, q_4\}$, $HS_2 = \{q_1, q_5\}$ and $HS_3 = \{q_1, q_3, q_5\}$ are three $\{q_0\}$-home space. $HS_4 = \{q_1, q_4, q_7\}$ is a $\{q_6\}$-home space as well as a $\{q_0\}$-home space.</figcaption></figure>

Given a Petri Net PN and a subset of markings Init, a sink is a marking with no successor in the associated reachability graph RG(PN, Init). More generally, a subset S of markings is a sink in RG(PN, Init) if and only if $RS(M, S) = S$. Similarly, we say that strongly connected component S of RG(PN, Init) is strongly connected component sink if and only if $\nexists y \in RS(M, Init) \setminus S$ such that $\exists x \in S$ and $x \to y$. As any directed graph, RG(M, Init) can have its vertices (markings) partitioned into strongly connected components and some of them can be sink at the same time. The following property can be easily deduced from the definition of sink, strongly connected component, and home space.

**property 6.** If there exists a unique strongly connected component sink S in RG(M, Init) then S is a home space. Moreover, a marking is a home state if and only if it belongs to S.

Furthermore, any home space has at least one element in each strongly connected component sink of the reachability graph [24].

It is easy to prove that these properties hold even as the reachability graph can be infinite, considering that the definitions of sources, sinks, or strongly connected components are the same as in the case where the directed reachability graph is finite.

**property 7.** we consider a Petri Net PN paired with a single initial marking $q_0$. Then, three following statements are equivalent:

(i) the initial marking $q_0$ is a home state;

(ii) every reachable marking is a home state;

(iii) the reachability graph is strongly connected.

If $q_0$ is the initial marking, then, for all $x, y \in RS(PN, q_0)$, there exists a path from $q_0$ to x and a path from $q_0$ to y, and since $q_0$ is a home state, there also exists a path from x to $q_0$ and from y to $q_0$ in the reachability graph. Hence, $q_0$, x and y belong to the same strongly connected component. We easily conclude that the reachability graph is strongly connected. The other elements of the property become obvious. □

It is easy to deduce that any reachable marking from a home state $h$ is a home state even if $h$ is not the initial marking. The strong connectivity of a given reachability graph means that some transitions are necessarily live. This remark linking the notions of home state, strong connectivity, and liveness requires to be explored further. It is at the core of the following subsection.

## 5.2. Home spaces, semiflows, and liveness

Semiflows are intimately associated with home spaces and invariants and can greatly simplify the proof of fundamental properties of Petri Nets (even including parameters as in [31]) such as safeness,
boundedness, or more complex behavioral properties such as liveness. Let us provide three properties supporting this idea.

Let $Dom(t)$ denote the subset of markings from which the transition $t$ is executable, and $Im(t)$, the subset of markings that can be reached by the execution of $t$.

**property 8.** A transition $t$ is live if and only if there exists a home space $H$ such that $H \subseteq Dom(t)$.
Moreover, if $Dom(t)$ is a home space, then $Im(t)$ is also a home space.

This can be directly deduced from the usual definition of liveness and Definition 6 of home spaces. ☐

We consider $\langle PN, q_0 \rangle$, a Petri Net $PN$ with its initial marking $q_0$, its associated reachability set $RS$, its labeled reachability graph $LRG$, a home space $HS$ and $H = HS \cap RS$ such that $H$ induces (see, for instance, [32] for the notion of induced subgraph) a strongly connected subgraph of $LRG$.

**lemma 2.** If a home space $H$ induces a strongly connected subgraph of $LRG$, then a transition $t$ is live if and only if there exist $h_t \in H$ and $\sigma \in T^*$ such that $h_t \xrightarrow{\sigma t} h$.

If $HS$ is a home space, then $H$ is also a home space, and for all $q \in RS$, there exist $s_1 \in T^*$ and $h \in H$ such that $q \xrightarrow{s_1} h$.

The subgraph induced by $H$ being strongly connected, there exists a path from $h$ to $h_t$; in other words, there exists $s_2 \in T^*$ such that $h \xrightarrow{s_2} h_t$. We can construct a sequence $s = s_1 s_2 \sigma$ such that for all $q \in RS, q \xrightarrow{st} h$. Hence $t$ is live in $RS(M, q_0)$. The reverse is obvious. ☐

**property 9.** Let $PN$ be a Petri Net and $q$ be a home state. Then, any transition that is enabled at $q$ is live, and, more generally, a transition is live if and only if it appears as a label in $LRG(PN, q)$.

This can be proven directly from the definition of liveness and Lemma 2. ☐

We can then deduce from this property that liveness is decidable for Petri Nets equipped with a home state. More precisely, we have:

**theorem 4.** Let $PN$ be a Petri Net with a home state $q$, and $LCT(PN, q)$, the labeled coverability tree of $PN$. A transition is live if and only if it appears as a label in $LCT(PN, q)$.

This can be proven directly from the fact that a transition appears as a label of an edge of $LRG(PN, q)$ if and only if it appears as a label of an edge of $LCT(PN, q)$, and by considering Property 9. ☐

**corollary 2.** For any Petri Net with a home state $q$, liveness is decidable.

This is a direct consequence of Theorem 4 combined with Karp and Miller's theorem [33], stating that the coverability tree is finite. ☐

In [34], we find the following result: if a free choice Petri net is safe then there exists a home state. From corollary 2, we can conclude that liveness is decidable for free choice safe Petri Nets.

Given an initial state $q_0$, each semiflow can be associated with an invariant that, in turn, can be associated with a home space. In other words, if $f \in \mathcal{F}$, then $HS(f, q_0) = \{q \in Q \mid f^\top q = f^\top q_0\}$ is a $\{q_0\}$-home space, since $RS(M, q_0) \subseteq HS(f, q_0)$.

**property 10.** If $f \in \mathcal{F}$, then, for all $\alpha \in \mathbb{Q} \setminus \{0\}$, $HS(\alpha f, q_0) = HS(f, q_0)$. Also, for all $f$ and $g \in \mathcal{F}$ and for all $\alpha$ and $\beta \in \mathbb{Q}$, $HS(f, q_0) \cap HS(g, q_0) \subseteq HS(\alpha f + \beta g, q_0)$. Moreover, $HS(f, q_0) \cap HS(g, q_0)$ is a $\{q_0\}$-home space.

Note that $HS(f, q_0) \cap HS(g, q_0)$ is straightforwardly a $\{q_0\}$-home space, since they both contain $RS(M, q_0)^3$. If $q \in HS(f, q_0) \cap HS(g, q_0)$, then $\alpha(f^\top q) = \alpha(f^\top q_0)$ and $\beta(g^\top q) = \beta(g^\top q_0)$, so $(\alpha f + \beta g)^\top q = (\alpha f + \beta g)^\top q_0$, and, therefore, $q \in HS(\alpha f + \beta g, q_0)$ ☐

We define $\Omega$, the closure under $\cap$ of $\{H \subseteq Q \mid \exists f \in \mathcal{F}^+, H = HS(f, q_0)\}$, that is the smallest subset of $2^Q$ stable for $\cap$ containing $\{H \subseteq Q \mid \exists f \in \mathcal{F}^+, H = HS(f, q_0)\}$. For the same reason as for property 10, all elements of $\Omega$ are home spaces and there exists a unique nonempty minimal element $\omega = \min_{h \in \Omega} h$ characterized in the next section.

<footnote n="3">³Let us recall that, in general, the intersection of home spaces is not a home space (see Figure 2).</footnote>
### 5.3. Three extremums computability

Knowledge of any finite generating set allows a practical computation of the three extremums ($\lambda$, $\theta$, and $\omega$) defined in the previous sections.

We know that a finite generating set does exist by Gordan's lemma (1) and we know how to compute a generating set (see [7] for instance). Subsequently, we can state the following theorem which expresses the fact that three extremums ($\lambda$, $\theta$, and $\omega$) are computable as soon as any finite generating set is available.

**theorem 5.** Let $\mathcal{E} = \{e_1, \dots, e_N\}$ be any finite generating set of $\mathcal{F}^+$, and $q_0 \in Q$, an initial marking.

(i) If $\mathcal{E}$ is over $\mathbb{S}$, then we have: $\omega = \bigcap_{f \in \mathcal{F}^+} \mathrm{HS}(f, q_0) = \bigcap_{e_i \in \mathcal{E}} \mathrm{HS}(e_i, q_0)$;

(ii) If $\mathcal{E}$ is over $\mathbb{Q}^+$ or $\mathbb{N}$, then, for any place $p$ belonging to at least one support of a semiflow of $\mathcal{F}^+$, for all $q \in \mathrm{RS}(\mathrm{PN}, q_0)$, we have:

$$q(p) \le \lambda(p, q_0) = \min_{\{f \in \mathcal{F}^+ | f(p) \ne 0\}} \frac{f^\top q_0}{f(p)} = \min_{\{e_i \in \mathcal{E} | e_i(p) \ne 0\}} \frac{e_i^\top q_0}{e_i(p)};$$

(iii) If $\mathcal{E}$ is over $\mathbb{Q}^+$ or $\mathbb{N}$, then, for any transition $t$ belonging to at least one support of a semiflow of $\mathcal{F}^+$, for all $q \in \mathrm{RS}(\mathrm{PN}, q_0)$, we have:

$$\theta(t, q_0) = \min_{\{f \in \mathcal{F}^+ | f^\top \mathrm{Pre}(\cdot, t) \ne 0\}} \frac{f^\top q_0}{f^\top \mathrm{Pre}(\cdot, t)} = \min_{\{e_i \in \mathcal{E} | e_i^\top \mathrm{Pre}(\cdot, t) \ne 0\}} \frac{f^\top q_0}{f^\top \mathrm{Pre}(\cdot, t)}$$

For the item (i), let's consider $f \in \mathcal{F}^+$ with $f = \sum_{i=1}^{i=N} \alpha_i e_i$ and $q \in \bigcap_{e_i \in \mathcal{E}} \mathrm{HS}(e_i, q_0)$. Then, $\alpha_i(e_i^\top q) = \alpha_i(e_i^\top q_0)$, for all $i \in \{1, \dots, N\}$, and, hence $\sum_{i=1}^{i=N} \alpha_i(e_i^\top q) = \sum_{i=1}^{i=N} \alpha_i(e_i^\top q_0)$. Then, for all $f \in \mathcal{F}^+$, $f^\top q = f^\top q_0$, and $q \in \mathrm{HS}(f, q_0)$.

Therefore, since $\mathcal{E} \subset \mathcal{F}^+$ directly implies $(\bigcap_{f \in \mathcal{F}^+} \mathrm{HS}(f, q_0)) \subseteq \bigcap_{e_i \in \mathcal{E}} \mathrm{HS}(e_i, q_0)$, we have: $\bigcap_{e_i \in \mathcal{E}} \mathrm{HS}(e_i, q_0) = \bigcap_{f \in \mathcal{F}^+} \mathrm{HS}(f, q_0) = \omega$.

For the item (ii), let's consider a marking $q_0$, a place $p$, and a semiflow $f$ of $\mathcal{F}^+$ such that $f(p) > 0$ and $f = \sum_{i=1}^{i=N} \alpha_i e_i$, where $\alpha_i \ge 0$, for all $i \in \{1, \dots, N\}$.

Let's define $\lambda_{\mathcal{E}}$ such that $\lambda_{\mathcal{E}} = \min_{\{e_i \in \mathcal{E} | e_i(p) \ne 0\}} \frac{e_i^\top q_0}{e_i(p)}$. Then, there exists $j$ such that $1 \le j \le N$ and $\lambda_{\mathcal{E}} = \frac{e_j^\top q_0}{e_j(p)}$.

Therefore, for all $i \le N$ such that $e_i(p) \ne 0$, there exists $\delta_i \in \mathbb{Q}^+$ such that: $\frac{e_j^\top q_0}{e_j(p)} = \frac{e_i^\top q_0 - \delta_i}{e_i(p)}$. It can then be deduced, for all $i$ such that $\alpha_i e_i(p) \ne 0$:

$$\lambda_{\mathcal{E}} = \frac{\alpha_i(e_i^\top q_0 - \delta_i)}{\alpha_i e_i(p)},$$

and, therefore:

$$\lambda_{\mathcal{E}} = \frac{\sum_{\{i | \alpha_i e_i(p) > 0\}} \alpha_i (e_i^\top q_0 - \delta_i)}{\sum_{\{i | \alpha_i e_i(p) > 0\}} \alpha_i e_i(p)}$$

Since $\sum_{\{i | \alpha_i e_i(p) > 0\}} \alpha_i (e_i^\top q_0) = f^\top q_0 - \sum_{\{i | \alpha_i e_i(p) = 0\}} \alpha_i (e_i^\top q_0)$ and $\sum_{\{i | \alpha_i e_i(p) > 0\}} \alpha_i e_i(p) = f(p)$

$$\lambda_{\mathcal{E}} = \frac{f^\top q_0 - \sum_{\{i | e_i(p) > 0\}} \alpha_i \delta_i - \sum_{\{i | e_i(p) = 0\}} \alpha_i e_i^\top q_0}{f(p)}$$

Then, since $\delta_i \ge 0$ and $\alpha_i \ge 0$ for all $i$ such that $1 \le i \le N$,

$$\lambda_{\mathcal{E}} \le \frac{f^\top q_0}{f(p)}$$
This being verified for any semiflow of $\mathcal{F}^+$, we have $\lambda(p, q_0) = \lambda_{\mathcal{E}}$.

The item (iii) of the theorem can be proven by a similar demonstration □

Item (i) is similar to a result that can be found in [24]. The complexity of computing item (ii) or (iii) depends on $N$ the number of elements of $\mathcal{E}$. We know from theorem 3 that $N$ cannot be less than the number of minimal supports.

# 6. Reasoning with invariants, semiflows, and home spaces

Invariants, semiflows, and home spaces can be used in combination to prove a rich array of behavioral properties of Petri Nets, in particular when using parameters.

## 6.1. Methodically analyzing behavioral properties

The results presented in this paper provide verification engineers with a few steps to methodically analyze and prove behavioral properties, in particular that a subset of transitions are live:

- run existing algorithms to compute Generating sets,[7, 35], even with parameters as in [36]; comparisons and benchmarks can be found in [37] and more recently in [38],

- from a generating set, using property 10, infer a first home space that concisely describes how tokens are distributed over places,

- use theorem 5 to prune away impossible situations,

- step by step proceed by refinement of home states, finding which transitions can be enabled and constrain current home spaces until reaching a possible home state,

- Use algorithms as in [33, 39] to construct the labeled coverability tree (LCT), and then deduce which transitions are live from the ones that appears in LCT (theorem 4),

- ultimately, decide whether the Petri Net is live or not.

Here, through two related parameterized examples, we proceed by using basic arithmetic and some particularity of the structure of the model to determine a home space and a home state in the second case. Then, it becomes easy to determine for which values of the parameters the Petri Net possesses the required liveness property.

First, we propose to look at an example with a parameter $i$ to define its Pre and Post functions. This example allows one to detect whether a natural number $n$ is a multiple of $i$. The second example is an extension of the first one with a coloration of the tokens allowing one to detect the remainder of the Euclidean division of $n$ by $i$.

## 6.2. A first example

The Petri Net $TN(i) = \{\{A, B\}, \{t_1, t_2\}, Pre, Post\}$ in Figure 3 is defined by:

$$Pre(\cdot, t_1)^\top = (i, 0); Pre(\cdot, t_2)^\top = (1, 1);$$

$$Post(\cdot, t_1)^\top = (0, 1); Post(\cdot, t_2)^\top = (i + 1, 0).$$

The initial marking $q_0$ is such that $q_0(A) = n$ and $q_0(B) = x$, where $n$ and $x \in \mathbb{N}$.

A first version of this example can be found for $i = 2$ in [10] or in [21], without proof. Here, the Petri Net $TN(i)$ is enriched by introducing a parameter $i$ such that $i > 1$ to define its Pre and Post functions.

$g^\top = (1, i)$ is the minimal semiflow of minimal support, and we can prove that $\langle TN(i), q_0 \rangle$ is not live if and only if $g^\top q_0 \le i$ or $g^\top q_0 = n \times i$, independently of $q_0(B)$. In other words, $TN(i)$ recognizes whether a given number $n$ is a multiple of $i$.

First, if $g^\top q_0 < i$, then the enabling threshold of $t_1$ can never be reached (Property 3) and neither $t_1$ nor $t_2$ can be executed (since $q_0(B)$ is necessarily null to satisfy the inequality). Second, if $g^\top q_0 \ge i$, then we consider the Euclidean division of $g^\top q_0$ by $i$, giving $g^\top q_0 = n \times i + r$, where $r < i$. Then, since $g$ is a semiflow, $g^\top q = q(A) + iq(B) \equiv r \mod i$, and, therefore, $q(A) \equiv r \mod i$, for all $q \in RS(TN(i), q_0)$. If $r = 0$, then we have $q(A) = n \times i - i \times q(B)$, and $t_1$ can always be executed $n - q(B)$ times to reach a marking with zero token in $A$.
<figure><img src="image_7.png" /><figcaption>**Figure 3:** Semiflows must verify the system of equations (1) which is reduced to the following equation: $i \times a = b$, for which $g^\top = (1, i)$ is an obvious solution. $TN(i)$ is live if and only if $g^\top q_0 > i$ and is not a multiple of $i$, regardless of the initial marking of $B$. For $i = 1$, $TN(1)$ has no live transition, regardless of the initial marking.</figcaption></figure>

If $r \neq 0$ and $g^\top q_0 > i$, then after executing $t_1 n - q(B)$ times, we reach a marking with $r$ tokens in $A$ and at least one token in $B$. Therefore, $HS = \{q \in RS(TN(i), q_0) | q(A) \neq 0 \wedge q(B) \neq 0\}$ is a home space such that $HS \subseteq Dom(t_2)$ so, we can apply property 8 proving that $t_2$ is live. It is easy to conclude that the Petri Net $TN(i)$ is live if and only if $g^\top q_0 > i$ and is not a multiple of $i$, regardless of the initial marking of $B$. □

We can point out that it was not necessary to develop a symbolic reachability graph in order to decide whether or not the Petri Net is live or bounded. We could analyze the Petri Net even partially ignoring the initial marking (i.e., considering $q_0(A)$ as a parameter and without considering the values taken by $q_0(B)$).

## 6.3. Euclidean division

From the properties of $TN(i)$, it is natural to progress by one more step and propose to design a Petri Net with the ability not only to recognize whether a natural number $n$ is a multiple of a given natural number $i$, but more generally to recognize the remainder of the Euclidean division of $n$ such that $n > 0$ by $i$ such that $i > 1$. To this effect, we first consider the Colored Petri Net $TNCED(i)$ of Figure 4, and the parameter $i \geq 2$. Second, for easing the reasoning, we unfold $TNCED(i)$ into the classic Petri Net $TNED(i)$, where each place $A_j$ represents the color $j$ of $TNCED(i)$ (see Figures 4 and 5).

We define $P = \{\{A_j | j \in [0, i-1]\}, B\}$ and $T = \{t_{j,1}, t_{j,2} | j \in [0, i-1]\}$, where Pre and Post are defined by:

$$Pre(A_j, t_{j,1}) = i, Pre(B, t_{j,1}) = Pre(A_j, t_{j,2}) = 1$$

$$Post(A_j, t_{j,2}) = i + 1, Post(B, t_{j,1}) = 1.$$

where $j \in [0, i-1]$. The initial marking is such that $q_0(A_j) = n + j$, where $j \in [0, i-1]$, and $q_0(B) = x$, where $n > 0$ and $x$ are natural numbers.

<figure><img src="image_8.png" /><figcaption>**Figure 4:** $TNCED(i)$, is a Colored Petri Net with a set $C$ of colors to distinguish values between 0 and $i-1$ plus $\tau$ as an undefined color of token; $C = ([0, ...i-1] \cap \mathbb{N}) \cup \{\tau\}$.</figcaption></figure>

We have a system of $i$ equations: $i \times a_j = b$ with $j \in [0, i-1] \cap \mathbb{N}$, for which $g$ such that $g(A_j) = 1$ for $j \in [0, i-1] \cap \mathbb{N}$ and $g(B) = i$ is the minimal semiflow of minimal support in $\mathbb{N}$. This Colored Petri Net allows knowing the remainder of the Euclidean division of a natural number $n$ by $i$.
<figure><img src="image_9.png" /><figcaption>**Figure 5:** $TNED(i)$ is the unfolded version of $TNCED(i)$. To compute semiflows, we have a system of $i$ equations: $i \times a_j = b$ with $j \in [0, i-1]$, for which $g$ such that $g(A_j) = 1$ for $j \in [0, i-1]$ and $g(B) = i$ is the minimal semiflow of minimal support in $\mathbb{N}$. This parameterized Petri Net allows knowing the remainder of the Euclidean division of a natural number $n$ by $i$.</figcaption></figure>

We set $g_i^T = (1, \dots, 1, i)$, such that $g(A_j) = 1$ for $j \in [0, i-1]$, and $g(B) = i$ is the minimal semiflow of minimal support in $\mathbb{N}$. We have a first invariant $I$, for all $q \in RS(TNED(i), q_0)$:

$$g^T q_0 = g^T q = \sum_{j=0}^{j=i-1} q_0(A_j) + iq_0(B) = i \times (x + n + \frac{i-1}{2}).$$

Then, we need to notice that any place $A_j$ is connected to only two transitions, $t_{j,1}$ and $t_{j,2}$, such that:

$$Post(A_j, t_{j,1}) - Pre(A_j, t_{j,1}) = -i,$$

$$Post(A_j, t_{j,2}) - Pre(A_j, t_{j,2}) = i.$$

Hence, for all $q \in RS(TNED(i), q_0)$ and $j \in [0, i-1]$, $q(A_j)$ can only vary by $\pm i$. We then deduce a family of invariants $I(j)$ for $j \in [0, i-1]$:

$$I(j) : \forall q \in RS(TNED(i), q_0), q(A_j) \equiv q_0(A_j) \mod i.$$

Let's perform the Euclidean division of $q_0(A_j)$ by $i$. We have: $q_0(A_j) = n + j = a_j \times i + \alpha_j$, where $\alpha_j < i$ for all $j \in [0, i-1]$. A new family of invariants $I'(j)$ can be directly deduced from each $I(j)$:

$$I'(j) : \forall q \in RS(TNED(i), q_0), q(A_j) \geq \alpha_j.$$

Furthermore, it must be pointed out that $\{\alpha_0, \dots, \alpha_{i-1}\}$ is a permutation of $\{0, \dots, i-1\}$. Indeed, if there exist $j < i$ and $j' < i$ such that $\alpha_j = \alpha_{j'}$, then $n + j - a_j \times i = n + j' - a_{j'} \times i$, and $|j - j'| = |a_j - a_{j'}| \times i$. Since $|j - j'| < i$, we have $a_j = a_{j'}$ and $j = j'$. Therefore,

(a) $\sum_{j=0}^{j=i-1} q(A_j) \geq \frac{i(i-1)}{2}$ (directly from the $I'(j)$ family of invariants), and

(b) there is a unique $k \in [0, i-1]$ such that $\alpha_k = 0$.

From (a) and $I$, we deduce, for all $q \in RS(TNED(i), q_0)$, $q(B) \leq x + n$ (which is a better bound than the one that can be deduced from Proposition 2). Also, from $I(j)$, we can deduce, $\forall q \in RS(TNED(i), q_0)$, $q(A_j) = y_j \times i + \alpha_j$, where $y_j \in \mathbb{N}$.
From any reachable marking $q$, the sequence $\sigma_q = t_{0,1}^{y_0} \cdots t_{i-1,1}^{y_{i-1}}$ can be executed and reach the marking $q_h$ such that, for all $j \in [0, i-1]$, $q_h(A_j) = \alpha_j$ and $q_h(B) = x+n$.

We know $q_h$ is a home state, since $\sigma_q$ is defined for any reachable marking (Note that $q_0$ is not a home state). From Property 9, we deduce that, since any transition $t_{j,2}$ where $j \neq k$ is executable ($n > 0$ hence, $q_h(B) > 1$ and $q_h(A_j) = \alpha_j > 0$), then $t_{j,2}$ is live, and, therefore, the corresponding transitions $t_{j,1}$ are also live.

From (b), $q_h(A_k) = 0$ from, which we deduce that $t_{k,1}$ and $t_{k,2}$ are not live$^4$. Finally, we have $n+k = a_k \times i$, and the remainder of the Euclidean division of $n$ by $i$ is $i-k$.

TNED($i$) provides the ability to recognize this remainder by the remarkable fact that $(t_{k,1}, t_{k,2})$ is the only couple of transitions not live □

Most of the time, in real-life use cases, when a model accepts a set of home states, then the initial marking belongs to it. It is not the case in our example, and this suggests the following conjecture:

"If the initial marking $q_0$ of a Petri Net $PN$ is not a home state and there exists a home state in $RS(PN, q_0)$, then there exists at least one non-live transition in $\langle PN, q_0 \rangle$."

# 7. Conclusion

It has been recalled how semiflows allow inferring strong constraints over all possible markings of a given Petri Net, which greatly help analysis of behavioral properties such as not only boundedness but also liveness. Moreover, analysis can be performed with incomplete information, particularly when markings and even structures are described with parameters as in our two examples.

The set of semiflows can be characterized with the notion of minimal generating set, and we hope that our three decomposition theorems reached their final version. They were useful to make properties on boundedness or liveness computable. Theorem 5 is an indication that knowledge of a generating set brings most of the information that semiflows in $\mathcal{F}^+$ can provide for analysis of behavioral properties.

Most of the time, especially with real-life system models, it will be possible to avoid a painstaking symbolic model checking or a parameterized and complex development of a reachability graph [40, 41].

We introduced new results about home spaces; in particular, theorem 4 is new to the best of our knowledge (for instance, it does not appear in the recent survey on decidability issues for Petri Nets [42]). This theorem is interesting for at least two different reasons. First, from a theoretical point of view, it characterizes a class containing unbounded Petri Nets, since the existence of a home state does not mean that the Petri Net is bounded. Second, from a practical point of view, it shed a new light on the usage of coverability graphs, since real-life systems often have a home state by design. It increases the importance one can grant to the construction of coverability trees, which is used mostly to determine which places are bounded (see important works by Finkel and al [39] about accelerating this construction) by supporting the analysis of liveness.

At last, we presented most of these results in the framework of Petri Nets, we believe that most of these results apply to Transition Systems. This, indeed, constitutes a starting point for future work.

# Declaration on Generative AI

During the preparation of this work, I used Overleaf and deepL for grammar and spelling check, paraphrase and reword. After using these tools/services, I reviewed and edited the content as needed and take(s) full responsibility for the publication's content.

<footnote n="4">⁴Actually, it suffices to notice that $A_k$ is an empty deadlock that remains empty.</footnote>
## References

[1] G. Memmi, Minimal generating sets for semiflows, in: M. Huisman, A. Ravara (Eds.), Formal Techniques for Distributed Objects, Components, and Systems, Springer Nature Switzerland, Cham, 2023, pp. 189-205.

[2] K. Jensen, Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Springer, 1997.

[3] G. Memmi, Fuites et Semi-flots dans les Réseaux de Petri, Thèse de Docteur-Ingénieur, U. P. et M. Curie, Paris, France, 1978.

[4] Y. E. Lien, Analysis of conservational transition systems, *ACM '73: Proc. of the ACM annual conference* 5 (1973) pp 440–441. URL: https://doi.org/10.1145/800192.805789.

[5] K. Lautenbach, H. A. Schmid, Use of Petri nets for proving correctness of concurrent process systems, in: *Information Processing '74, Proc. I.F.I.P. Congress*, North Holland Pub., (1974), pp. 187–191.

[6] G. Memmi, Semiflows and invariants. application in Petri nets theory, in *Journées d'Etudes sur les Réseaux de Petri AFCET-Institut de Programmation*) (1977) pp. 145–150.

[7] J. Martinez, M. Silva, A simple and fast algorithm to obtain all invariants of a generalised Petri net, in: *ATPN*, Springer, 1982, pp. 301–310.

[8] Y. E. Lien, Termination properties of generalized Petri nets, *SIAM J. on Computing* 5 (1976) pp. 251–265.

[9] J. Sifakis, Structural properties of Petri nets, in: J. Winkowski (Ed.), *MFCS 1978, Proc. 7th Symp., Zakopane, Poland, volume 64 of LNCS*, Springer, (1978), pp. 474–483.

[10] G. W. Brams, Réseaux de Petri: Théorie et Pratique, Masson, Paris, France, 1982.

[11] J. M. Colom, E. Teruel, M. Silva, S. Haddad, Structural methods, in: C. Girault, R. Valk (Eds.), *Petri Nets for Systems Engineering, A guide to Modeling, Verification, and Applications*, Springer Berlin Heidelberg, 2003, pp. 277–316.

[12] M. Silva, E. Teruel, J. M. Colom, Linear algebraic and linear programming techniques for the analysis of place/transition net systems, Springer Berlin Heidelberg, 1998, pp. 309–373.

[13] P. Czerner, J. Esparza, J. Leroux, Lower bounds on the state complexity of population protocols, *Distributed Comput. 36* (2023) 209–218.

[14] M. D. Johnston, D. F. Anderson, G. Craciun, R. Brijder, Conditions for extinction events in chemical reaction networks with discrete state spaces, *J. Mathematical Biology* 76,6 (2018) pp. 1535–1558.

[15] L. W. Dworzanski, I. A. Lomazova, Structural place invariants for analyzing the behavioral properties of nested Petri nets, in: F. Kordon, D. Moldt (Eds.), *ATPN and Concurrency*, Springer Int. Pub., Cham, 2016, pp. 325–344.

[16] K. Wolf, How Petri Net Theory Serves Petri Net Model Checking: A Survey, Springer Berlin Heidelberg, 2019, pp. 36–63.

[17] C. Girault, R. Valk, Petri Nets for Systems Engineering, A guide to Modeling, Verification, and Applications, Springer, 2003.

[18] J. M. Colom, M. Silva, E. Teruel, Properties, in: C. Girault, R. Valk (Eds.), *Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications*, Springer Berlin Heidelberg, 2003, pp. 53–72.

[19] F. Krückeberg, M. Jaxy, Mathematical methods for calculating invariants in Petri nets, in: G. Rozenberg (Ed.), *Advances in Petri Nets 1987*, Springer Berlin Heidelberg, 1987, pp. 104–131.

[20] G. Ciardo, G. Mecham, E. Paviot-Adet, M. Wan, P-semiflow computation with decision diagrams, in: W. K. e. Franceschinis G. (Ed.), *ATPN, Petri Nets 2009, LNCS 5606*, Springer, Berlin, Heidelberg, (2009), pp. 143–162.

[21] G. Memmi, Methodes d'analyse de Réseaux de Petri, Réseaux a Files, Applications au temps reel, Thèse d'Etat, U. P. et M. Curie, Paris, France, 1983.

[22] N. Alon, K. A. Berman, Regular hypergraphs, gordon's lemma, steinitz' lemma and invariant theory, *J. of Combinatorial Theory, A* 43 (1986) pp. 91–97.

[23] G. Memmi, G. Roucairol, Linear algebra in net theory, in: W. Brauer (Ed.), *Net Theory and*
*Applications, Proceedings of the Advanced Course on General Net Theory of Processes and Systems*, Hamburg, Germany, October 8-19, 1979, volume 84 of LNCS, Springer, 1979, pp. 213–223.

[24] C. Johnen, Analyse Algorithmique des Réseaux de Petri : Vérification d'Espaces d'Accueil, Systèmes de Réécriture, Thèse de 3ème cycle, U. Paris Sud, Orsay, France, 1987.

[25] C. Johnen, G. Memmi, D'espaces d'accueil dans les réseaux de petri, in *Journées d'Etudes sur les Réseaux de Petri AFCET-Institut de Programmation*) (1991).

[26] J. Vautherin, G. Memmi, Computation of flows for unary-predicates/transition-nets, in: G. Rozenberg, H. Genrich, G. Roucairol (Eds.), *Advances in Petri Nets 1984, European Workshop on Applications and Theory in Petri Nets*, selected papers, volume 188 of LNCS, Springer, 1984, pp. 455–467.

[27] A. Finkel, M. Hilaire, Resilience and home-space for wsts, in: R. Dimitrova, O. Lahav, S. Wolff (Eds.), Verification, Model Checking, and Abstract Interpretation, Springer Nature Switzerland, Cham, 2024, pp. 147–168.

[28] P. Jančar, J. Leroux, Semilinear home-space is decidable for Petri nets, arXiv 2207.02697 (2022). arXiv:2207.02697.

[29] T. Hujsa, J. Delosme, A. M. Kordon, Polynomial sufficient conditions of well-behavedness and home markings in subclasses of weighted Petri nets, ACM Trans. Embed. Comput. Syst. 13 (2014) 141:1–141:25.

[30] D. Frutos Escrig, C. Johnen, Decidability of home space property., Technical Report, Université Paris-Saclay, LRI, UA CNRS 410, RR n 503, 1989.

[31] M. Bozga, J. Esparza, R. Iosif, J. Sifakis, C. Welzel, Structural invariants for the verification of systems with parameterized architectures, in: A. Biere, D. Parker (Eds.), *Tools and Algorithms for the Construction and Analysis of Systems*, Springer Int. Pub., Cham, (2020), pp. 228–246.

[32] R. Diestel, Infinite Graphs, GTM 173, 5th Edition, Springer, (2017), pp. 209–281.

[33] R. Karp, R. Miller, Parallel program schemata, *J. of Computer and System Sciences* vol. 3, issue 2 (1969) pp. 147–195.

[34] E. Best, K. Voss, Free choice systems have home states, Acta Informatica 21 (1984) 89–100.

[35] H. Alaiwan, G. Memmi, Algorithmes de recherche des solutions entières positives d'un système linéaire d'équations homogènes, *Revue Technique Thomson-CSF* 14 (1982) pp. 125–135.

[36] J. Couvreur, S. Haddad, J. Pradat-Peyre, Generative families of positive invariants in coloured nets sub-classes, in: G. Rozenberg (Ed.), APN'93, Gjern, Denmark, June 1991, volume 674 of LNCS, Springer, 1991, pp. 51–70.

[37] J. M. Colom, M. Silva, Convex geometry and semiflows in P/T nets. A comparative study of algorithms for computation of minimal p-semiflows, in: G. Rozenberg (Ed.), *Advances in Petri Nets 1990* [10th Int. Conf. on ATPN, Bonn, Germany, Proc.], LNCS 483, Springer, 1989, pp. 79–112.

[38] Y. Thierry-Mieg, Efficient strategies to compute invariants, bounds and stable places of Petri nets, in: PNSE'23, 2023, Lisbon, Portugal, 2023. URL: https://github.com/yanntm/InvariantPerformance/blob/master/README.md.

[39] A. Finkel, S. Haddad, I. Khmelnitsky, Minimal coverability tree construction made complete and efficient, in: J. Goubault-Larrecq, B. König (Eds.), *Foundations of Software Science and Computation Structures - 23rd Int. Conf., FOSSACS 2020*, Dublin, Ireland, April, 2020, LNCS 12077, Springer, 2020, pp. 237–256.

[40] G. Delzanno, J. F. Raskin, L. van Begin, Attacking symbolic state explosion, in: *Proc. of the 13th International Conference on Computer Aided Verification, CAV 2001*, LNCS 2102, Springer, (2001), pp. 298–310.

[41] G. Chiola, C. Dutheillet, G. Franceschinis, S. Haddad, A symbolic reachability graph for coloured Petri nets, Theor. Comput. Sci. 176 (1997) 39–65.

[42] J. Esparza, M. Nielsen, Decidability issues for Petri nets – a survey, in: Arxiv 2411.01592, 2024. URL: https://arxiv.org/abs/2411.01592.