Liveness-enforcing supervision of bounded ordinary Petri nets using partial order methods

This paper combines and refines recent results into a systematic way to verify and enforce the liveness of bounded ordinary Petri nets. The approach we propose is based on a partial-order method called network unfolding. Network unfolding maps the original Petri net to an acyclic occurrence net. A finite prefix of the occurrence net is defined to give a compact representation of the original net reachability graph while preserving the causality between net transitions. A set of transition invariants denoted as base configurations is identified in the finite prefix. These base configurations capture all of the fundamental executions of the net system, thereby providing a modular way to verify and synthesize supervisory net systems. This paper proves necessary and sufficient conditions that characterize the original net liveness and the existence of maximally permissive supervisory policies that enforce liveness