After briefly recalling basic notations of Petri Nets, home spaces, and semiflows, we focus on ℱ +, the set of semilfows with non-negative coordinates where the notions of minimality of semiflows and minimality of supports are particularly critical to develop an efective 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 suficient 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 eficiently 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 eficiency brought by the combination of these results to the verification engineer.
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 diferent 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. Then, we show how basic arithmetic, linear algebra, or algebraic geometry can eficiently 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 [
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 [
The three decomposition theorems of Section 4.2 have been first published in [
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.
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 = ⟨, , , ⟩, where is a finite set of places and a finite set of transitions such that ∩ = Ø. A transition of is defined by its Pre(· , t ) and (· , ) conditions1: : × → N is a function providing a weight for pairs ordered from places to transitions, while : × → N is a function providing a weight for pairs ordered from transitions to places. Here, will denote the number of places: = | |.
A marking (or state in Transition Systems) : → N allows representing the evolution of the system along the execution (or firing ) of a transition or of a sequence of transitions (i.e., a word in 1We use here the usual notation: (· , )() = (, ) and (· , )() = (, ). * ). We say that is enabled at marking if and only if ≥ (· , ), and as an enabled transition at (we write that ∈ Dom()), can be executed, reaching a marking ′ from such that: ′ = + (· , ) − (· , ).
This is also denoted as ′ = () or more traditionally → ′ (we also write ′ ∈ Im()). Similarly, for a sequence of transitions allowing to reach a marking ′ from a marking , we write → ′. When the sequence of transitions allowing to reach a marking ′ from a marking is unknown, we may write →* ′. Given a marking , a place is said to contain tokens as () = .
We also define , 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 = N .
( , ) denotes the set of reachability of a Petri Net from a subset of : ( , ) = { ∈ | ∃ ∈ , →* }.
( , ), and ( , ) denote the reachability graph without labels (as in Figure 2) and with labels in respectively; while ( , 0) denote the labeled coverability tree given an initial marking 0.
The concept of semiflows over non negative integers were first described by Y.E. Lien [
In this section, we consider a Petri Net with its initial marking 0 and the set of reachable markings from 0 through all sequences of transitions denoted by ( , 0).
A Semiflow is a solution of the following homogeneous system of | | diodefinition 1 (Semiflow). phantine equations:
⊤ (· , ) = ⊤ (· , ), ∀ ∈ , where ⊤ denotes the scalar product of the two vectors and , since , (· , ) and (· , ) can be considered as vectors once the places of have been ordered.
ℱ and ℱ + denote the sets of solutions of the system of equations (1) that have their coeficients in Z and in N, respectively.
Any non-null solution of the homogeneous system of equations (1) allows to directly deduce the following invariant of defined by its and functions (used in the system of equations (1) that satisfies):
∀ ∈ ( , 0) : ⊤ = ⊤0.
In the rest of the paper, we abusively use the same symbol ‘0’ to denote (0, ..., 0)⊤ of N, for all in N. The support of a semiflow is denoted by ‖ ‖ and is defined by (1) (2) ‖ ‖ = { ∈ | () ̸= 0}.
We will use the usual component-wise partial order in which (1, 2, . . . , )⊤ ≤ (1, 2, . . . , )⊤ if and only if ≤ , for all ∈ {1, . . . , }.
The most interesting set of semiflows, from a behavioral analysis standpoint, is ℱ +, defined over natural numbers. This can be seen through the following three properties. First, we define the positive and negative supports of a semiflow ∈ ℱ as: and ‖ ‖+ = { ∈ | () > 0} ‖ ‖− = { ∈ | () < 0} , with ‖ ‖ = ‖ ‖− ∪ ‖ ‖+. We can then rewrite Equation (2) as: ⊤ = ⃒⃒⃒⃒ ∑︁ ()()⃒⃒⃒⃒ − ⃒⃒⃒⃒ ∑︁ ()()⃒⃒⃒⃒ = ⊤0.
⃒⃒ ∈‖‖+ ⃒⃒ ⃒⃒ ∈‖‖− ⃒⃒
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 . 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 belongs to N and that a subset of places is bounded.
property 1. For any semiflow ∈ ℱ , ‖ ‖+ is bounded if and only if ‖ ‖− is bounded.
froOmf aconuyrisnei,tiifal‖m ‖a− rki=ng∅),anthdeins so∈meℱti+meancdal‖led‖ciosnnseercveastsiavreilcyo mstpruocnteunrtalalsy ibnou[8n]d.edM(oir.ee.,gbeonuenradlelyd,
considering a weighting function over being defined over non-negative integers and verifying the
following system of inequalities:
⊤ (· , ) ≤ ⊤ (· , ), ∀ ∈ ,
(4)
the following properties can be easily proven [
Moreover, the marking of any place of ‖ ‖ has an upper bound: 0 is such that it verifies Equation (4), then the set of places of ‖ ‖ is structurally () ≤ 0 ()
, ∀ ∈ ( , 0).
If > 0, then ‖ ‖+ = ‖ ‖ = , 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 [
min {∈ℱ+ | ()̸=0} ()
The following corollary can be directly deduced from the fact that any semiflow in ℱ + satisfies the system of inequalities (4); therefore, Property 2 can apply: corollary 1. For any place belonging to at least one support of a semiflow of ℱ +, an upper bound can be defined for the marking of relatively to an initial marking 0 such that: ∀ ∈ ( , 0), () ≤ (, 0) =
min {∈ℱ+ | ()̸=0} ()
We will see with Theorem 5 that this bound is computable as a consequence of Theorems 1 and 3. definition 2. Given a transition and a semiflow in ℱ +, the scalar product (· , ) is called the f-enabling threshold of .
Sometimes, when there is no ambiguity, (· , ) is more simply called the enabling threshold of
as in [
This gives us a second reason for particularly considering a semiflow as being defined over nonnegative integers is that the system of inequalities 0 ≥ (· , ), ∀ ∈ , (5) becomes a necessary condition for any transition to stand a chance to be enabled from any reachable marking from 0, then to be live. Equation (5) motivates the definition 2. property 3. If is a transition and ∈ ℱ + ∖ {0} such that 0 < (· , ), then cannot be executed from ⟨ , 0⟩.
More generally, a necessary condition for a transition to be executed at least once from ⟨ , 0⟩ is with its extremum the inequality of property 3 can rewritten such that: Property 3 is not a suficient condition for a transition to be enabled, see figure 1.
1 ≤
min {∈ℱ+ | ⊤ (· ,)̸=0} ⊤ (· , ) Θ(, 0) = { ∈ Q+ | ∃ ∈ ℱ +, = ⊤ ⊤(0· , ) } 1 ≤ (, 0) = min {∈Θ} We can define Θ stemming from property 3 the same way we defined Λ stemming from property 2:
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
possible is by adding tokens in ‖ ‖ for any semiflow for which inequality (5) is not satisfied. We
conjecture that the notion of siphon [
At last, the following known property ([
If is a non-null integer then ‖ ‖ = ‖ ‖.
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 [
‖ + ‖ = ‖ ‖ ∪
The notion of generating sets for semiflows is well known and eficiently supports the handling of an
important class of invariants. Several results have been published, starting from the initial definition
and structure of semiflows [
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.
definition 3 (Generating set). A subset of ℱ + is a generating set over a set S (where S ∈ {N, Q+, Q} with Q+ denoting the set of non-negative rational numbers) if and only if for all ∈ ℱ +, we have = ∑︀∈ , where ∈ S and ∈ .
Since N ⊂ Q+ ⊂ Q, a generating set over N is also a generating set over Q+, and a generating set
over Q+ is also a generating set over 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 [
Several definitions around the concept of minimal semiflow were introduced in [
A non-null semiflow is minimal with respect to ≤ if and only if
A minimal semiflow cannot be decomposed as the sum of another semiflow and a non-null nonnegative 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 eficiently 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 ℱ +. First, the number of minimal semiflows over N can be quite large. Second, considering a basis over Q is of course relevant to handle ℱ , while less relevant when it is about ℱ +, and may not capture behavioral constraints as easily. We will have to consider Q+.
Generating sets can be characterized thanks to three decomposition theorems. A first version of them
can be found in [
The fact that there exists a finite generating set over 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 [
The question of the existence of a finite generating set being solved for N, is necessarily solved for Q+ and 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 N) A semiflow is minimal if and only if it belongs to all generating sets over N.
The set of minimal semiflows of ℱ + is a finite generating set over N.
Let’s consider a semiflow ∈ ℱ + ∖ {0} and its decomposition over any family of non-null semiflows , 1 ≤ ≤ . Then, there exist 1, ..., ∈ N such that = ∑︀= . Since ̸= 0 and all coeficients =1 are in N, there exists ≤ such that 0 ⪇ ≤ ≤ . If is minimal, then = 1 and = . Hence, if a semiflow is minimal, then it belongs to any generating set over 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, . Since any minimal semiflow is in , the subset of all minimal semiflows is included in and therefore finite. Let ℰ = {1, ...} be this subset and prove by construction that ℰ is a generating set.
For any semiflow ∈ ℱ +, we build the following sequence leading to the decomposition of over ℰ : i) 0 = , ii) = − 1 − such that ∈ ℱ + and − 1 − ( + 1) ∈/ ℱ +.
By construction of the non-negative integers , we have = − ∑︀==1 ∈ ℱ + and ∀ ∈ ℰ , − ∈/ ℱ + therefore, ∀ ∈ ℰ , ∃, () − () < 0; therefore ∄ ∈ ℰ such that ≤ . This means that is either minimal or null. Since ℰ includes all minimal semiflows, therefore = 0, and any semiflow can be decomposed as a linear combinations of minimal semiflows; in other words, ℰ is a ifnite generating set 2.
It is now clear that if a semiflow belongs to any generating set, then it belongs in particular to ℰ ; therefore, is a minimal semiflow. □
Let’s point out that since ℰ is not necessarily a basis, the decomposition is not unique in general and depends on the order in which the minimal semiflows of ℰ are considered to perform the decomposition.
However, a minimal semiflow does not necessarily belong to a generating set over Q+ or Q.
These two theorems can already be found in [
i) there exists a unique minimal semiflow such that = ‖ ‖ and, for all ∈ ℱ + such that ‖‖ = , there exists ∈ N such that = , and
ii) any non-null semiflow such that ‖‖ = constitutes a generating set over Q+ or Q for ℱ+ = { ∈ ℱ + | ‖‖ = }.
In other words, { } is a unique generating set over N for ℱ+ = { ∈ ℱ + | ‖‖ = }. Indeed, this uniqueness property is lost in Q+ or in Q, since any element of ℱ+ is a generating set of ℱ+ over Q+ or Q. 2If ℰ were to be infinite, the construction could still be used, since the monotonically decreasing sequence is bounded by i0naini)d. N is nowhere dense, so we would have l→im∞( − ∑︀==1 ) = 0, with the same definition of the coeficients as theorem 3. (Decomposition over Q+) Any support of semiflows is covered by the finite subset {1, 2, . . . , } of minimal supports of semiflows included in : = ⋃︀= . =1
Moreover, for all ∈ ℱ + such that ‖ ‖ ⊆ , one has = ∑︀==1 , where, for all ∈ {1, 2, ... }, ∈ Q+ and the semiflows are such that ‖‖ = .
A sketch of the proof of Theorem 3 using Property 4 can be found in [
The notion of home space was first defined in [
Home spaces are extremely useful to analyze liveness (see [
Given a Petri Net , its associated set of all potential markings and a subset of , 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 , 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 of , a set HS is an Init-home space if and only if, for all ∈ ( , ), ( , ) ∩ ̸= Ø, in other words, there exists ℎ ∈ HS such that ℎ is reachable from , (i.e. →* ℎ).
This definition is general and can be applied to any Transition System. In [
If is an Init-home state, then it is straightforwardly an {}-home state, and we simply say that is a
home state when there is no ambiguity. This is the usual notation that can be found in [
In many systems, the initial marking 0 represents an idle state from which the various capabilities of the system can be executed. In this case, it is important for 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 such that (, 0) ⊆ Dom() and {0} = Im() (which means that is executable from any reachable marking and that its execution reaches 0). However, by requiring to add too much complexity to (one edge per node), this function is most of the time abstracted away when building up.
It is not always easy to prove that a given set is an Init-home space. This question is addressed in [
It may be worth mentioning the straightforward following properties, given two subsets and of markings. property 5. If is an A-home space, it is a B-home space for any nonempty subset of . If 1 is an 1-home space and 2 is an 2-home space, then 1 ∪ 2 is an (1 ∪ 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. 1, 2 and 3, as defined Figure 2, are three {0}-home spaces. While 1 ∩ 3 = {1, 3} is a {0}-home space, 1 ∩ 2 = {1} is not a {0}-home space (even if it is a {1}-home state).
Given a Petri Net and a subset of markings , a sink is a marking with no successor in the associated reachability graph ( , ). More generally, a subset of markings is a sink in ( , ) if and only if (, ) = . Similarly, we say that strongly connected component of ( , ) is strongly connected component sink if and only if ∄ ∈ (, ) ∖ such that ∃ ∈ and → . As any directed graph, (, ) 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 in (, ) then is a home space. Moreover, a marking is a home state if and only if it belongs to .
Furthermore, any home space has at least one element in each strongly connected component sink of the
reachability graph [
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 paired with a single initial marking 0. Then, three following statements are equivalent: (i) the initial marking 0 is a home state; (ii) every reachable marking is a home state; (iii) the reachability graph is strongly connected.
If 0 is the initial marking, then, for all , ∈ ( , 0), there exists a path from 0 to and a path from 0 to , and since 0 is a home state, there also exists a path from to 0 and from to 0 in the reachability graph. Hence, 0, and 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 ℎ is a home state even if ℎ 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.
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 [
Let Dom(t) denote the subset of markings from which the transition is executable, and Im(t), the subset of markings that can be reached by the execution of . property 8. A transition is live if and only if there exists a home space such that ⊆ 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 ⟨ , 0⟩, a Petri Net with its initial marking 0, its associated reachability set ,
its labeled reachability graph , a home space and = ∩ such that induces (see,
for instance, [
If is a home space, then is also a home space, and for all ∈ , there exist 1 ∈ * and ℎ ∈ such that →1 ℎ.
The subgraph induced by being strongly connected, there exists a path from ℎ to ℎ; in other words, there exists 2 ∈ * such that ℎ →2 ℎ. We can construct a sequence = 12 such that for all ∈ , → . Hence is live in (, 0). The reverse is obvious. □ property 9. Let be a Petri Net and be a home state. Then, any transition that is enabled at is live, and, more generally, a transition is live if and only if it appears as a label in ( , ).
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 be a Petri Net with a home state , and ( , ), the labeled coverability tree of . A transition is live if and only if it appears as a label in ( , ).
This can be proven directly from the fact that a transition appears as a label of an edge of ( , ) if and only if it appears as a label of an edge of ( , ), and by considering Property 9. □ corollary 2. For any Petri Net with a home state , liveness is decidable.
This is a direct consequence of Theorem 4 combined with Karp and Miller’s theorem [
In [
Given an initial state 0, each semiflow can be associated with an invariant that, in turn, can be associated with a home space. In other words, if ∈ ℱ , then (, 0) = { ∈ | ⊤ = ⊤0} is a {0}-home space, since (, 0) ⊆ (, 0). property 10. If ∈ ℱ , then, for all ∈ Q ∖ {0}, (, 0) = (, 0). Also, for all and ∈ ℱ and for all and ∈ Q, (, 0) ∩ (, 0) ⊆ ( + , 0). Moreover, (, 0) ∩ (, 0) is a {0}-home space.
Note that (, 0) ∩ (, 0) is straightforwardly a {0}-home space, since they both contain (, 0)3. If ∈ (, 0) ∩ (, 0), then ( ⊤) = ( ⊤0) and (⊤) = (⊤0), so ( + )⊤ = ( + )⊤0, and, therefore, ∈ ( + , 0) □
We define Ω, the closure under ∩ of { ⊆ | ∃ ∈ ℱ +, = (, 0)}, that is the smallest subset of 2 stable for ∩ containing { ⊆ | ∃ ∈ ℱ +, = (, 0)}. For the same reason as for property 10, all elements of Ω are home spaces and there exists a unique nonempty minimal element = minℎ∈Ω ℎ characterized in the next section. 3Let us recall that, in general, the intersection of home spaces is not a home space (see Figure 2).
Knowledge of any finite generating set allows a practical computation of the three extremums ( , , and ) 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 [
min ⊤0 = {∈ℱ+ | ()̸=0} ()
min {∈ℰ | ()̸=0} () ⊤0 ; (iii) If ℰ is over Q+ or N, then, for any transition belonging to at least one support of a semiflow of ℱ +, for all ∈ ( , 0), we have : (, 0) =
min {∈ℱ+ | ⊤ (· ,)̸=0}} ⊤ (· , ) =
min {∈ℰ | ⊤ (· ,)̸=0}} ⊤ (· , ) .
For the item (i), let’s consider ∈ ℱ + with = ∑︀==1 and ∈ ⋂︀∈ℰ (, 0). Then, (⊤) = (⊤0), for all ∈ {1, ... }, and, hence ∑︀==1 (⊤) = ∑︀==1 (⊤0). Then, for all ∈ ℱ +, ⊤ = ⊤0, and ∈ (, 0). ⋂︀T∈hℰerefo(re,,si0n)ce=ℰ⋂︀⊂∈ℱℱ+ +di(re,ct0ly) =impl.ies (⋂︀∈ℱ+ (, 0)) ⊆ ⋂︀∈ℰ (, 0), we have:
For the item (ii), let’s consider a marking 0, a place , and a semiflow of ℱ + such that () > 0 and = ∑︀==1 , where ≥ 0, for all ∈ {1, ... }.
Let’s define ℰ such that ℰ = min{∈ℰ | ()̸=0} ⊤()0 . Then, there exists such that 1 ≤ ≤ Therefore, for all ≤ such that () ̸= 0, there exists ∈ Q+ such that: ⊤()0 = ⊤0− . It () can then be deduced, for all such that () ̸= 0: and ℰ = ⊤()0 . and, therefore: Since ∑︀{ | ()>0} (⊤0) = ⊤0 − and ∑︀{ | ()>0} () = () ℰ = ⊤0 − ∑︀{|()>0} − () ∑︀{ | ()=0} ⊤0 Then, since ≥ 0 and ≥ 0 for all such that 1 ≤ ≤ , ℰ = (⊤0 − ) ,
() ℰ = ∑︀{ | ()>0} (⊤0 − ) ∑︀{ | ()>0} () ∑︀{ | ()=0} (⊤0) ℰ ≤ ⊤0 () This being verified for any semiflow of ℱ +, we have (, 0) = ℰ .
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 [
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.
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,[
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 to define its Pre and Post functions. This example allows one to detect whether a natural number is a multiple of . 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 by .
The Petri Net () = ⟨{, }, {1, 2}, , ⟩ in Figure 3 is defined by: (· , 1)⊤ = (, 0); (· , 2)⊤ = (1, 1); (· , 1)⊤ = (0, 1); (· , 2)⊤ = ( + 1, 0).
The initial marking 0 is such that 0() = and 0() = , where and ∈ N.
A first version of this example can be found for = 2 in [
⊤ = (1, ) is the minimal semiflow of minimal support, and we can prove that ⟨ (), 0⟩ is not live if and only if ⊤0 ≤ or ⊤0 = × , independently of 0(). In other words, () recognizes whether a given number is a multiple of .
First, if ⊤0 < , then the enabling threshold of 1 can never be reached (Property 3) and neither 1 nor 2 can be executed (since 0() is necessarily null to satisfy the inequality). Second, if ⊤0 ≥ , then we consider the Euclidean division of ⊤0 by , giving ⊤0 = × + , where < . Then, since is a semiflow, ⊤ = () + () ≡ mod , and, therefore, () ≡ mod , for all ∈ ( (), 0). If = 0, then we have () = × − × (), and 1 can always be executed − () times to reach a marking with zero token in .
If ̸= 0 and ⊤0 > , then after executing 1 − () times, we reach a marking with tokens in and at least one token in . Therefore, = { ∈ ( (), 0) | () ̸= 0 ∧ () ̸= 0} is a home space such that ⊆ Dom(2) so, we can apply property 8 proving that 2 is live. It is easy to conclude that the Petri Net () is live if and only if ⊤0 > and is not a multiple of , regardless of the initial marking of . □
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 0() as an a parameter and without considering the values taken by 0()).
From the properties of (), 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 is a multiple of a given natural number , but more generally to recognize the remainder of the Euclidean division of such that > 0 by such that > 1. To this efect, we first consider the Colored Petri Net () of Figure 4, and the parameter ≥ 2. Second, for easing the reasoning, we unfold () into the classic Petri Net (), where each place represents the color of () (see Figures 4 and 5).
We define = {{ | ∈ [0, − 1]}, } and = {,1, ,2| ∈ [0, − 1]}, where Pre and Post are defined by : ( , ,1) = , (, ,1) = ( , ,2) = 1 ( , ,2) = + 1, (, ,1) = 1. where ∈ [0, − 1] . The initial marking is such that 0( ) = + , where ∈ [0, − 1], and 0() = , where > 0 and are natural numbers.
We set = (1, · · · 1, ), such that ( ) = 1 for ∈ [0, − 1], and () = is the minimal semiflow of minimal support in N. We have a first invariant , for all ∈ ( (), 0): ⊤0 = ⊤ = =− 1 ∑︁ 0( ) + 0() = × ( + + − 1 ).
=0 2
Then, we need to notice that any place is connected to only two transitions, ,1 and ,2, such that: ( , ,1) − ( , ,1) = − , ( , ,2) − ( , ,2) = .
Hence, for all ∈ ( (), 0) and ∈ [0, − 1], ( ) can only vary by ± . We then deduce a family of invariants () for ∈ [0, − 1]: () : ∀ ∈ ( (), 0), ( ) ≡ 0( ) mod .
Let’s perform the Euclidean division of 0( ) by . We have: 0( ) = + = × + , where < for all ∈ [0, − 1]. A new family of invariants ′() can be directly deduced from each (): ′() : ∀ ∈ ( (), 0), ( ) ≥ .
Furthermore, it must be pointed out that { 0, · · · − 1} is a permutation of {0, · · · − 1}. Indeed, if there exist < and ′ < such that = ′ , then + − × = + ′ − ′ × , and | − ′| = | − ′ | × . Since | − ′| < , we have = ′ and = ′. Therefore, (a) ∑︀==0− 1 ( ) ≥ (−2 1) (directly from the ′() family of invariants), and (b) there is a unique ∈ [0, − 1] such that = 0.
From (a) and , we deduce, for all ∈ ( (), 0), () ≤ + (which is a better bound than the one that can be deduced from Proposition 2). Also, from (), we can deduce, ∀ ∈ ( (), 0), ( ) = × + , where ∈ N.
From any reachable marking , the sequence = 00,1 · · · −− 11,1 can be executed and reach the marking ℎ such that, for all ∈ [0, − 1] , ℎ( ) = and ℎ() = + .
We know ℎ is a home state, since is defined for any reachable marking (Note that 0 is not a home state). From Property 9, we deduce that, since any transition ,2 where ̸= is executable ( > 0 hence, ℎ() > 1 and ℎ( ) = > 0), then ,2 is live, and, therefore, the corresponding transitions ,1 are also live.
From (b), ℎ() = 0 from, which we deduce that ,1 and ,2 are not live4. Finally, we have + = × , and the remainder of the Euclidean division of by is − .
() provides the ability to recognize this remainder by the remarkable fact that (,1, ,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 0 of a Petri Net is not a home state and there exists a home state in ( , 0), then there exists at least one non-live transition in ⟨ , 0⟩."
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 ℱ + 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 [
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
[
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.
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.