Home Spaces and Semiflows for the Analysis of Parameterized Petri Nets

After briefly recalling basic notations of Petri Nets, home spaces, and semiflows, we focus on ℱ⁺, the set of semiflows with non-negative coordinates where the notions of minimality of semiflows and minimality of supports are particularly critical to develop an effective analysis of invariants and behavioral properties of Petri Nets such as boundedness or even liveness. We recall known behavioral properties attached to the notion of semiflows that we associate with extremums. We also recall three known decomposition theorems considering ℕ, ℚ⁺, and ℚ respectively where the decomposition over ℕ is being improved with a necessary and sufficient condition. Then, we regroup a number of properties (old and new) especially around the notions of home spaces and home states which, in combination with semiflows, are used to efficiently support the analysis of behavioral properties. We introduce a new result on the decidability of liveness under the existence of a home state. We introduce new results on the structure and behavioral properties of Petri Nets, illustrating again the importance of considering generating sets of semiflows with non-negative coordinates. As examples, we present two related Petri Net modeling arithmetic operations (one of which represents an Euclidean division), illustrating how results on semiflows and home spaces can be methodically used in analyzing the liveness of the parameterized model and underlining the efficiency brought by the combination of these results to the verification engineer.