A THEORY OF TIMED AUTOMATA

We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed wor ds - infinite sequences in which a real-valued time of occurrence is a ssociated with each symbol. We study timed automata from the perspecti ve of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deter ministic transition structures, and both Buchi and Muller acceptance c onditions. We show that nondeterministic timed automata are closed und er union and intersection, but not under complementation, whereas dete rministic timed Muller automata are closed under all Boolean operation s. The main construction of the paper is an (PSPACE) algorithm for che cking the emptiness of the language of a (nondeterministic) timed auto maton. We also prove that the universality problem and the language in clusion problem are solvable only for the deterministic automata: both problems are undecidable (PI1(1)-hard) in the nondeterministic case a nd PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requ irements of finite-state systems.