Event-clock automata: a determinizable class of timed automata. (English) Zbl 0912.68132

Summary: 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.


68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata


Kronos; Uppaal
Full Text: DOI


[1] Alur, R.; Courcoubetis, C.; Dill, D., Model checking in dense real time, Inform. and comput., 104, 2-34, (1993) · Zbl 0783.68076
[2] Alur, R.; Courcoubetis, C.; Henzinger, T., Computing accumulated delays in real-time systems, (), 181-193
[3] Alur, R.; Dill, D., A theory of timed automata, Theoret. comput. sci., 126, 183-235, (1994) · Zbl 0803.68071
[4] Alur, R.; Feder, T.; Henzinger, T., The benefits of relaxing punctuality, J. ACM, 43, 116-146, (1996) · Zbl 0882.68021
[5] Alur, R.; Henzinger, T., Back to the future: towards a theory of timed regular languages, (), 177-186 · Zbl 0977.68548
[6] Alur, R.; Itai, A.; Kurshan, R.; Yannakakis, M., Timing verification by successive approximation, Inform. and comput., 118, 1, 142-157, (1995) · Zbl 0939.68705
[7] Alur, R.; Kurshan, R., Timing analysis in C{\scospan}, (), 220-231
[8] Bengtsson, J.; Larsen, K.; Larsson, F.; Pettersson, P.; Yi, W., UPPAAL: a tool suite for automatic verification of real-time systems, (), 232-243
[9] Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, (), 399-409
[10] Daws, C.; Olivero, A.; Tripakis, S.; Yovine, S., The tool K{\scronos}, (), 208-219
[11] Dill, D., Timing assumptions and verification of finite-state concurrent systems, (), 197-212
[12] Henzinger, T.; Manna, Z.; Pnueli, A., Temporal proof methodologies for timed transition systems, Inform. and comput., 112, 273-337, (1994) · Zbl 0820.68085
[13] Henzinger, T.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model checking for real-time systems, Inform. and comput., 111, 193-244, (1994) · Zbl 0806.68080
[14] Hopcroft, J.; Ullman, J., Introduction to automata theory, languages, and computation, (1979), Addison-Wesley Reading, MA · Zbl 0426.68001
[15] Kurshan, R., Computer-aided verification: the automata-theoretic approach, (1994), Princeton University Press Princeton, NJ
[16] Lynch, N.; Attiya, H., Using mappings to prove timing properties, Distrib. comput., 6, 121-139, (1992) · Zbl 0773.68054
[17] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems, (1991), Springer Berlin · Zbl 0753.68003
[18] Merritt, M.; Modugno, F.; Tuttle, M., Time-constrained automata, (), 408-423
[19] Schneider, F.; Bloom, B.; Marzullo, K., Putting time into proof outlines, (), 618-639
[20] Sistla, A.; Vardi, M.; Wolper, P., The complementation problem for Büchi automata with applications to temporal logic, Theoret. comput. sci., 49, 217-237, (1987) · Zbl 0613.03015
[21] Wolper, P.; Vardi, M.; Sistla, A., Reasoning about infinite computation paths, (), 185-194
[22] Yannakakis, M.; Lee, D., An efficient algorithm for minimizing real-time transition systems, (), 210-224
[23] Yoneda, T.; Shibayam, A.; Shlingloff, B.; Clarke, E., Efficient verification of parallel real-time systems, (), 321-332
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.