A Determinizable Class of Timed Automata

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 ( nite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the languageinclusion 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 speci cation language for real-time properties. We provide an algorithm for checking if a timed automaton ...

• Type: Conference
• Year: 1994
• Where: CAV
• Authors: Rajeev Alur, Limor Fix, Thomas A. Henzinger
• Keywords: CAV 1994, Event-recording Automata, Hardware, Timed Automaton, Transition Systems