Skip to main content
SpringerLink
Log in

Symbolic and Compositional Reachability for Timed Automata

  • Conference paper
Reachability Problems (RP 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6227))

Included in the following conference series:

  • 368 Accesses

Abstract

The model-checker Uppaal [LPY97] is based on the theory of timed automata [AD90] and its modeling languague offers additional features such as networks of timed automata, clocks and stop-watches, synchronizing over synchronous and broadcast channels, discrete variables ranging over bounded integers or structured types (arrays and records) as well as user-defined types and functions.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

References

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

    Chapter  Google Scholar 

  2. Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Abdeddaïm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 478–492. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  4. Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–277. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. STTT 8(3), 204–215 (2006)

    Article  Google Scholar 

  7. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing uppaal over 15 years. Software – Practice and Experience (to appear, 2010)

    Google Scholar 

  8. Bellman, R.: Dynamic programming and stochastic control processes. Information and Control 1(3), 228–239 (1958)

    Article  MATH  MathSciNet  Google Scholar 

  9. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Brekling, A.W., Hansen, M.R., Madsen, J.: Models and formal verification of multiprocessor system-on-chips. J. Log. Algebr. Program. 77(1-2), 1–19 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  11. Behrmann, G., Larsen, K.G., Andersen, H.R., Hulgaard, H., Lind-Nielsen, J.: Verification of hierarchical state/event systems using reusability and compositionality. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 163–177. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Behrmann, G., Larsen, K.G., 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 

  13. Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. 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 (1990)

    Google Scholar 

  15. David, A., Larsen, K.G., Illum, J., Skou, A.: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1. In: Model-Based Design for Embedded Systems. Computational Analysis, Synthesis, and Design of Dynamic Systems. CRC Press, Boca Raton (2009)

    Google Scholar 

  16. Hansen, M.R., Madsen, J., Brekling, A.W.: Semantics and verification of a language for modelling hardware architectures. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 300–319. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  17. Hendriks, M., van den Nieuwelaar, B., Vaandrager, F.W.: Model checker aided design of a controller for a wafer scanner. STTT 8(6), 633–647 (2006)

    Article  Google Scholar 

  18. Igna, G., Kannan, V., Yang, Y., Basten, T., Geilen, M., Vaandrager, F.W., Voorhoeve, M., de Smet, S., Somers, L.J.: Formal modeling and scheduling of datapaths of digital document printers. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 170–187. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Laroussinie, F., Larsen, K.G.: CMC: A tool for compositional model-checking of real-time systems. In: Proc. IFIP Joint Int. Conf. on Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE-PSTV’98), pp. 439–456. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  20. Laroussinie, F., Larsen, K.G.: Cmc: A tool for compositional model-checking of real-time systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) FORTE, IFIP Conference Proceedings, vol. 135, pp. 439–456. Kluwer, Dordrecht (1998)

    Google Scholar 

  21. Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: IEEE Real-Time Systems Symposium, pp. 14–24. IEEE Computer Society, Los Alamitos (1997)

    Google Scholar 

  22. Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic – and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995)

    Google Scholar 

  23. Lind-Nielsen, J., Andersen, H.R., Behrmann, G., Hulgaard, H., Kristoffersen, K. J., Larsen, K.G.: Verification of large state/event systems using compositionality and dependency analysis. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 201–216. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  24. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1(1-2), 134–152 (1997)

    MATH  Google Scholar 

  25. Nyman, U.: Compositional bachwards reachability of timed automata. Master’s thesis, Department of Computer Science, Aalborg University (2002)

    Google Scholar 

  26. Poulsen, D.B., van Vliet, J.W.B.P.T.: Concrete traces for uppaal. Master’s thesis, Department of Computer Science. Aalborg University (2010)

    Google Scholar 

  27. Tripakis, S., Yovine, S.: Analysis of timed systems based on time-abstracting bisimulation. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 232–243. Springer, Heidelberg (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Denmark

    Kim Guldstrand Larsen

Authors
  1. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic

    Antonín Kučera

  2. Department of Computer Science, University of Liverpool, Ashton Building, L69 3BX, Liverpool, England

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Larsen, K.G. (2010). Symbolic and Compositional Reachability for Timed Automata. In: Kučera, A., Potapov, I. (eds) Reachability Problems. RP 2010. Lecture Notes in Computer Science, vol 6227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15349-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15349-5_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15348-8

  • Online ISBN: 978-3-642-15349-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation