Semiflows, Home Spaces, and Home States, Applications to the Analysis of Parameterized Petri Nets
Gerard Memmi
TL;DR
The paper develops a formal framework that uses semiflows and home spaces to analyze parameterized Petri nets, focusing on invariants, boundedness, and liveness. It defines the sets of semiflows $\mathcal{F}$ and $\mathcal{F}^+$, introduces generating sets and three decomposition theorems, and shows how to compute key extremal bounds $\lambda(p,q_0)$, $\theta(t,q_0)$, and $\omega(q_0)$ from finite generating sets. A new result establishes the decidability of liveness for nets with a home state, leveraging the finite coverability tree construction of Karp and Miller. The framework is demonstrated on parameterized nets modeling arithmetic operations (e.g., Euclidean division), illustrating how semiflow- and home-space analysis can guide parameter synthesis and prove liveness more efficiently than exhaustive symbolic methods.
Abstract
After rapidly recalling basic notations relatively to semiflows and Petri nets, we define F, the set of semiflows over Z that we associate with a specific class of invariants. We then focus on F+, the set of semiflows with non-negative coordinates which are important to study the behavior of a Petri net. We recall known behavioral properties attached to semiflows in F+ that we associate with two sets of bounds regarding boundedness then liveness. We recall the notions of home states and home spaces for which we regrouped old and new properties. We introduce a new result on the decidability of liveness under the existence of a home state. The notions of minimality of semiflows and minimality of supports allow us to define generating sets that are particularly critical to develop an effective analysis of invariants and behavioral properties of Petri nets such as boundedness or even liveness. We also recall three known decomposition theorems considering N, Q+, and Q respectively where the decomposition over N is being improved with a necessary and sufficient condition. We use the notion the notion of generating sets to show that extremums linked to the set of bounds mentioned here above, are indeed computable by providing their values. Two related Petri net modeling arithmetic operations (one of which represents an Euclidean division) illustrate how results on semiflows and home spaces can be methodically used in efficiently analyzing the liveness of the parameterized model and underlining the efficiency brought by the combination of these results.