Behavioral Property Analysis and Supervisory Control of Petri Nets Using Semi-Structural Approaches

This dissertation is dedicated to the behavioral property verification and supervisory control problems in Petri nets using semi-structural approaches. The main results are abstracted as follows. 1. As an efficient abstraction-based technique, the basis marking approach has been widely adopted in solving various Petri-net-based problems, in which a compact struc-ture, namely basis reachability graph (BRG), is constructed that abstracted the reach-ability information of the Petri net. However, in general, not all information regarding the behaviors of a Petri net can be encoded in the corresponding BRG; thus, the conventional BRG-based method may not be applied for behavior verification. In this dissertation, a semi-structural technique on verifying behavioral properties of a Petri net, including nonblockingness, reversibility, deadlock-freeness, liveness, and home state existence, is proposed. In this technique, we construct a structure called a minimal-maximal basis reachability graph (min-max-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking, reversible, deadlock-free, live, and contains home state. We show that the above-mentioned property-verification problems of a Petri net can all be carried out by testing equivalent properties of its corresponding min-max-BRG. The developed approach does not require the construction of the reachability graph and has wide applicability. 2. Although the min-max-BRG exhibits practical efficiency in solving the behavioral property verification problem, unlike the basis-marking-based approach, currently, there are no analysis methods for addressing with min-max-BRGs on state estima-tion and supervisory control problems, in which behavior (e.g., non-blockingness, deadlock-freeness, or liveness) analysis plays a key role. This motivated us to devel-op an alternative non-blockingness/deadlock-freeness/liveness verification method in Petri nets by fully tapping into the power of the conventional types of BRGs whose analysis methods are relatively mature. In this dissertation, by selecting the considered transition partitioning of a Petri net, we propose two subclasses of BRGs: conflict-increase BRGs (CI-BRGs) and conflict-free BRGs (CF-BRGs). By employing graph theory, the former can be specifically tailored for non-blockingness verification, while the latter can be used for verifying deadlock-freeness and liveness. Thanks to the compactness of the BRG, the developed approaches possess practical efficiency since the exhaustive enumeration of the state space can be avoided. 3. For partially controllable Petri nets, the deadlock-freeness and liveness enforcement problems are investigated. Most of the solutions in the literature require enumerating the reachability set a priori, thus suffering from the state explosion problem. Other approaches that avoid enumeration are either only applicable to subclasses of Petri nets (highly dependent on some particular Petri net structures) or in general not maximally permissive. This dissertation proposes a subclass of CF-BRG, namely conflict-free-control-explicit BRG (CFCE-BRG). By marrying the BRG-based technique and the classical theory of supervisory control, we design two deadlock-freeness and liveness-enforcing supervisors that are maximally permissive. The supervisors we developed are both characterized as corresponding CFCE-BRG-derived automata. Compared to other techniques in the literature, our method is applicable to arbitrarily bounded Petri nets without an exhaustive reachability space enumeration, thus alleviating the state explosion problem.