Symbolic representation and computation of timed discrete event systems

In this paper, we symbolically represent timed discrete event systems (TDES), which can be used to efficiently compute the supervisor in the supervisory control theory context. We model a TDES based on \emph{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. To tackle large problems all computations are conducted symbolically using binary decision diagrams (BDDs). We show how TEFAs can be represented by BDDs. The main feature of this approach is that the BDD-based fixed point computations is not based on $\mathit{tick}$ models that have been commonly used in this area, leading to better performance in many cases. In a case study, we efficiently computed the supervisor of a well-known production cell