11institutetext: LTCI, Telecom-Paris, Institut polytechnique de Paris,
Palaiseau, France

# Home Spaces and Invariants to Analyze Parameterized Petri Nets

Gerard Memmi

###### Abstract

This article focuses on comparing the notions of home spaces and invariants,
in Transition Systems and more particularly, in Petri Nets as well as a
variety of derived Petri Nets.

After recalling basic notions of Petri Nets and semiflows, we then discuss
important characteristics of finite generating sets for $\mathcal{F}$, the set
of all semiflows with integer coordinates of a given Petri Net. Then, we
particularly focus on $\mathcal{F^{+}}$ the set of semiflows with non-negative
coordinates.

Minimality of semiflows and minimality of supports are critical to develop
effective analysis of invariants and behavioral properties of Petri Nets such
as boundedness or even liveness. We recall known decomposition theorems
considering semirings such as $\mathbb{N}$ or $\mathbb{Q^{+}}$ then fields
such as $\mathbb{Q}$. The result over $\mathbb{N}$ is being improved into a
necessary and sufficient condition.

In addition, we present general new results about the topology and the
behavioral properties of a Petri Net, illustrating the importance of
considering semiflows with non-negative coordinates.

Then, we regroup a number of results around the notion of home space and home
state applied to transition systems. Home spaces and semiflows are used to
efficiently support the analysis of behavioral properties.

In this regard, we present a methodology to analyze a Petri Nets by successive
refinement of home spaces directly deduced from semiflows and apply it to
analyze a parameterized example drawn from the telecommunication industry
underlining the efficiency brought by using minimal semiflows of minimal
supports as well as the new results on the topology of the model. This
methodology is better articulated than in previous papers, and brings us
closer to an automated analysis.

###### Keywords:

Invariants Home spaces Petri Nets Transition Systems generating sets
semiflows.

##  1 Introduction

###  1.1 Motivations

Parallel programs, distributed systems, telecommunication networks, cyber-
physical systems are complex entities to design, model, and verify. Using
formal verification at different stages of the system development life cycle
is a strong motivation that spread throughout this paper and provide us with
rationale for many concepts, definitions, and behavioral properties.

How to best define and use invariants to analyze the behavior of a model? Can
we not only prove that a formula is an invariant, but find a way in which they
can be organized or concisely described, a way in which they can be discovered
or computed? How can invariants be combined to represent a meaningful
behavior? How can invariants be decomposed into simpler and verifiable
properties? How to determine whether a given decomposition is more effective
than another one with regard to formal verification?

This paper which must be considered as a continuation of the work described in
[Mem23]. We want to show how linear algebra or algebraic geometry can
efficiently sustain invariant calculus. In such a setting, linear algebra can
also be applied and utilized to prove a large variety of behavioral
properties. When the model is parameterized, it can be used to determine in
which domain behavioral properties can be satisfied.

###  1.2 Outline and contributions

After providing some basic notations in Section 2 and recalling a first set of
classic properties for semiflows (be in $\mathbb{Z}$ or $\mathbb{N}$) in
Section 3, the notions of generating sets are briefly recalled from [Mem23].

The notions of generating sets, minimal semiflows, and minimal supports are
then defined in Section 4.

The three decomposition theorems of Section 4.4 have been first published in
[Mem78] then slightly improved in [Mem23]. Here, the first theorem is extended
one more time to fully characterize minimal semiflows and generating sets over
$\mathbb{N}$. The other two theorems are just recalled to present a complete
result. Subsequently, theorem 4.4 describes three extremums regarding any
semiflows and place in a support of a semiflow. This result can be computed
from any generating set. This important detail was never stressed out before
despite its importance from a computational point of view. This will later be
used in the analysis of two examples presented Section 6.

Then, the notion of home space is described Section 5 with a set of results
linked to their structure and later to their key relation with liveness
Section 5.2.

Two parameterized examples are given to illustrate how invariants and home
spaces can be used to prove behavioral properties of a Petri Net in Section 6.
A first example is analyzed with basic arithmetic reasoning. A second example
is drawn from the telecommunication industry Section 6.2. It illustrates a
method of analysis by home spaces refinement based on some of the theoretical
results presented in this paper; in particular theorem 4.4.

Section 7 concludes and provides possible avenues of future research. At last,
some additional thoughts will conclude this note.

##  2 Basic notations

In this Section, we briefly recall Petri Nets, including the notion of
potential state space usual in Transition Systems, introducing notations that
will be used in this paper. Then, we define semiflows in $\mathbb{Z}$ and
basic properties in $\mathbb{N}$ highlighting why semiflows in $\mathbb{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, $T$ a finite set of transitions such that $P\cap T=\text{\O}$.
A transition $t$ of $T$ is defined by its $Pre(\cdot,t)$ and $Post(\cdot,t)$
conditions 111We use here the usual notation: $Pre(\cdot,t)(p)=Pre(p,t)$ and
$Post(\cdot,t)(p)=Post(p,t)$.: $Pre:P\times T\rightarrow\mathbb{N}$ is a
function providing a weight for pairs ordered from places to transitions,
$Post:P\times T\rightarrow\mathbb{N}$ is a function providing a weight for
pairs ordered from transitions to places. $d$ will denote the number of
places: $d=|P|$.

The dynamic behavior of Petri Nets is modeled via markings. A marking or state
(as in any transition system) $q:\ P\rightarrow\mathbb{N}$ is a function that
evolves with the execution (or firing) of transitions or sequence of
transitions (i.e. a word in $T^{*}$). When $q(p)=k$, it is often said that the
place $p$ contains $k$ tokens.

We also define $Q$, the set of all potential markings (also known as state
space in Transition Systems); for Petri Nets we usually have:
$Q=\mathbb{N}^{d}$. Then, $RS(PN,A)$ will denote the reachability set of a
Petri Net (or model) PN from a subset $A$ of $Q$: $RS(PN,A)=\\{q\in Q\ |\
\exists a\in A,\ q\ \texttt{reachable from}\ a\\}$. $RG(PN,A)$ or $LRG(PN,A)$
will denote the corresponding reachability graph with labels in $T$ for
$LRG(PN,A)$, without labels in $T$ for $RG(PN,A)$ as in Figure 1.

Extensive definitions, properties, and case studies can be found in many
lecture notes and books, in particular in [Bra82, GV03].

##  3 Petri Nets and Semiflow basic properties

###### Definition 1

A semiflow is a solution of the following homogeneous system of $|T|$
diophantine equations:

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

where $x^{\top}y$ denotes the scalar product of the two vectors $x$ and $y$
since $f,Pre$ and $Post$ 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) which have their coefficients in $\mathbb{Z}$ and in
$\mathbb{N}$ respectively.

Considering 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})$, any non-null solution $f$ of the homogeneous system of
equations (1) allows to directly deduce the following invariant of the Petri
Net defined by its $Pre$ and $Post$ functions (used in the system of equations
that $f$ satisfies):

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

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

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

