Efficient analysis of weighted Petri nets

In this talk, I present new results for the efficient analysis of three behavioral properties of weighted Petri nets: liveness, (non-)deadlockability and reversibility.

This work will appear in Fundamenta Informaticae as an extended version of Petri nets 2017.

Liveness preserves the possibility to fire any transition after a finite number of other firings, non-deadlockability, also known as deadlock-freeness, is weaker than liveness and states the absence of reachable deadlocks i.e. markings that enable no transition,
and reversibility ensures that the initial marking can be reached from any reachable marking, inducing the strong connectedness of the reachability graph.

They are often studied together with boundedness, which designates the finiteness of the reachability graph.

These behavioral properties are fundamental for many real-world applications, such as embedded systems, and are often required to be monotonic, meaning preserved upon any increase of the marking considered. However, their checking is intractable in the general case and their monotonicity is not always satisfied.So as to simplify the analysis of these features, structural approaches have been previously exploited in particular subclasses of Petri nets, deducing the behavior from the underlying graph and the initial marking only, often in polynomial time.

In this work, such structural conditions are further developed to analyze (non-)deadlockability, liveness, reversibility and their monotonicity in larger subclasses of weighted Petri nets. Some of these new checking methods are the first ones to operate in polynomial time. This study also delineates more sharply the structural frontier between monotonicity and non-monotonicity for the three behavioral properties.