A Language-Theoretic Classification of Discrete-Time Discrete Event Systems

There exists extensive research on formal verification methods for timed discrete event systems. These formalisms are usually considered in the dense (or continuous) time model. Dense time semantics allow accurate modeling of real-world systems, but often lead to undecidability results for many verification problems, even if heavily restricted subclasses are considered. To overcome these limitations, timed behavior is often approximated using the discrete time model where time progresses only in discrete steps. However, these works almost exclusively consider single classes like timed automata or time Petri nets and rarely study how these classes relate. While the relationships between timed discrete event systems are well understood in the dense time model, there exist almost no results for the discrete time model. In this paper, we aim to close this gap. We develop a language-theoretic classification of several classes of discrete-time discrete event systems (DTDES). We consider timed automata, time Petri nets, constant-time automata, and tick automata, all with discrete time semantics. We study each class with multiple semantic extensions like silent transitions, periodic time constraints, and arbitrary clock updates. We classify these formalisms by their expressiveness, provide, where possible, transformations between different classes of DTDES, and analyze their worst-case complexity. Our classification unifies DTDES in terms of expressiveness and thus provides insights into generalizing verification methods from one class to others by means of reduction.