Nonblocking Supervisory Control Synthesis of Timed Automata using Abstractions and Forcible Events

Conventional supervisory control synthesis techniques are not adequate for timed automata (TA) due to their infinite state space. This paper presents a supervisory control synthesis technique for TA with the objective of satisfying controllability and nonblockingness. The synthesis method consists of three steps. First, a TA is abstracted to a finite automaton (FA). The event set of the FA includes the discrete events of the TA as well as an event representing the passage of a significant amount of time. Time passage is considered to be preemptable by events from a given set of forcible events. Second, an algorithm is presented to synthesize a controllable and nonblocking supervisor for the FA. Finally, a time-refinement technique is proposed to convert the supervisor to a TA