We will use the usual componentwise partial order in which

$(x_{1},x_{2},\dots,x_{d})^{\top}\leq(y_{1},y_{2},\dots,y_{d})^{\top}$ if and
only if $x_{i}\leq y_{i}\ \forall i\in\\{1,\dots,d\\}$.

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

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

$\left\|f\right\|_{-}=\left\\{p\in P\ |\ f(p)<0\right\\}$,

with $\left\|f\right\|=\left\|f\right\|_{-}\cup\ \left\|f\right\|_{+}$.

We can then rewrite the system of equations (2):

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

As we can see, the formulation of equation 3 is a differential between the
weighted number of tokens in the places of the positive support and the
weighted number of tokens in the places of the negative support of $f$. This
differential 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 recalling that the initial state $q_{0}$ belongs to
$\mathbb{N}^{d}$.

###### Property 1

For any semiflow $f\in\mathcal{F}$, $\exists p\in\left\|f\right\|_{+}$ not
bounded if and only if $\exists p\in\left\|f\right\|_{-}$ not bounded.

Of course, if $\left\|f\right\|_{-}=\varnothing$ then $f\in\mathcal{F}^{+}$
and $\left\|f\right\|$ is necessarily structurally bounded. More generally,
considering a weighting function $f$ over $P$ being defined over non-negative
integers, the following properties can be easily proven [Mem78]:

###### Property 2

If $f\geq 0$ is such that $f^{T}Pre(\cdot,t)\geq f^{T}Post(\cdot,t)\ \forall
t\in T$, then the set of places of $\left\|f\right\|$ is structurally bounded
(i.e. bounded from any initial marking).

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

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

If $f>0$ then $\left\|f\right\|_{+}=\left\|f\right\|=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 [Sif78] or [Bra82]). This property is indeed
false for a semiflow that verifies the system but would have at least one
negative element and constitutes a first reason for particularly considering
weight functions $f$ over $P$ being defined over non-negative integers
including $\mathcal{F}^{+}$.

The following corollary can directly be deduced from the fact that any
semiflow in $\mathcal{F}^{+}$ satisfies property 2:

###### Corollary 1

For any place $p$ belonging to at least one support of a semiflow of
$\mathcal{F}^{+}$, an upper bound $\mu$ can be defined for the marking of $p$
such that:

$\forall q\in RS(PN,q_{0}),\ \
q(p)\leq\mu(p,q_{0})=\min_{\\{f\in\mathcal{F}^{+}\ |\ f(p)\neq
0\\}}\frac{f^{\top}q_{0}}{f(p)}\ $

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),\ \ \ \ \forall t\in T$ (4)

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. In [Bra82],
$f^{T}Pre(\cdot,t)$ is called the enabling threshold of $t$.

###### Property 3

If $t$ is a transition and $\exists f\in\mathcal{F}^{+}\setminus\\{0\\}$ such
that:

$f^{T}q_{0}<f^{T}Pre(\cdot,t)$, then $t$ cannot be executed from $\langle
M,q_{0}\rangle$.

This property can be used when looking for a frugal management of resources
(i.e. a marking as small as possible) and still fully functioning (i.e. live).
Another application is when the model is defined with parameters, then, some
values of these parameters for which the model is not live (see example of
figure 2) can be directly deduced from theorem 4.4.

At last, the following property can easily be proven true in $\mathcal{F}^{+}$
and not true in $\mathcal{F}$:

###### Property 4

If $f$ and $g$ are two semiflows with no negative coefficients, then we have:
$\left\|f+g\right\|=\left\|f\right\|\cup\left\|g\right\|$.

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

This property can already be found in [Mem78] or [Bra82] .

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 the domain of biomolecular
chemistry relatively to chemical reaction networks [JACB18] which brings us
back to the original vision of C. A. Petri 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

###  4.1 Generating sets

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 [Mem77] to a large array of applications used especially to analyze
Petri Nets [CTSH03, DL16, JACB18, Wol19].

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

###  4.2 Basic definitions and results

###### Definition 2

A subset $\mathcal{G}$ of $\mathcal{F^{+}}$ is a generating set over a set
$\mathbb{S}$ (where $\mathbb{S}\in\\{\mathbb{N},\mathbb{Q^{+}},\mathbb{Q}\\}$
with $\mathbb{Q^{+}}$ denoting the set of non-negative rational numbers) if
and only if $\forall f\in\mathcal{F}^{+}$ we have
$f=\sum_{g_{i}\in\mathcal{G}}\alpha_{i}g_{i}$ where $\alpha_{i}\in\mathbb{S}$
and $g_{i}\in\mathcal{G}$.

Since $\mathbb{N}\subset\mathbb{Q^{+}}\subset\mathbb{Q}$, 222 Where $\subset$
denotes the strict inclusion between sets. 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. Therefore, it is important to precise over
which set the coordinates (used for the decomposition of a semiflow) belong.

-If $\mathcal{G}$ is a generating set over $\mathbb{Q}$ then

$\mathcal{V(G)}=\\{f\in\mathbb{Q}{{}^{d}}\ |\
f=\sum_{i=1}^{i=k}\alpha_{i}g_{i}\ \text{and}\ \alpha_{i}\in\mathbb{Q}\\}$ is
a vector space and $\mathcal{F^{+}}=\mathcal{V(G)}\cap\mathbb{N}{{}^{d}}$. We
can extract from $\mathcal{G}$ a basis of $\mathcal{V(G)}$ (see, for instance,
[Lan02] p. 85) which also is a generating set of $\mathcal{F^{+}}$ over
$\mathbb{Q}$ since the elements of this basis are in $\mathcal{F^{+}}$.

###  4.3 Minimal supports and minimal semiflows

The fact that there exists a finite generating set over $\mathbb{N}$ is non
trivial. This result was proven by Gordan circa 1885 then Dickson circa 1913.
Here, we directly rewrite Gordan’s lemma [AB86] by adapting it to our
notations.

###### Lemma 1

(Gordan circa 1885) Let $\mathcal{F^{+}}$ be the set of non-negative integer
solutions of the system of equations (1). Then, there exists a finite
generating set of vectors in $\mathcal{F^{+}}$ such that every element of
$\mathcal{F^{+}}$ is a linear combination of these vectors with non-negative
integer coefficients.

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

Several definitions around the concept of minimal semiflow were introduced in
[STC98] p. 319, in [CST03] p. 68, [KJ87], [CMPAW09], or in [Mem78, Mem83],
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 componentwise partial order on $\mathbb{N}{{}^{d}}$ since the
various definitions we found in the literature as well as the results of this
note can be described in terms of these sole two classic notions.

######  Definition 3 (minimal support)

A non-empty support $\left\|f\right\|$ of a semiflow $f$ is minimal with
respect to set inclusion if and only if $\nexists\
g\in\mathcal{F}^{+}\setminus\\{0\\}$ such that
$\left\|g\right\|\subset\left\|f\right\|$.

######  Definition 4 (minimal semiflow)

A non-null semiflow $f$ is minimal with respect to $\leq$ if and only if
$\nexists\ g\in\mathcal{F^{+}}\setminus\\{0,f\\}$ such that $g\leq f$.

In other words, a minimal semiflow cannot be decomposed as the sum of another
semiflow and a non-null non-negative vector. This remark yields initial
insight into the foundational role of minimality regarding the decomposition
of semiflows. We are looking for characterizing generating sets such that they
allow analyzing various behavioral properties as efficiently as possible.

The notion of minimality is key to decompose semiflows then to analyze
behavioral properties concisely. First, if we were to consider a generating
set over $\mathbb{N}$, then we may have to explore every minimal semiflow.
Although finite, the number of minimal semiflows can be quite large. Second,
considering a basis over $\mathbb{Q}$ is of course relevant to handle
$\mathcal{F}$ less when it is about $\mathcal{F}^{+}$ and may not capture
behavioral constraints as easily (see the example of Section 6.2).

###  4.4 Three decomposition theorems

Generating sets can be characterized thanks to a set of three decomposition
theorems. A first version of them can be found in [Mem78] with their proofs. A
second version version can be found in [Mem23] with few improvements. Here,
only theorem 4.1 which is valid over $\mathbb{N}$ is extended to fully
characterize minimal semiflows and generating sets over $\mathbb{N}$, and is
provided with a new proof using Gordan’s lemma 1. Theorems 4.2 and 4.3 are
recalled for completeness and are unchanged from [Mem23].

####  4.4.1 Decomposition over non-negative integers

###### Theorem 4.1

(Decomposition over $\mathbb{N}$)

A semiflow is minimal if and only if it belongs to any generating set 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\leq i\leq k$.
Then, $\exists a_{1},...,a_{k}\in\mathbb{N}$ such that
$f=\sum_{i=1}^{i=k}a_{i}f_{i}$. Since $f\neq 0$ and all coefficients $a_{i}$
are in $\mathbb{N}$, $\exists j\leq k$ such that $0<f_{j}\leq a_{j}f_{j}\leq
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}$
333This point is taken for granted in [Mem78] as well as the rest of
literature on semiflows.. 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$:

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}\in\mathcal{F^{+}}$ and $\nexists e_{i}\in\mathcal{E}$ such that
$e_{i}\leq r_{n}$. This means that $r$ is either minimal or null. Since
$\mathcal{E}$ includes all minimal semiflows, therefore, $r=0$, and any
semiflow can be decomposed as a linear combinations of minimal semiflows, in
other words, $\mathcal{E}$ is a finite generating set. 444If $\mathcal{E}$ was
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\limits_{n\to\infty}f-\sum_{j=1}^{j=n}k_{j}e_{j}=0$ with the same
definition of the coefficients $k_{j}$ as in ii). 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.4.2 Decomposition over semiflows of minimal support

This theorem 4.2 can already be found in [Mem23].

###### Theorem 4.2

(Minimal support) If $I$ is a minimal support then

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

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

In other words, $\\{f\\}$ is a unique generating set over $\mathbb{N}$ for
$\mathcal{F}_{I}^{+}=\\{g\in\mathcal{F^{+}}\ |\ \left\|g\right\|=I\\}$.
However, this uniqueness property is indeed 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}$.

###### Theorem 4.3

(Decomposition over $\mathbb{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, $\forall f\in\mathcal{F^{+}}$ such that $\left\|f\right\|\subseteq
I$, one has $f=\sum_{i=1}^{i=N}\alpha_{i}g_{i}$ where $\forall
i\in\\{1,2,...N\\},\ \alpha_{i}\in\mathbb{Q^{+}}$ and the semiflows $g_{i}$
are such that $\left\|g_{i}\right\|=I_{i}$.

A sketch of proof of theorem 4.3 can be found in [Bra82], a complete proof in
[Mem78].

###  4.5 Three extremums drawn from the notion of semiflow

The knowledge of any finite generating set allows a practical computation of
the three extremums directly inspired from property 10 Section 5.2, corollary
1 and property 4 of Section 3. Let us define them:

###### Definition 5

Given an initial state $q_{0}$ and the set of semiflows $\mathcal{F^{+}}$, the
three following limits can be defined:

  * •

$\iota=\bigcap_{f\in\mathcal{F^{+}}}HS(f,q_{0})$, where $HS(f,q_{0})=\\{q\in
Q\ |\ f^{\top}q=f^{\top}q_{0}\\}$,

  * •

$\mu(p,q_{0})=\min_{\\{f\in\mathcal{F}^{+}\ |\ f(p)\neq
0\\}}\frac{f^{\top}q_{0}}{f(p)}$ is the lowest bound that can be built from a
semiflow the support of which contains the given place $p$ in $P$,

  * •

$\rho=\left\|\sum_{f\in\mathcal{F}^{+}}f\right\|$ is the largest support of
any semiflow in $\mathcal{F^{+}}$.

Theorem 4.4 expresses the fact that these extremums are computable as soon as
any generating set is available:

###### Theorem 4.4

Let’s $\mathcal{E}=\\{e_{1},...e_{N}\\}$ be any finite generating set of
$\mathcal{F}^{+}$, and $q_{0}\in Q$ an initial state:

  * •

If $\mathcal{E}$ is over $\mathbb{S}$ then we have:

$\iota=\bigcap_{f\in\mathcal{F^{+}}}HS(f,q_{0})=\bigcap_{e_{i}\in\mathcal{E}}HS(e_{i},q_{0})$,

  * •

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}^{+}$,
$\forall q\in RS(PN,q_{0})$, we have :

$q(p)\leq\mu(p,q_{0})=\min_{\\{f\in\mathcal{F}^{+}\ |\ f(p)\neq
0\\}}\frac{f^{\top}q_{0}}{f(p)}=\min_{\\{e_{i}\in\mathcal{E}\ |\ e_{i}(p)\neq
0\\}}\frac{{e_{i}}^{\top}q_{0}}{e_{i}(p)}$,

  * •

If $\mathcal{E}$ is over $\mathbb{S}$ then we have:

$\rho=\left\|\sum_{f\in\mathcal{F}^{+}}f\right\|=\bigcup_{f\in\mathcal{F}^{+}}\left\|f\right\|=\bigcup_{e_{i}\in\mathcal{E}}\left\|e_{i}\right\|$

First, the three extremums are computable since by Gordan’s lemma of section
4.2, there exists a finite generating set such as $\mathcal{E}$.

  * •

For the first item, 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}}HS(e_{i},q_{0})$, then:

$\alpha_{i}(e_{i}^{\top}q)=\alpha_{i}(e_{i}^{\top}q_{0})\ \forall
i\in\\{1,...N\\}$, 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:

