Symbolic Supervisory Control of Timed Discrete Event Systems

We symbolically compute a nonblocking, controllable, and minimally restrictive supervisor for timed discrete event systems (TDESs), in the supervisory control theory context. We model TDES based on timed extended finite automata (TEFAs): an augmentation of extended finite automata (EFAs) by incorporating discrete time into the model. EFAs are ordinary automata extended with discrete variables, where conditional expressions and update functions can be attached to the transitions. The controllability is defined based on the corresponding tick models of the TEFAs. A tick can be considered as an event that is generated by a global digital clock. The tick models suffer from a major problem: the state size is very sensitive to the clock frequency. We show how a controllable supervisor, equivalent to the one computed based on the tick models, can be obtained by eliminating the tick events. To tackle large problems, all computations are conducted symbolically using binary decision diagrams (BDDs). We show that, based on the proposed approach, a fixed point is reached earlier in the reachability analysis and that the size of the intermediate BDDs usually becomes smaller. The framework has been applied to a real industrial application and several benchmarks.