The theory of timed automata

  • Rajeev Alur
  • David Dill
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


We propose timed automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words — strings in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.


Real-time systems Automatic verification Formal languages Automata theory 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ACD90]
    Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for real-time systems. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 414–425, 1990.Google Scholar
  2. [ACD91]
    Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking for probabilistic real-time systems. In Automata, Languages and Programming: Proceedings of the 18th ICALP, Lecture Notes in Computer Science 510, 1991.Google Scholar
  3. [AFH91]
    Rajeev Alur, Tomás Feder, and Thomas Henzinger. The benefits of relaxing punctuality. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 139–152, 1991.Google Scholar
  4. [Alu91]
    Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.Google Scholar
  5. [BCD+90]
    J.R. Burch, E.M. Clarke, D.L. Dill, L.J. Hwang, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, pages 428–439, 1990.Google Scholar
  6. [Büc62]
    Richard Büchi. On a decision method in restricted second-order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science 1960, pages 1–12. Stanford University Press, 1962.Google Scholar
  7. [CDK89]
    E.M. Clarke, I.A. Draghicescu, and R.P. Kurshan. A unified approach for showing language containment and equivalence between various types of ω-automata. Technical report, Carnegie Mellon University, 1989.Google Scholar
  8. [CES86]
    Edmund Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.CrossRefGoogle Scholar
  9. [Cho74]
    Yaacov Choueka. Theories of automata on ω-tapes: a simplified approach. Journal of Computer and System Sciences, 8:117–141, 1974.Google Scholar
  10. [CY91]
    Costas Courcoubetis and Mihalis Yannakakis. Minimum and maximum delay problems in real-time systems. In Proceedings of the Third Workshop on Computer-Aided Verification, Aalborg University, Denmark, 1991.Google Scholar
  11. [DW90]
    David Dill and Howard Wong-Toi. Synthesizing processes and schedulers from temporal specifications. In Proceedings of the Second Workshop on Computer-Aided Verification, Rutgers University, 1990.Google Scholar
  12. [EC82]
    E. Allen Emerson and Edmund M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.CrossRefGoogle Scholar
  13. [GW91]
    Patrice Godefroid and Pierre Wolper. A partial approach to model-checking. In Proceedings of the Sixth IEEE Symposium on Logic in Computer Science, pages 406–415, 1991.Google Scholar
  14. [Hoa78]
    C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.CrossRefGoogle Scholar
  15. [HU79]
    John Hopcroft and Jeff Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.Google Scholar
  16. [Kur87]
    Robert Kurshan. Complementing deterministic Büchi automata in polynomial time. Journal of Computer and System Sciences, 35:59–71, 1987.CrossRefGoogle Scholar
  17. [Lam83]
    Leslie Lamport. What good is temporal logic? In R.E.A. Mason, editor, Information Processing 83: Proceedings of the Ninth IFIP World Computer Congress, pages 657–668. Elsevier Science Publishers, 1983.Google Scholar
  18. [McN66]
    Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.Google Scholar
  19. [MP81]
    Zohar Manna and Amir Pnueli. The temporal framework for concurrent programs. In R.S. Boyer and J.S. Moore, editors, The correctness problem in Computer science, pages 215–274. Academic Press, 1981.Google Scholar
  20. [Pnu77]
    Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–77, 1977.Google Scholar
  21. [Pnu86]
    Amir Pnueli. Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In Current Trends in Concurrency, Lecture Notes in Computer Science 224, pages 510–584. Springer-Verlag, 1986.Google Scholar
  22. [Rog67]
    Hartley Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.Google Scholar
  23. [Saf88]
    Shmuel Safra. On the complexity of ω-automata. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science, pages 319–327, 1988.Google Scholar
  24. [SVW87]
    A. Prasad Sistla, Moshe Vardi, and Pierre Wolper. The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science, 49, 1987.Google Scholar
  25. [Tho90]
    Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. Elsevier Science Publishers, 1990.Google Scholar
  26. [Var87]
    Moshe Vardi. Verification of concurrent programs — the automata-theoretic framework. In Proceedings of the Second IEEE Symposium on Logic in Computer Science, pages 167–176, 1987.Google Scholar
  27. [VW86]
    Moshe Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First IEEE Symposium on Logic in Computer Science, pages 332–344, 1986.Google Scholar
  28. [WH91]
    Howard Wong-Toi and Girard Hoffmann. The control of dense real-time discrete event systems. 1991.Google Scholar
  29. [WVS83]
    Pierre Wolper, Moshe Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths. In Proceedings of the 24th IEEE Symposium on Foundations of Computer Science, pages 185–194, 1983.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Rajeev Alur
    • 1
  • David Dill
    • 2
  1. 1.AT&T Bell LaboratoriesMurray HillUSA
  2. 2.Department of Computer ScienceStanford UniversityStanfordUSA

Personalised recommendations