Semiflows, Home Spaces, and Home States, Applications to the Analysis of Parameterized Petri Nets

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.