$f^{\top}q=f^{\top}q_{0}$, and $q\in HS(f,q_{0})\ \ \forall
f\in\mathcal{F^{+}}$ therefore,

(since $\mathcal{E}\subset\mathcal{F^{+}}$ directly involves
$(\bigcap_{f\in\mathcal{F^{+}}}HS(f,q_{0}))\subseteq\bigcap_{e_{i}\in\mathcal{E}}HS(e_{i},q_{0})$)
we have:

$\bigcap_{e_{i}\in\mathcal{E}}HS(e_{i},q_{0})=\bigcap_{f\in\mathcal{F^{+}}}HS(f,q_{0})=\iota$.

  * •

For the second item of the theorem, let’s consider a state $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}\geq 0\ \forall
i\in\\{1,...N\\}$.

Let’s define $\mu_{\mathcal{E}}$ such that:
$\mu_{\mathcal{E}}=\min_{\\{e_{i}\in\mathcal{E}\ |\ e_{i}(p)\neq
0\\}}\frac{{e_{i}}^{\top}q_{0}}{e_{i}(p)}$.

Then $\exists j$ such that $1\leq j\leq N$, and
$\mu_{\mathcal{E}}=\frac{{e_{j}}^{\top}q_{0}}{e_{j}(p)}$.

Therefore, $\forall i\leq N$, such that $e_{i}(p)\neq 0$,
$\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:

$\mu_{\mathcal{E}}=\frac{\alpha_{j}{e_{j}}^{\top}q_{0}}{\alpha_{j}e_{j}(p)}=\frac{\alpha_{i}({e_{i}}^{\top}q_{0}-\delta_{i})}{\alpha_{i}e_{i}(p)}\
\forall i$ such that $e_{i}(p)\neq 0$, therefore:

$\mu_{\mathcal{E}}=\frac{\sum_{\\{i\ |\
e_{i}(p)>0\\}}\alpha_{i}({e_{i}}^{\top}q_{0}-\delta_{i})}{\sum_{\\{i\ |\
e_{i}(p)>0\\}}\alpha_{i}e_{i}(p)}$

$=\frac{\sum_{\\{i\ |\
e_{i}(p)>0\\}}\alpha_{i}({e_{i}}^{\top}q_{0}-\delta_{i})+\sum_{\\{i\
|e_{i}(p)=0\\}}(\alpha_{i}{e_{i}}^{\top}q_{0}-\alpha_{i}{e_{i}}^{\top}q_{0})}{\sum_{\\{i\
|\ e_{i}(p)>0\\}}\alpha_{i}e_{i}(p)}$

$=\frac{\sum_{\\{i|e_{i}(p)>0\\}}\alpha_{i}{e_{i}}^{\top}q_{0}+\sum_{\\{i|e_{i}(p)=0\\}}\alpha_{i}{e_{i}}^{\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}}{\sum_{\\{i\ |\
e_{i}(p)>0\\}}\alpha_{i}e_{i}(p)+\sum_{\\{i\ |\
e_{i}(p)=0\\}}\alpha_{i}e_{i}(p)}$

since $\sum_{\\{i\ |\ e_{i}(p)=0\\}}\alpha_{i}e_{i}(p)=0$. Then, since
$\delta_{i}\geq 0$ and $\alpha_{i}\geq 0\ \forall i$ such that $1\leq i\leq N$

$\mu_{\mathcal{E}}=\frac{\sum_{i=1}^{i=N}\alpha_{i}{e_{i}}^{\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}}{\sum_{i=1}^{i=N}\alpha_{i}e_{i}(p)}$

$\mu_{\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)}\leq\frac{f^{\top}q_{0}}{f(p)}$

This being verified for any semiflow of $\mathcal{F}^{+}$, we have:
$\mu(p,q_{0})=\mu_{\mathcal{E}}$.

  * •

For the third item of the theorem, let’s consider $\mathcal{E}$ a generating
set over $\mathbb{S}$ then, any semiflow $f$ can be decomposed as follows:

$f=\sum_{\alpha_{i}>0}\alpha_{i}e_{i}+\sum_{\alpha_{i}<0}\alpha_{i}e_{i}$
where $\alpha_{i}\in\mathbb{S}$. $f\in\mathcal{F}^{+}$ means that at least one
coefficient $\alpha_{i}$ is strictly positive and
$\sum_{\alpha_{i}<0}|\alpha_{i}|e_{i}+f=\sum_{\alpha_{i}>0}\alpha_{i}e_{i}\neq
0$.

Therefore, applying property 4:

$\left\|f\right\|\subseteq\left\|\sum_{\alpha_{i}<0}|\alpha_{i}|e_{i}+f\right\|=\left\|\sum_{\alpha_{i}>0}\alpha_{i}e_{i}\right\|=\bigcup_{\alpha_{i}>0}\left\|\alpha_{i}e_{i}\right\|\subseteq\bigcup_{e_{i}\in\mathcal{E}}\left\|e_{i}\right\|$.

Hence,
$\rho=\left\|\sum_{f\in\mathcal{F}^{+}}f\right\|=\bigcup_{e_{i}\in\mathcal{E}}\left\|e_{i}\right\|$
$\square$

This theorem means that these three extremums $\iota$, $\mu$ and $\rho$ can be
computed with the help of one finite generating set. The third part of this
theorem means that if $\mathcal{E}=\\{e_{1},...e_{N}\\}$ is any generating set
of a given Petri Net PN then
$\bigcup_{e_{i}\in\mathcal{E}}\left\|e_{i}\right\|$ is also the largest
support of PN (it would be useless to look for another semiflow).

##  5 Home spaces and home states

The notion of home space was first defined in [Mem83] for Petri Nets
relatively to a single initial state. Here, we effortlessly extend its
definition relatively to a nonempty subset of states. Verifying that a set of
states is a home space is possible as soon as a conceptual model supports
building up Reachability Sets ($RS$) and associated reachability graphs ($RG$
and $LRG$ for Reachability Graph, and Labeled Reachability Graph
respectively).

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

###  5.1 Definitions and basic properties

Given a model $M$, its associated state space $Q$ and a subset $Init$ of $Q$,
we say that a set _HS_ is an Init-home space if and only if for any
progression of the model $M$ from any element of $Init$, there exists a way of
prolonging this progression and reach an element of _HS_. In other words:

###### Definition 6

Given a nonempty subset $Init$ of $Q$, a set HS is an Init-home space if and
only if $\forall q\in RS(M,Init)$, $\exists h\in\emph{HS}$ such that $h$ is
reachable from $q$ (i.e. such that $q\overset{*}{\rightarrow}h$).

HS is a well-structured home space if and only if: $\forall q\in Q$, $\exists
h\in\emph{HS}$ such that $q\overset{*}{\rightarrow}h$.

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

We immediately have $HS\cap RS(M,Init)\neq\varnothing$. However, depending on
the definition of $Q$ and for algebraic reasons, we must point out that $HS$
is not necessarily included in $Q$ and we may have $h\in HS$ such that for
some state variables $x_{i},\ h(x_{i})\notin D_{i}$ ($D_{i}$, being the domain
in which $x_{i}$ varies in $Q$).

If $HS$ is a well-structured home space then $\forall Init\in
2^{Q}\setminus\\{\emptyset\\}$, $HS$ is an Init-home space. Also, if $A$ is
such that $Q=RS(M,A)$ and HS is an A-home space then HS is a well-structured
home space.

###### Definition 7

A state $s$ is an home state if and only if $\\{s\\}$ is an $\\{s\\}$-home
space.

This last definition is directly drawn from the definition given in [Bra82]
p.59 or in [GV03] p. 63 for Petri Nets. It can be found in many papers such as
[HDK14].

In many systems, the initial state $q_{0}$ represents an idle state from which
the various capabilities of the system can be enabled. In this case, it is
important for $q_{0}$ to be a home state. This property is usually guarantied
by a reset function which can be modeled in a simplistic way by adding a
transition $r$ such that $\forall q\in RS(M,q_{0}),\ q_{0}\in r(q)$ (which
means that $r$ is executable from any reachable state and that its execution
reaches $q_{0}$). However, 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 A-home space. This
question is addressed in [JL22] and is proven decidable for home state when
the conceptual model is a Petri Net but is still open in a more general case.
Furthermore, a corpus of decidability properties can be found in [VJ85, FEJ89,
FH24], or [JL22]. It may be worth mentioning the straightforward following
properties, given a subset of states, $A$:

###### Property 5

Any set containing an A-home space is also an A-home space. 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 A1-home space and $HS_{2}$ is an A2-home space then $HS_{1}\cup
HS_{2}$ is an ($A1\cup A2$)-home space.

However, the intersection of two home spaces is not necessarily a home space.
Figure 1 is representing the reachability graph of a transition system with
eight states. $HS_{1},HS_{2},HS_{3}$ as defined Figure 1 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 1: $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}\\},\
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.

Given a model $M$ and a subset of states $Init$, a sink is a state with no
successor in the associated reachability graph $RG(M,Init)$.

###### Property 6

If there exists a sink $q_{f}\in RG(M,Init)$ then it belongs to any Init-home
space. More generally, any home space has at least one element in each
strongly connected component sink of the reachability graph 555It is easy to
prove that this property holds even when the reachability graph is 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..

For the following property, we consider a model $M$ paired with a single
initial state $q_{0}$.

###### Property 7

The three following statements are equivalent:

  * (i)

the initial state is a home state (then there is no sink),

  * (ii)

every reachable state is a home state,

  * (iii)

the reachability graph is strongly connected.

###  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 [BEI+20]) such as safeness, boundedness, or more
complex behavioral properties such as liveness. Let us provide three
properties supporting this idea.

Dom(t) will denote the subset of states from which the transition $t$ is
executable and Im(t) the subset of states which can be reached by the
execution of $t$.

###### Property 8

A transition $t$ is live if and only if Dom(t) is a home space.

Moreover, if Dom(t) is a home space then Im(t) is also a home space.

This relationship is further supported when considering the following property
regarding home states:

###### Property 9

Let $M$ be a model and $q_{0}$ be a home state then:

any transition that is enabled from $q_{0}$ is live,

more generally,

a transition is live if and only if it appears as a label in $LRG(M,q_{0})$.

This can easily be proven directly from the definition of liveness and the
property 7 about home states . $\square$

Given an initial state $q_{0}$, each semiflows can be associated with an
invariant which 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\ |\
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:
$\forall\alpha\in\mathbb{Q}\setminus\\{0\\},HS(\alpha f,q_{0})=HS(f,q_{0})$,

$\forall f,g\in\mathcal{F},\forall\alpha,\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.

$HS(f,q_{0})\ \cap\ HS(g,q_{0})$ is straightforwardly a $\\{q_{0}\\}$-home
space since they both contain $RS(M,q_{0})$. Let us recall that in general,
the intersection of home spaces is not a home space (see Figure 1). 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}$, therefore,
$q\in HS(\alpha f+\beta g,q_{0})$ $\square$

These three properties provide us with a methodology to analyze and prove that
a subset of transitions are live. From a set of invariants, we can define a
first home space $HS$ that concisely describe how tokens are distributed over
places. From this token distribution, we can analyze what transition are
enabled in order to prove that a specific given marking $q$ ($q_{0}$ being the
usual case) is always reachable from any element of $HS$. When this is
possible, it can easily be deduced that $q$ is a home state. Then, it may be
possible using property 9 to prove which transition are live and whether the
Petri Net is live or not. This will be illustrated later with a few examples
in section 6.

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

Invariants, semiflows, and home spaces can be used to prove a rich array of
behavioral properties of conceptual models such as labeled transition system
or Petri Net even within different settings, in particular when using
parameters.

We used to prove liveness by starting by a known home space then proceeding
cases by cases, sub-case by sub-cases using a generating set of semiflows, we
can often prove that the initial state is a home state (definition 7) and from
there conclude to the liveness of the model using properties 9 (see example in
[VM84, Mem23]. Here, through two parameterized examples, we proceed by using
basic arithmetic for the first example, or by refinement of home spaces in the
second example. This methodology brings us closer to an automated analysis to
address liveness in parameterized models.

Analysis can be performed with incomplete information on the initial marking
as shown in the first example below or on a subsystem exhibiting some
compositionality ability. It can be described with parameters which will make
the invariant calculus more complex but still tractable as shown in the
subsequent examples. Most of the time, especially with actual system models,
it will be possible to conclude avoiding a painstaking symbolic model checking
or a parameterized and complex development of a reachability graph [DRvB01].
At the very least it could be envisioned to combine this method with existing
ones in order to get an acceleration.

###  6.1 A tiny example

The Petri Net $TN=\langle\\{A,B\\},\\{t_{1},t_{2}\\},Pre,Post\rangle$ in
Figure 2 is defined by:

$Pre(\cdot,t_{1})^{\top}=(k,0);Pre(\cdot,t_{2})^{\top}=(1,1)$;

$Post(\cdot,t_{1})^{\top}=(0,1);Post(\cdot,t_{2})^{\top}=(k+1,0).$

This example can be first found in [Bra82] or in [Mem83] without proof. Here,
the analysis is generalized by introducing a parameter $k$ such that $k>1$.

What is remarkable about the analysis of this tiny example is 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 an
additional parameter and without even considering the value taken by
$q_{0}(B)$ ).

Figure 2: This parameterized version TN(k) of our tiny Petri Net is live if
and only if $g^{\top}q_{0}>k$ and is not a multiple of $k$, whatever is the
initial marking of $B$. For $k=1$, the Petri Net has no live transition
whatever is the initial marking.

