## Event-Clock Automata: A Determinizable Class of Timed Automata

*Rajeev Alur, Limor Fix, and
Thomas A. Henzinger*
We introduce *event-recording automata*.
An event-recording automaton is a timed automaton that contains, for every
event *a*, a clock that records the time of the last occurrence of
*a*.
The class of event-recording automata is, on one hand, expressive enough to
model (finite) timed transition systems and, on the other hand,
determinizable and closed under all boolean operations.
As a result, the language-inclusion problem is decidable for event-recording
automata.
We present a translation from timed transition systems to event-recording
automata, which leads to an algorithm for checking if two timed transition
systems have the same set of timed behaviors.

We also consider *event-predicting automata*, which contain clocks that
predict the time of the next occurrence of an event.
The class of *event-clock automata*, which contain both event-recording
and event-predicting clocks, is a suitable specification language for
real-time properties.
We provide an algorithm for checking if a timed automaton meets a
specification that is given as an event-clock automaton.

*Proceedings of the
Sixth International Conference on Computer-aided Verification*
(CAV 1994),
Lecture Notes in Computer Science 818,
Springer-Verlag, 1994, pp. 1-13.
To appear in * Theoretical Computer Science*.