Skip to main content
SpringerLink
Log in

Distributed Algorithms for Time Optimal Reachability Analysis

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2016)

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

Abstract

Time optimal reachability analysis is a novel model based technique for solving scheduling and planning problems. After modeling them as reachability problems using timed automata, a real-time model checker can compute the fastest trace to the goal states which constitutes a time optimal schedule. We propose distributed computing to accelerate time optimal reachability analysis. We develop five distributed state exploration algorithms, implement them in Uppaal enabling it to exploit the compute resources of a dedicated model-checking cluster. We experimentally evaluate the implemented algorithms with four models in terms of their ability to compute near- or proven-optimal solutions, their scalability, time and memory consumption and communication overhead. Our results show that distributed algorithms work much faster than sequential algorithms and have good speedup in general.

This work has been supported by Danish National Research Foundation – Center for Foundations of Cyber-Physical Systems, a Sino-Danish research center.

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 EPUB and 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

Notes

  1. 1.

    For real Uppaal models, the location is a vector of locations from each parallelly composed timed automata and the values of all discrete variables in the model.

  2. 2.

    http://www.kasahara.elec.waseda.ac.jp/schedule/stgarc_e.html.

References

  1. Abdeddaim, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272–300 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Barnat, J., Brim, L., Češka, M., Ročkai, P.: DiVinE: parallel distributed model checker (tool paper). In: HiBi/PDMC, pp. 4–7. IEEE (2010)

    Google Scholar 

  4. Barnat, J., Bauch, P., Brim, L., Ceska, M.: Designing fast LTL model checking algorithms for many-core gpus. J. Parallel Distrib. Comput. 72(9), 1083–1097 (2012)

    Article  Google Scholar 

  5. Behrmann, G.: Distributed reachability analysis in timed automata. STTT 7(1), 19–30 (2005)

    Article  Google Scholar 

  6. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T.: Efficient guiding towards cost-optimality in UPPAAL. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: 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 

  9. Behrmann, G., Hune, T., Vaandrager, F.W.: Distributing timed model checking - how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Bengtsson, J.E., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)

    Google Scholar 

  13. Fehnker, A.: Bounding and Heuristics in Forward Reachability Algorithms. UB Nijmegen [Host] (2000)

    Google Scholar 

  14. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  15. Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: FCT, pp. 62–88 (1995)

    Google Scholar 

  16. Niebert, P., Tripakis, S., Yovine, S.: Minimum-time reachability for timed automata. In: IEEE Mediteranean Control Conference (2000)

    Google Scholar 

  17. Stern, U., Dill, D.L.: Parallelizing the Mur\(\varphi \) verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  18. Tel, G.: Introduction to Distributed Algorithms, 2nd edn. Cambridge University Press, New York (2001)

    MATH  Google Scholar 

  19. Verstoep, K., Bal, H.E., Barnat, J., Brim, L.: Efficient large-scale model checking. In: IPDPS, pp. 1–12 (2009)

    Google Scholar 

  20. Zhang, Z., Nielsen, B., Larsen, K.G.: Time optimal reachability analysis using swarm verification. In: SAC SVT, pp. 1634–1640 (2016)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aalborg University, Aalborg, Denmark

    Zhengkui Zhang, Brian Nielsen & Kim G. Larsen

Authors
  1. Zhengkui Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Brian Nielsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhengkui Zhang .

Editor information

Editors and Affiliations

  1. Carl von Ossietzky Universität , Oldenburg, Germany

    Martin Fränzle

  2. LSV, ENS de Cachan , Cachan Cedex, France

    Nicolas Markey

A Results for Runtime

A Results for Runtime

Table 6. Runtime (sec) of Aircraft-Landing-15
Full size table
Fig. 4.
figure 4

Cost vs. Runtime for Aircraft-Landing-15

Full size image

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Zhang, Z., Nielsen, B., Larsen, K.G. (2016). Distributed Algorithms for Time Optimal Reachability Analysis. In: Fränzle, M., Markey, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2016. Lecture Notes in Computer Science(), vol 9884. Springer, Cham. https://doi.org/10.1007/978-3-319-44878-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-44878-7_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-44877-0

  • Online ISBN: 978-3-319-44878-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation