Abstract
Model checking is emerging as a practical tool for automated debugging of complex reactive systems such as embedded controllers and network protocols (see [23] for a survey). Traditional techniques for model checking do not admit an explicit modeling of time, and are thus, unsuitable for analysis of real-time systems whose correctness depends on relative magnitudes of different delays. Consequently, timed automata [7] were introduced as a formal notation to model the behavior of real-time systems. Its definition provides a simple way to annotate state-transition graphs with timing constraints using finitely many real-valued clock variables. Automated analysis of timed automata relies on the construction of a finite quotient of the infinite space of clock valuations. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theory of timed automata, and their role in specification and verification of real-time systems.
Chapter PDF
Similar content being viewed by others
References
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In Real-Time: Theory in Practice, REX Workshop, LNCS 600, pages 1–27. Springer-Verlag, 1991.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for probabilistic real-time systems. In Automata, Languages and Programming: Proc. of 18th ICALP, LNCS 510, pages 115–136, 1991.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, 1993.
R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems. In CONCUR’ 92, LNCS 630, pages 340–354, 1992.
R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
R. Alur, C. Courcoubetis, and T. Henzinger. The observational power of clocks. In CONCUR’ 94: Fifth Conference on Concurrency Theory, LNCS 836, pages 162–177, 1994.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.
R. Alur, L. Fix, and T. Henzinger. Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science, 211:253–273, 1999.
R. Alur and T. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181–204, 1994.
R. Alur and T. Henzinger. Modularity for timed and hybrid systems. In CONCUR’ 97: Eighth Conference on Concurrency Theory, LNCS 1243, pages 74–88, 1997.
R. Alur, T. Henzinger, and P.-H. Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181–201, 1996.
R. Alur, A. Itai, R. Kurshan, and M. Yannakakis. Timing verification by successive approximation. Information and Computation, 118(1):142–157, 1995.
R. Alur, L. Jagadeesan, J. Kott, and J. V. Olnhausen. Model-checking of real-time systems: a telecommunications application. In Proc. of Intl. Conf. on Software Engineering, 1997.
R. Alur and R. Kurshan. Timing analysis in COSPAN. In Hybrid Systems III: Control and Verification, LNCS 1066, pages 220–231. Springer-Verlag, 1996.
R. Alur, R. Kurshan, and M. Viswanathan. Membership problems for timed and hybrid automata. In Proceedings of the 19th IEEE Real-Time Systems Symposium. 1998.
E. Asarin, O. Maler, and P. Caspi. A Kleene theorem for timed automata. In Proceedings of the 12th IEEE Symposium on Logic in Computer Science, pages 160–171, 1997.
G. Behrmann, K. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. In Computer Aided Verification, 1999.
S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. In Compositionality-the significant difference, LNCS. Springer-Verlag, 1998.
M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In Computer Aided Verification, LNCS 1254, pages 179–190. 1997.
S. Campos and E. Clarke. Real-time symbolic model checking for discrete time models. In Theories and experiences for real-time system development, AMAST series in computing, 1994.
E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. Workshop on Logic of Programs, LNCS 131, pages 52–71, 1981.
E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6):61–67, 1996.
C. Courcoubetis and M. Yannakakis. Minimum and maximum delay problems in real-time systems. In Third Workshop on Computer-Aided Verification, LNCS 575, pages 399–409, 1991.
C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool kronos. In Hybrid Systems III: Verification and Control, LNCS 1066, pages 208–219. Springer-Verlag, 1996.
L. de Alfaro. Formal verification of probabilistic systems. PhD thesis, Stanford University, 1997.
D. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, LNCS 407, pages 197–212, 1989.
E. Emerson, A. Mok, A. Sistla, and J. Srinivasan. Quantitative temporal reasoning. In Computer-Aided Verification, 2nd International Conference, LNCS 531, pages 136–145, 1990.
R. Gawlick, R. Segala, J. Sogaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. In Proc. ICALP’94, LNCS 820, pages 166–177, 1994.
T. Henzinger. The theory of hybrid automata. In Proceedings of the 11th IEEE Symposium on Logic in Computer Science, pages 278–293, 1996.
T. Henzinger. It’s about time: Real-time logics reviewed. In CONCUR’ 98: Ninth International Conference on Concurrency Theory, LNCS 1466, pages 439–454. 1998.
T. Henzinger, P. Ho, and H. Wong-Toi. HyTech: the next generation. In TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, pages 41–71, 1995.
T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata. In Proceedings of the 27th ACM Symposium on Theory of Computing, pages 373–382, 1995.
T. Henzinger, Z. Manna, and A. Pnueli. What good are digital clocks? In ICALP 92: Automata, Languages, and Programming, LNCS 623, pages 545–558. Springer-Verlag, 1992.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
T. Henzinger, J. Raskin, and P. Schobbens. The regular real-time languages. In ICALP 98: Automata, Languages, and Programming, LNCS 1443, pages 580–593. 1997.
I. Kang and I. Lee. State minimization for concurrent system analysis based on state space exploration. In Proceedings of the Conference On Computer Assurance, pages 123–134, 1994.
R. Koymans. Specifying real-time properties with metric temporal logic. Journal of Real-Time Systems, 2:255–299, 1990.
R. Kurshan. Computer-aided Verification of Coordinating Processes: the automatatheoretic approach. Princeton University Press, 1994.
K. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1, 1997.
K. Larsen, B. Steffen, and C. Weise. Continuous modeling of real-time and hybrid systems: from concepts to tools. Software Tools for Technology Transfer, 1(2):64–85, 1997.
K. Larsen and Y. Wang. Time abstracted bisimulation: Implicit specifications and decidability. In Proceedings of Mathematical Foundations of Programming Semantics, 1993.
N. Lynch. Distributed algorithms. Morgan Kaufmann, 1996.
M. Merritt, F. Modugno, and M. Tuttle. Time constrained automata. In Proceedings of Workshop on Theories of Concurrency, 1991.
J. Ostroff. Temporal Logic of Real-time Systems. Research Studies Press, 1990.
A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–77, 1977.
J. Queille and J. Sifakis. Specification and verification of concurrent programs in CESAR. In Proceedings of the Fifth Symposium on Programming, LNCS 137, pages 195–220, 1982.
S. Tasiran, R. Alur, R. Kurshan, and R. Brayton. Verifying abstractions of timed systems. In CONCUR’ 96, LNCS 1119, pages 546–562, 1996.
S. Tasiran and R. Brayton. STARI: a case study in compositional and hierarchical timing verification. In CAV’97, LNCS 1254, pages 191–201, 1997.
S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations. In Proceedings of the Eighth Conference on Computer Aided Verification, LNCS 1102, 1996.
K. Čerāns. Decidability of bisimulation equivalence for parallel timer processes. In CAV’92, LNCS 663, pages 302–315, 1992.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. of the First IEEE Symp. on Logic in Computer Science, pages 332–344, 1986.
T. Wilke. Specifying state sequences in powerful decidable logics and timed automata. In FTRTFT’94, LNCS 863, pages 694–715. Springer-Verlag, 1994.
M. Yannakakis and D. Lee. An efficient algorithm for minimizing real-time transition systems. In CAV’93, LNCS 697, pages 210–224, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R. (1999). Timed Automata. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_3
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive