Petri net control of systems under discrete-event supervision

Synthesis and verification of discrete control logic by a combined application of automata based supervisory control theory and Petri nets is addressed. While supervisory control theory is well suited to specification and design of the interlock part of the control logic, the sequencing part can be more easily described by Petri net models. The basic idea presented in the paper is to design basic interlock logic by the use of supervisory control theory and then to use the derived model of admissible behaviour as a process model. The sequencing part is designed in a form of a Petri net model which is verified against the process model. The basic property of interest is the absence of blocking. To study the interaction of the two models we use an extension of Place/Transition nets which includes external inputs and outputs, i.e., the Real-time Petri nets (RTPN). In order to verify the nonblocking of the controller a new kind of reachability analysis is proposed, which considers all possible changes of the controller input and output signals.