Behavioral Property Analysis And Supervisory Control Of Petri Nets Using Semi-Structural Approaches

With decades of industrial informatization and intelligent transformation development,the modeling,analysis and control of complex and large-scale systems have penetrated into all aspects of manufacturing,including production control,remote services,assembly testing,maintenance,after-sales operation,and so on.As a fundamental concept in system theory,the behavior of a system characterizes,under different input conditions,how the state variables respond to the input values changing with time or events.In an engineering context,the first step is to model a given real-world system with mathematical tools for simulating and reproducing the operating process.Then,the behavioral properties of the system should be analyzed qualitatively or quantitatively.Finally,for systems that do not achieve the desired behavioral properties,the considered and proper input values/conditions should be further adjusted,also known as,to control the system.Discrete-event systems(DESs)are event-driven systems whose state space is a discrete set.A suite of real-world systems with engineering backgrounds can be naturally modelled using DESs,e.g.,manufacturing,queueing,and communication systems.DESs have some meaningful behavioral properties,e.g.,reachability(whether a given state can be reached from the initial state of the system through a sequence of events),non-blockingness(all states can access a set of given final states in the system),liveness(at any state,any event of the system can eventually occur as the system evolves),deadlock-freeness(at any state,at least an event of the system can occur),and so on.On the one hand,plenty of behavior properties in DESs also relate to the corresponding physical properties that are far-reaching in real-world systems;ergo,efficient techniques for verifying them-especially on large scale systems-are demanded.In general,the verification methods that base on a state-space enumeration or reachability graph construction are inevitably restricted by the state explosion problem.Therefore,researchers are devoted to finding other structural or semi-structural-based countermeasures that achieve practical efficiency.On the other hand,in order to ensure that the un-controlled DES achieves desired behavior properties,proper control policies need to be designed so that the controlled closedloop systems meet expectations.Practically,not all events in a given DES are controllable due to factors such as sensor shortage or technical limitations.Therefore,it is a tricky but worth-investigating task to design a supervisor(i.e.,an online control agent)with both good efficiency(i.e.,can be designed in a reasonable time)and permissiveness(i.e.,allow the occurrence of as many states as possible).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 structure,namely basis reachability graph(BRG),is constructed that abstracted the reachability 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 non-blockingness,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 estimation and supervisory control problems,in which behavior(e.g.,non-blockingness,deadlock-freeness,or liveness)analysis plays a key role.This motivated us to develop 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: conflictincrease 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-freecontrol-explicit BRG(CFCE-BRG).By marrying the BRG-based technique and the classical theory of supervisory control,we design two deadlock-freeness and livenessenforcing 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.