Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Timed Automata: Semantics, Algorithms and Tools

  • Chapter
Lectures on Concurrency and Petri Nets (ACPN 2003)

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

Included in the following conference series:

Abstract

This chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the concrete and abstract semantics of timed automata (based on transition rules, regions and zones), decision problems, and algorithms for verification. A detailed description on DBM (Difference Bound Matrices) is included, which is the central data structure behind several verification tools for timed systems. As an example, we give a brief introduction to the tool Uppaal.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Aceto, L., Bergueno, A., Larsen, K.G.: Model checking via reachability testing for timed automata. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 263. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  2. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)

    Google Scholar 

  3. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Journal of Information and Computation 104(1), 2–34 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  4. Alur, R., Courcoubetis, C., Henzinger, T.A.: The observational power of clocks. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 162–177. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  5. Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  6. Alur, R., Dill, D.L.: A theory of timed automata. Journal of Theoretical Computer Science 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  7. Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science 211(1-2), 253–273 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  8. Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM 41(1), 181–204 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  9. Balarin, F.: Approximate reachability analysis of timed automata. In: Proceedings, 17th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Los Alamitos (1996)

    Google Scholar 

  10. Behrmann, G., David, A., Larsen, K.G., Yi, W.: Unification & sharing in timed automata verification. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 225–229. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Behrmann, G., Larsen, K., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)

    MATH  Google Scholar 

  13. Bengtsson, J.: Reducing memory usage in symbolic state-space exploration for timed systems. Technical Report 2001-009, Department of Information Technology, Uppsala University (2001)

    Google Scholar 

  14. Bengtsson, J.: Clocks, dbms and states in timed systems. Ph.D. Thesis, ACTA Universitatis Upsaliensis 39, Uppsala University (2002)

    Google Scholar 

  15. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  16. Bentsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491–503. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Berthomieu, B., Diaz, M.: Modeling and verification of timed dependent systems using timed petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)

    Article  MathSciNet  Google Scholar 

  18. Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36, 145–182 (1998)

    MATH  MathSciNet  Google Scholar 

  19. Cerans, K.: Decidability of bisimulation equivalences for parallel timer processes. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663. Springer, Heidelberg (1992)

    Google Scholar 

  20. Chaochen, Z.: Duration calculus, a logical approach to real-time systems. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 1–7. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  21. David, A., Behrmann, G., Larsen, K.G., Yi, W.: A tool architecture for the next genreation of UPPAAL. Technical Report 2003-011, Department of Information Technology, Uppsala University (2003)

    Google Scholar 

  22. Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proceedings, 17th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Los Alamitos (1996)

    Google Scholar 

  23. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1989)

    Google Scholar 

  24. Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: Schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67–82. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Floyd, R.W.: Acm algorithm 97: Shortest path. Communications of the ACM 5(6), 345 (1962)

    Article  Google Scholar 

  26. Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)

    Google Scholar 

  27. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 394–406 (1992)

    Google Scholar 

  28. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Journal of Information and Computation 111(2), 193–244 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  29. Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21(8), 666–676 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  30. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)

    Google Scholar 

  31. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of realtime systems: Compact data structure and state space reduction. In: Proceedings, 18th IEEE Real-Time Systems Symposium, pp. 14–24. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  32. Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nordic Journal of Computing (1999)

    Google Scholar 

  33. Larsen, K.G., Petterson, P., Yi, W.: UPPAAL in a nutshell. Journal on Software Tools for Technology Transfer (1997)

    Google Scholar 

  34. Larsen, K.G., Pettersson, P., Yi, W.: Compositional and Symbolic Model- Checking of Real-Time Systems. In: Proc. of the 16th IEEE Real-Time Systems Symposium, December 1995, pp. 76–87. IEEE Computer Society Press, Los Alamitos (1995)

    Chapter  Google Scholar 

  35. Larsen, K.G., Wang, Y.: Time-abstracted bisimulation: Implicit specifications and decidability. Information and Computation 134(2), 75–101 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  36. Larsson, F.: Efficient implementation of model-checkers for networks of timed automata. Licentiate Thesis 2000-003, Department of Information Technology, Uppsala University (2000)

    Google Scholar 

  37. Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gear-Box Controller. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 281–297. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  38. Lindahl, M., Pettersson, P., Yi, W.: Formal Design and Analysis of a Gearbox Controller. Springer International Journal of Software Tools for Technology Transfer (STTT) 3(3), 353–368 (2001)

    MATH  Google Scholar 

  39. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  40. Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: Theory and application. Journal of Information and Computation 114(1), 131–178 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  41. Pettersson, P.: Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis, Uppsala University (1999)

    Google Scholar 

  42. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theoretical Computer Science 58(1-3), 249–261 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  43. Rokicki, T.G.: Representing and Modeling Digital Circuits. PhD thesis, Stanford University (1993)

    Google Scholar 

  44. Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987. Springer, Heidelberg (1995)

    Google Scholar 

  45. Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 59–70. Springer, Heidelberg (1993)

    Google Scholar 

  46. Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 210–224. Springer, Heidelberg (1993)

    Google Scholar 

  47. Yi, W.: CCS + time = an interleaving model for real time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510. Springer, Heidelberg (1991)

    Google Scholar 

  48. Yi, W., Jonsson, B.: Decidability of timed language-inclusion for networks of realtime communicating sequen tial processes. In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol. 880. Springer, Heidelberg (1994)

    Google Scholar 

  49. Yi, W., Petterson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: Proceedings, Seventh International Conference on Formal Description Techniques, pp. 223–238 (1994)

    Google Scholar 

  50. Yovine, S.: Kronos: a verification tool for real-time systems. Journal on Software Tools for Technology Transfer 1 (October 1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Uppsala University,  

    Johan Bengtsson & Wang Yi

Authors
  1. Johan Bengtsson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wang Yi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Applied Computer Science, Catholic University of Eichstätt-Ingolstadt,  

    Jörg Desel

  2. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Wolfgang Reisig

  3. , Leiden Center of Advanced Computer Science (LIACS), Leiden University, Niels Bohrweg 1, 2333, Leiden, CA, The Netherlands

    Grzegorz Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bengtsson, J., Yi, W. (2004). Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds) Lectures on Concurrency and Petri Nets. ACPN 2003. Lecture Notes in Computer Science, vol 3098. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27755-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-27755-2_3

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-27755-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation