## 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.

*Theoretical Computer Science* 211:253-273, 1999.
A preliminary version appeared in the
*Proceedings of the
Sixth International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 818,
Springer, 1994, pp. 1-13.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1994 Springer,
1999 Elsevier.