We have the following minimal semiflow: $g^{\top}=(1,k)$ and we can show that
the TN(k) is not live if and only if $g^{\top}q_{0}\leq k$ or
$g^{\top}q_{0}=nk$ where $n\in\mathbb{N}$, independently of $q_{0}(B)$ which
could be considered as a second parameter.

First, if $g^{\top}q_{0}<k$ 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}\geq k$ then we consider the Euclidean division of
$g^{\top}q_{0}$ by $k$ giving: $g^{\top}q_{0}=nk+i$ where $i<k$ then since $g$
is a semiflow, $g^{\top}q=q(A)+kq(B)\equiv i\ (mod\ k)$ therefore $q(A)\equiv
i\ \forall q\in RS(TN(k),q_{0})$. If $i=0$ then we have $q(A)=nk-kq(B)$ and
$t_{1}$ can be enabled $n-q(B)$ times to reach a marking with zero token in
$A$. If $i\neq 0$ and $g^{\top}q_{0}>k$ then $q(A)\neq 0$ and either $q(A)>k$
or $q(B)\neq 0\ \forall q\in RS(TN(k),q_{0})$. In the first case, $t_{1}$ is
enabled; in the second case $t_{2}$ is enabled. It is easy to conclude that
the Petri Net $TN(k)$ is live if and only if $g^{\top}q_{0}>k$ and is not a
multiple of $k$ whatever is the initial marking of $B$. $\square$

Even if adding more resources to the system under study can bring confidence
that some actions will eventually be performed, this does not necessarily
result in solving a deadlock issue; this could even create a deadlock
situation! In this regard, adding more resources may ends up as a “false good
idea” that is encountered with many students. This is certainly one of the
reasons why the coverability tree does not allow to study liveness [Fin93].

###  6.2 A parameterized example from the telecommunication industry

The Petri Net $TEL(x,y)=\langle P_{TEL},T_{TEL},Pre,Post\rangle$ is described
Figure 3

where $P_{TEL}=\\{LA,CLA,WLA,A,CA,PU,S,F,R\\}$

and $T_{TEL}=\\{t_{1},t_{2},t_{3},t_{4},t_{5},t_{6},t_{7},t_{8},t_{9}\\}$.

TEL(x,y) is a reduced Petri Net version of a Fifo Net published in [MF85,
MM81]. It is well known that reduction rules preserve liveness, however, it is
also well known that some rules do not preserve boundedness 666See [Bra82,
CTSH03] for Petri Nets reduction rules.. A sketchy and incomplete version of
the analysis hereunder is published in [Mem23].

This example is representing two subscriber types, “a caller" and a “callee,"
having a conversation (places $CLA$ and $CA$ respectively). We simplify the
model by taking into account only the actions related to calling for the
caller and the actions related to being called for the callee. Initially, they
are in an idle state with places $LA$ and $A$ marked with one token per
subscriber. We will want this principle be satisfied for any evolution of
TEL(x,y). Signals $PU$ and $R$ are sent from the caller to the callee and
signals $S$ and $F$ from the callee to the caller. The overall desired
behavior is that caller and callee cannot go back to their idle state as long
they have not received all the signals sent to them despite the fact that they
both can hang up at any time making the order in which signals $F$ and $R$ are
sent and received undetermined.

From their idle state (place $LA$), the caller can pick up their phone
(transitions $t_{1}$) sending the signal $PU$ to the callee. From their idle
state (place $A$), the callee, upon receiving the signal $PU$, can pick up
their phone (transition $t_{7}$), send the signal $S$ and go to conversation
(place $CA$) from where they can hang up (transition $t_{8}$) at any time
sending the signal $F$ to the caller. Receiving the signal $S$, the caller can
go (transition $t_{2}$) to the conversation (place $CLA$). They can also hang
up at any time (transitions $t_{3},t_{4},t_{5}$) sending the signal $R$ to the
callee. After hanging up via $t_{4}$ or $t_{5}$, the caller will have to wait
(place $W$) until they receive the signal $F$ from the callee before going
back (transition $t_{6}$) to their initial idle state $LA$. The callee can go
back to their idle state $A$ only upon receiving the signal $R$ (transition
$t_{9}$).

The initial state $q_{0}$ is such that $q_{0}(LA)=x,q_{0}(A)=y$ and
$q_{0}(p)=0$ for any other place: the modeled system is in its idle state.

Figure 3: This Petri Net TEL(x,y) has exactly three minimal semiflows of
minimal support, constituting a generating set over $\mathbb{Q}^{+}$:
$\mathcal{GB}_{1}=\\{f_{1},\ f_{2},\ f_{3}\\}$ such that:
$f_{1}(LA)=f_{1}(CLA)=f_{1}(WLA)=f_{1}(PU)=f_{1}(S)=\ 1$ and $f_{1}(p)=\ 0$
for any other place,
$f_{2}(LA)=f_{2}(PU)=f_{2}(F)=f_{2}(CA)=\ 1$ and $f_{2}(p)=\ 0$ for any other
place,
$f_{3}(CLA)=f_{3}(S)=f_{3}(R)=f_{3}(A)=\ 1$ and $f_{3}(p)=\ 0$ for any other
place.
$\mathcal{GB}_{1}$ and its corresponding invariants are concisely represented
by a tableau Figure 4.

####  6.2.1 Proving the TEL(x,y) example with parameters

A similar analysis scheme could be conducted with a colored Petri Net instead
of the Petri Net of Figure 3 with two parameters to model $x$ callers and $y$
callees, where $x>0$ and $y>0$. Considering the parameterized Petri Net of
Figure 3, the initial state $q_{0}$ becomes: $q_{0}(LA)=x,\ q_{0}(A)=y$ and
$q_{0}(p)=0$ for any other place $p$. The generating set
$\mathcal{GB}_{1}=\\{f_{1},\ f_{2},\ f_{3}\\}$ is minimal and its three
associated invariants are:

$\forall q\in RS(TEL(x,y),q_{0})$:

$f_{1}^{\top}q=f_{1}^{\top}q_{0}=x$, $f_{2}^{\top}q=f_{2}^{\top}q_{0}=x$,
$f_{3}^{\top}q=f_{3}^{\top}q_{0}=y$,

as described Figure 4.

Figure 4: This tableau is concise way to represent a generating set and
corresponding invariants of $\mathcal{GB}_{1}$. It reads for instance:
$f_{1}(LA)=1$ or $f_{1}(A)=0$. The three semiflows $f_{1},\ f_{2},\ f_{3}$ do
not depends on the initial state (even enriched with parameters); only the
evaluation functions of the three corresponding invariants are depending on
the initial state, therefore are defined with parameters.

This time, we want to prove that TEL(x,y) is live and satisfies the following
property:

$\mathcal{P}_{1}(x,y):HS(z)=\\{q|\ q(CLA)=q(CA)=z\ \text{and}\ z\leq
min(x,y)\\}$ is a home space,

$\mathcal{P}_{2}(x,y):\forall q\in RS(TEL(x,y),q_{0})$, $q(CLA)\leq min(x,y)$
and $q(CA)\leq min(x,y)$.

First, from property 10 that $HS_{0}=\\{q\in Q\ |\
f_{1}^{\top}q=f_{2}^{\top}q=x,\text{and}f_{3}^{\top}q=y$ } is a home space.

From any state $q\in HS_{0}$, it is always possible to execute the sequence:

$\sigma_{1}=(t_{5}t_{9})^{q(S)}(t_{4}t_{9})^{q(CLA)}t_{9}^{q(R)}$. We then
reach a state $q_{1}$ such that $q_{1}(S)=q_{1}(CLA)=q_{1}(R)=0\ $ defining a
second home space $HS_{1}=\\{q\in HS_{0}\ |\ q(S)=q(CLA)=q(R)=0\\}$. From the
invariant associated with $f_{3}$, it can be directly deduced that $\forall
q_{1}\in HS_{1}$, we have $q_{1}(A)=y$. Similarly, it is always possible to
empty $CA$ from its tokens: $\forall q_{1}\in HS_{1}$, it is always possible
to execute $\sigma_{2}=t_{8}^{q(CA)}$ reaching a state $q_{2}$ such that
$q_{2}(CA)=0$ defining a third home space $HS_{2}=\\{q\in HS_{1}\ |\
q(CA)=0\\}$.

Since $y>0$, from any state $q_{2}$ in $HS_{2}$, it is always possible to
execute the sequence:

$\sigma_{3}=(t_{7}t_{5}t_{9}t_{8})^{q_{2}(PU)}$. We then reach a state $q_{3}$
still in $HS_{2}$ (each time $t_{7}$ puts a token in $S$ and $CA$, we can
execute $t_{5}t_{9}$ and $t_{8}$ respectively to return to $HS_{2}$) such that
$q_{3}(PU)=0$ defining a fourth home space $HS_{3}=\\{q\in HS_{2}\ |\
q(PU)=0\\}$. From the two invariants associated with $f_{1}$ and $f_{2}$, it
can be deduced that $\forall q\in HS_{3}$, we have $q(LA)+q(WLA)=x$ and
$q(LA)+q(F)=x$ respectively, hence necessarily, $q(WLA)=q(F)$. Therefore, from
any state $q_{3}$ in $HS_{3}$, it is always possible to execute the sequence:
$\sigma_{4}=t_{6}^{q_{3}(F)}$ reaching a state $q_{4}$ still in $HS_{3}$ such
that $q_{4}(WLA)=q_{4}(F)=0$ therefore, $q_{4}(LA)=x$. The only such state is
$q_{0}$ which being always reachable via the sequence
$\sigma_{1}\sigma_{2}\sigma_{3}\sigma_{4}$, is a home state. From there,
$t_{1}$ is live (from property 9) and it becomes easy to prove that the Petri
Net is live.

Figure 5: TEL2(x,y): By adding the place $WA$ and connecting it to the
transitions $t_{8}$ and $t_{9}$, we generate a fourth minimal semiflow without
changing the three first ones.
$f_{4}(A)=f_{4}(CA)=f_{4}(WA)=\ 1$ and $f_{1}(p)=\ 0$ for any other place

From $q_{0}$ home state, we can always execute the sequence
$\sigma_{z}=(t_{1}t_{7}t_{2})^{z}$ as long as $z\leq min(x,y)$; therefore
$HS(z)=\\{q|\ q(CLA)=q(CA)=z\ \text{and}\ z\leq min(x,y)\\}$ is a home space
meaning that it is always possible to have $z$ pairs of subscribers in a
conversation at the same time which satisfies $\mathcal{P}_{1}(x,y)$.

Furthermore, by applying theorem 4.4 using $\mathcal{GB}_{1}$, we directly
have:

$\forall q\in RS(TEL(x,y),q_{0}),q(CLA)\leq\mu(CLA,q_{0})=min(x,y)$.

This is the first half of property $\mathcal{P}_{2}(x,y)$ and it means that we
can only have up to $min(x,y)$ simultaneous conversations.

However, the same theorem allows deducing not only that:

$\forall q\in RS(TEL(x,y),q_{0}),q(CA)\leq\mu(CA,q_{0})=x$, but also that
there is not hope to find a better bound for $CA$ with the only help of
semiflows. Worse, it can be shown that $\mu(CA,q_{0})=x$ can be reached and
that $\mathcal{P}_{2}(x,y)$ is not satisfied. In the case where $x>y$, this
would model the fact that a callee can be in a simultaneous conversation with
several callers (which is a possibility today, but was not expected here).
Moreover, this situation does not comply with the principle of one token per
subscriber since we would have more than $y$ callee.

This situation is due to an oversimplification of TEL(x,y). By restoring one
reduction rule back and remembering that in particular, the callee process was
modeled by state machines, we construct the Petri Net $TEL2(x,y)$ of Figure 5.
$TEL2(x,y)$ has an augmented generating set
$\mathcal{GB}_{2}=\mathcal{GB}_{1}\cup\\{f_{4}$} where $f_{4}$ is a new
minimal semiflow such that $f_{4}(A)=f_{4}(CA)=f_{4}(WA)=\ 1$ and $f_{1}(p)=\
0$ for any other place and is directly associated with the following
invariant: $\forall q\in RS(TEL2(x,y),q_{0}),\
f_{4}^{\top}q=f_{4}^{\top}q_{0}=y$. We can apply theorem 4.4 again to $CA$ and
this time obtain $\forall q\in RS(TEL2(x,y),q_{0}),\
q(CA)\leq\mu(CA,q_{0})=min(x,y)$ and finish to prove $\mathcal{P}_{2}(x,y)$.
Indeed, it can be shown that with similar method of proofs, $TEL2(x,y)$
satisfies $\mathcal{P}_{1}(x,y)$ and is live. $\square$

##  7 Conclusion

As soon as we can associate the behavior of a system under study with a set of
state variables and follow its evolution through sequences of states forming a
reachability graph (or a structure) where each edge is associated with a
transition, we can assume the existence of an underlying Transition System.
Doing so, invariants and home spaces can be checked or proven along all
possible sequences and help understanding and verifying the functioning of
such a system.

It has been recalled how semiflows create a link from the static topology (the
bipartite graph) to the dynamic evolution (the variation of the number of
tokens) of the Petri Net. They support constraints over all possible markings
which greatly help analyzing and discovering behavioral properties (even some
unspecified ones). Semiflows infer a class of invariants with a constant
evaluation function that can be computed from the initial marking of the Petri
Net under consideration. Last but not least, they can be characterized by a
generating set that can be used in order to support some elegant level of
behavioral analysis even with the presence of some level of parameterization.

