19 mars 2018Thomas Hujsa (Onera)
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.
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.