Liveness and deadlock-freeness verification and enforcement in bounded Petri nets using basis reachability graphs.

This paper studies the verification and enforcement of deadlock-freeness and liveness in partially controllable Petri nets. First, we introduce a particular type of basis reachability graphs called conflict-free-control-explicit basis reachability graphs (CFCE-BRGs), in which the firings of all structurally conflicting transitions and all controllable ones are explicitly encoded. We propose two sufficient and necessary conditions for verifying deadlock-freeness and liveness of a Petri net; both can be verified by inspecting a CFCE-BRG using graph theory. Moreover, we develop two maximally permissive deadlock-freeness and liveness enforcing supervisors based on the trimming of CFCE-BRGs. The developed approaches are applicable to arbitrary bounded Petri nets, without an exhaustive reachability space enumeration. [ABSTRACT FROM AUTHOR]