Skip to main content
SpringerLink
Log in
Book cover

Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems)

REX 1991: Real-Time: Theory in Practice pp 45–73Cite as

The theory of timed automata

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 600))

Abstract

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.

Supported by the NSF under grant MIP-8858807.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. Rajeev Alur. Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University, 1991.

    Google Scholar 

  5. 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. 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. 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. 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.

    Article  Google Scholar 

  9. Yaacov Choueka. Theories of automata on ω-tapes: a simplified approach. Journal of Computer and System Sciences, 8:117–141, 1974.

    Google Scholar 

  10. 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. 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. E. Allen Emerson and Edmund M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241–266, 1982.

    Article  Google Scholar 

  13. 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. C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978.

    Article  Google Scholar 

  15. John Hopcroft and Jeff Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

    Google Scholar 

  16. Robert Kurshan. Complementing deterministic Büchi automata in polynomial time. Journal of Computer and System Sciences, 35:59–71, 1987.

    Article  Google Scholar 

  17. 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. Robert McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.

    Google Scholar 

  19. 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. 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. 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. Hartley Rogers. Theory of Recursive Functions and Effective Computability. McGraw-Hill, 1967.

    Google Scholar 

  23. 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. 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. 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. 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. 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. Howard Wong-Toi and Girard Hoffmann. The control of dense real-time discrete event systems. 1991.

    Google Scholar 

  29. 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 

Download references

Author information

Authors and Affiliations

  1. AT&T Bell Laboratories, 07974, Murray Hill, NJ, USA

    Rajeev Alur

  2. Department of Computer Science, Stanford University, 94305, Stanford, CA, USA

    David Dill

Authors
  1. Rajeev Alur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Dill
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker C. Huizing W. P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Dill, D. (1992). The theory of timed automata. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031987

Download citation

  • DOI: https://doi.org/10.1007/BFb0031987

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55564-3

  • Online ISBN: 978-3-540-47218-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation