Analysis of Behavioural Properties of Bounded Petri Nets with a Semi-Structural Approach

In this paper, we propose a semi-structural approach to verify some behavioural properties of bounded Petri nets, including home state existence, reversibility, liveness, and deadlock-freeness. An abstracted representation of the state space of Petri nets, called minimax basis reachability graph (minimax-BRG), is employed. We show how the verification of the above-mentioned properties for a bounded Petri net can be carried out testing equivalent properties of its corresponding minimax-BRG. Being the minimax-BRGs an abstracted representation of the reachability graph, the exhaustive enumeration of the state space can be avoided and we show, via numerical simulations, that this approach achieves significant practical efficiency.