SUPERVISOR SYNTHESIS FOR REAL-TIME DISCRETE-EVENT SYSTEMS

This paper introduces a formal framework to logically analyze and cont rol real-time discrete event systems (RTDESs). Time Petri nets are ext ended to controlled rime Petri nets (CtlTPNs) to model the dynamics of RTDESs that can be controlled by real-rime supervisors. The logical b ehaviors of CtlTPNs are represented by control class graphs (CCGs) whi ch are untimed automata with timing and control information in their s tate transition labels. We prove that the CCG corresponding to a CtlTP N expresses completely the logical behavior of the CtlTPN. The real-ti me supervisor is based on a nondeterministic logical supervisor for th e CCG, including the delay for control computations to ensure the supe rvisor is acceptable in a true real-time environment. We prove the exi stence of a unique maximal controllable sublanguage of a given specifi cation language and present an algorithm to construct the sublanguage. We also prove that the real-time supervisor meets the prespecified re al-time behavior and present an online control algorithm to implement real-time supervisors. The concepts and algorithms are illustrated for an example of packet reception processes in a communication network.