Unbounded product-form Petri nets

TL;DR

This paper introduces open { extPi}3-nets, a class of infinite-state Petri nets, and demonstrates that key properties like liveness, reachability, and ergodicity can be decided efficiently, along with a method to compute steady-state distributions.

Contribution

It generalizes closed { extPi}3-nets to open nets, enabling analysis of infinite-state systems with polynomial-time decision algorithms and a pseudo-polynomial time method for steady-state normalization.

Findings

Liveness can be decided in polynomial time.

Reachability in live { extPi}3-nets is decidable in polynomial time.

Ergodicity can be decided in polynomial time.

Abstract

Computing steady-state distributions in infinite-state stochastic systems is in general a very dificult task. Product-form Petri nets are those Petri nets for which the steady-state distribution can be described as a natural product corresponding, up to a normalising constant, to an exponentiation of the markings. However, even though some classes of nets are known to have a product-form distribution, computing the normalising constant can be hard. The class of (closed) {\Pi}3-nets has been proposed in an earlier work, for which it is shown that one can compute the steady-state distribution efficiently. However these nets are bounded. In this paper, we generalise queuing Markovian networks and closed {\Pi}3-nets to obtain the class of open {\Pi}3-nets, that generate infinite-state systems. We show interesting properties of these nets: (1) we prove that liveness can be decided in polynomial time, and that reachability in live {\Pi}3-nets can be decided in polynomial time; (2) we show that we can decide ergodicity of such nets in polynomial time as well; (3) we provide a pseudo-polynomial time algorithm to compute the normalising constant.