Structural characterization and qualitative properties of Product Form Stochastic Petri Nets

The model of Stochastic Petri nets (SPN) with a product form solution (Π-net) is a class ofnets for which there is an analytic expression ofthe steady state probabilities w.r.t. markings, as for product form queueing networks w.r.t. queue lengths. In this paper, we prove new important properties of this kind of nets. First we provide a polynomial time (w.r.t. the size ofthe net structure) algorithm to check whether a SPN is a Π-net. Then, we give a purely structural characterization of SPN for which a product form solution exists regardless the particular values ofprobabilistic parameters ofthe SPN. We call such nets Π-bar nets. We also present untimed properties of Π-nets and Π-bar nets such like liveness, reachability, deadlock freeness and characterization of reachable markings. The complexity ofthe reachability and the liveness problems is also addressed for Π-nets and Π-bar nets nets. These results complement previous studies on these classes ofnets and improve the applicability of Product Form solutions.