We believe that these results may be enriched along two different alleys. From
a mathematical point of view, the relation with integer linear programming or
convex geometry has been investigated many times, particularly in [CS89],
however, we believe it could be fruitful to look at the notion of toric
varieties and saturated semigroups [Oda12]. From a Petri Net and, even more
broadly, from a transition system theory point of view, applying these new
results to a variety of models (for example, colored Petri Nets or any
transition system that can be associated with a system of equations such as
Equation (1)) remains to be done.

Finally, we would like to stress the possibility to automate the proof scheme
exhibited throughout the parameterized examples of Section 6 in particular by
introducing tableaux (facilitating calculation) and a method by refinements of
home space which constitute two new steps towards this goal bringing
simplification and clarification compared to proceeding by cases and sub-cases
(used in [Mem23] and other papers).

## References

  * [AB86] N. Alon and K. A. Berman.  Regular hypergraphs, gordon’s lemma, steinitz’ lemma and invariant theory.  J. of Combinatorial Theory, A, 43:pp. 91–97, 1986.
  * [BEI+20] M. Bozga, J. Esparza, R. Iosif, J. Sifakis, and C. Welzel.  Structural invariants for the verification of systems with parameterized architectures.  In A. Biere and D. Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 228–246, Cham, (2020). Springer Int. Pub.
  * [Bra82] G. W. Brams.  Réseaux de Petri: Théorie et Pratique.  Masson, Paris, France, 1982.
  * [CMPAW09] G. Ciardo, G. Mecham, E. Paviot-Adet, and M. Wan.  P-semiflow computation with decision diagrams.  In Wolf K. (eds) Franceschinis G., editor, ATPN, Petri Nets 2009, LNCS 5606, pages 143–162. Springer, Berlin, Heidelberg, (2009).
  * [CS89] J. M. Colom and M. Silva.  Convex geometry and semiflows in P/T nets. A comparative study of algorithms for computation of minimal p-semiflows.  In G. Rozenberg, editor, Advances in Petri Nets 1990 [$10^{th}$ Int. Conf. on ATPN, Bonn, Germany, Proc.], LNCS 483, pages 79–112. Springer, 1989.
  * [CST03] J. M. Colom, M. Silva, and E. Teruel.  Properties.  In C. Girault and R. Valk, editors, Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications, pages 53–72. Springer Berlin Heidelberg, 2003.
  * [CTSH03] J. M. Colom, E. Teruel, M. Silva, and S. Haddad.  Structural methods.  In C. Girault and R. Valk, editors, Petri Nets for Systems Engineering, A guide to Modeling, Verification, and Applications, pages 277–316. Springer Berlin Heidelberg, 2003.
  * [DL16] L. W. Dworzanski and I. A. Lomazova.  Structural place invariants for analyzing the behavioral properties of nested petri nets.  In F. Kordon and D. Moldt, editors, ATPN and Concurrency, pages 325–344, Cham, 2016. Springer Int. Pub.
  * [DRvB01] G. Delzanno, J. F. Raskin, and L. van Begin.  Attacking symbolic state explosion.  In Proc. of the $13^{th}$ International Conference on Computer Aided Verification, CAV 2001, LNCS 2102, pages 298–310. Springer, (2001).
  * [FEJ89] D. Frutos Escrig and C. Johnen.  Decidability of home space property.  Technical report, Université Paris-Saclay, LRI, UA CNRS 410, RR n 503, 1989.
  * [FH24] A. Finkel and M. Hilaire.  Resilience and home-space for wsts.  In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation, pages 147–168, Cham, 2024. Springer Nature Switzerland.
  * [Fin93] A. Finkel.  The minimal coverability graph for petri nets.  in W. Reisig and G. Rozenberg (Eds) Advances in Petri Nets, LNCS 674, pages pp. 210–243, 1993.
  * [GV03] C. Girault and R. Valk.  Petri Nets for Systems Engineering, A guide to Modeling, Verification, and Applications.  Springer, 2003.
  * [HDK14] Thomas Hujsa, Jean-Marc Delosme, and Alix Munier Kordon.  Polynomial sufficient conditions of well-behavedness and home markings in subclasses of weighted petri nets.  ACM Trans. Embed. Comput. Syst., 13(4s):141:1–141:25, 2014.
  * [JACB18] M. D. Johnston, D. F. Anderson, G. Craciun, and R. Brijder.  Conditions for extinction events in chemical reaction networks with discrete state spaces.  J. Mathematical Biology, 76,6:pp. 1535––1558, 2018.
  * [JL22] P. Jančar and J. Leroux.  Semilinear home-space is decidable for petri nets.  arXiv 2207.02697, 2022.
  * [KJ87] F. Krückeberg and M. Jaxy.  Mathematical methods for calculating invariants in petri nets.  In G. Rozenberg, editor, Advances in Petri Nets 1987, pages 104–131. Springer Berlin Heidelberg, 1987.
  * [Lan02] S. Lang.  Algebra, $3^{rd}$ revised Ed. GTM, Springer, 2002.
  * [Mem77] 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), pages pp. 145–150, 1977.
  * [Mem78] 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.
  * [Mem83] 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.
  * [Mem23] Gerard Memmi.  Minimal generating sets for semiflows.  In Marieke Huisman and António Ravara, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 189–205, Cham, 2023. Springer Nature Switzerland.
  * [MF85] G. Memmi and A. Finkel.  An introduction to fifo nets-monogeneous nets: A subclass of fifo nets.  Theor. Comput. Sci., 35:191–214, 1985.
  * [MM81] R. Martin and G. Memmi.  Specification and validation of sequential processes communicating by fifo channels.  In $4^{th}$ Int. Conf. on Software Engineering for Telecommunication Switching Systems, Warwick U. Conventry, U.K, pages 54–57. SIEE, 1981.
  * [Oda12] T. Oda.  Convex Bodies and Algebraic Geometry (An Introduction to the Theory of Toric Varieties).  Springer, 2012.
  * [Sif78] J. Sifakis.  Structural properties of petri nets.  In J. Winkowski, editor, MFCS 1978, Proc. $7^{th}$ Symp., Zakopane, Poland, volume 64 of LNCS, pages 474–483. Springer, (1978).
  * [STC98] M. Silva, E. Teruel, and J. M. Colom.  Linear algebraic and linear programming techniques for the analysis of place/transition net systems, pages 309–373.  Springer Berlin Heidelberg, 1998.
  * [VJ85] Rüdiger Valk and Matthias Jantzen.  The residue of vector sets with applications to decidability problems in petri nets.  Acta Informatica, 21:643–674, 1985.
  * [VM84] J. Vautherin and G. Memmi.  Computation of flows for unary-predicates/transition-nets.  In G. Rozenberg, H. Genrich, and G. Roucairol, editors, Advances in Petri Nets 1984, European Workshop on Applications and Theory in Petri Nets, selected papers, volume 188 of LNCS, pages 455–467. Springer, 1984.
  * [Wol19] K. Wolf.  How Petri Net Theory Serves Petri Net Model Checking: A Survey, pages 36–63.  Springer Berlin Heidelberg, 2019.