Abstract
We introduce the class of event- recording timed automata (ERA). An event-recording automaton contains, for every event a, a clock that records the time of the last occurrence of a. The class ERA 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 timed automata (EPA), which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata (ECA), 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.
Supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under grant CCR-8701103, and by DARPA/NSF under grant CCR-9014363.
Supported in part by the National Science Foundation under grant CCR-9200794 and by the United States Air Force Office of Scientific Research under contract F49620-93-1-0056.
Chapter PDF
Similar content being viewed by others
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104:2–34, 1993.
R. Alur, C. Courcoubetis, and T. Henzinger. Computing accumulated delays in real-time systems. In Proceedings of the Fifth Conference on Computer-Aided Verification, Lecture Notes in Computer Science 697, pages 181–193. Springer-Verlag, 1993.
R. Alur and D. Dill. Automata for modeling real-time systems. In Proceedings of the 17th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 443, pages 322–335. Springer-Verlag, 1990.
R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 139–152, 1991.
R. Alur and T. Henzinger. Back to the future: Towards a theory of timed regular languages. In Proceedings of the 33rd IEEE Symposium on Foundations of Computer Science, pages 177–186, 1992.
C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. In Proceedings of the Third Workshop on Computer-Aided Verification, Lecture Notes in Computer Science 575, pages 399–409, 1991.
T. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for realtime systems. In Proceedings of the 18th ACM Symposium on Principles of Programming Languages, pages 353–366, 1991.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. In Proceedings of the Seventh IEEE Symposium on Logic in Computer Science, pages 394–406, 1992.
J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.
R. Kurshan. Reducibility in analysis of coordination. In Lecture Notes in Computer Science, volume 103, pages 19–39. Springer-Verlag, 1987.
N. Lynch and H. Attiya. Using mappings to prove timing properties. Distributed Computing, 6:121–139, 1992.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991.
M. Merritt, F. Modugno, and M. Tuttle. Time-constrained automata. In Proceedings of the Workshop on Theories of Concurrency, Lecture Notes in Computer Science 527, pages 408–423. Springer-Verlag, 1991.
F. Schneider, B. Bloom, and K. Marzullo. Putting time into proof outlines. In Real-Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 618–639. Springer-Verlag, 1991.
A. Sistla, M. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49:217–237, 1987.
P. Wolper, M. Vardi, and A. Sistla. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, pages 185–194, 1983.
T. Yoneda, A. Shibayam, B. Schlingloff, and E. Clarke. Efficient verification of parallel real-time systems. In Proceedings of the Fifth Conference on Computer-Aided Verification, Lecture Notes in Computer Science 697, pages 321–332. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Fix, L., Henzinger, T.A. (1994). A determinizable class of timed automata. In: Dill, D.L. (eds) Computer Aided Verification. CAV 1994. Lecture Notes in Computer Science, vol 818. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58179-0_39
Download citation
DOI: https://doi.org/10.1007/3-540-58179-0_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58179-6
Online ISBN: 978-3-540-48469-1
eBook Packages: Springer Book Archive