Skip to main content
SpringerLink
Log in

Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11119))

Abstract

We study the reduction of bounded reachability analysis of timed automata (TA) to a Mixed Integer Linear Programming (MILP) problem. While bounded model checking of timed automata has been explored in the literature based on the satisfiability of Boolean constraint formulas over linear arithmetic constraints verified using SAT Modulo Theory (SMT) solvers, the approach presented in this paper opens up the alternative of using MILP solvers. We present some preliminary results comparing the two approaches and provide ideas on how linear optimization can be useful for analyzing the behavior of TA. The results are supported by a prototype implementation which relies either on a MILP solver (Gurobi) or an SMT solver (MathSAT). Certain techniques for reducing the search space and improving the performance are also discussed.

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.

    https://www.irit.fr/~Iulian.Ober/brat.

  2. 2.

    https://www.it.uu.se/research/group/darts/uppaal/benchmarks.

References

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

    Article  MathSciNet  Google Scholar 

  2. Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 243–259. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36135-9_16

    Chapter  MATH  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exper. 41(2), 133–142 (2011)

    Article  Google Scholar 

  4. 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). https://doi.org/10.1007/BFb0055643

    Chapter  Google Scholar 

  5. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

  6. Bouyer, P.: Weighted timed automata: model-checking and games. Electron. Notes Theor. Comput. Sci. 158, 3–17 (2006). Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXII)

    Google Scholar 

  7. Bozga, M., Graf, S., Mounier, L., Ober, I., Roux, J.-L., Vincent, D.: Timed extensions for SDL. In: Reed, R., Reed, J. (eds.) SDL 2001. LNCS, vol. 2078, pp. 223–240. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-48213-X_14

    Chapter  MATH  Google Scholar 

  8. Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237–267. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_8

    Chapter  MATH  Google Scholar 

  9. Bu, L., Cimatti, A., Li, X., Mover, S., Tonetta, S.: Model checking of hybrid systems using shallow synchronization. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE -2010. LNCS, vol. 6117, pp. 155–169. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13464-7_13

    Chapter  Google Scholar 

  10. Damm, W., Olderog, E.-R. (eds.): FTRTFT 2002. LNCS, vol. 2469. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45739-9

    Book  MATH  Google Scholar 

  11. David, A., Möller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218–232. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45923-5_15

    Chapter  Google Scholar 

  12. 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). https://doi.org/10.1007/3-540-52148-8_17

    Chapter  Google Scholar 

  13. Fränzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. Electron. Notes Theor. Comput. Sci. 133, 119–137 (2005)

    Article  Google Scholar 

  14. Graf, S.: Expression of time and duration constraints in SDL. In: Sherratt, E. (ed.) SAM 2002. LNCS, vol. 2599, pp. 38–52. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36573-7_3

    Chapter  Google Scholar 

  15. Graf, S.: OMEGA: correct development of real time and embedded systems. Softw. Syst. Model. 7(2), 127–130 (2008)

    Article  Google Scholar 

  16. Gurobi Optimization Inc., Reference manual v. 7.5. https://www.gurobi.com/documentation/7.5/refman.pdf. Accessed on 8 June 2018

  17. Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: Damm and Olderog [10], pp. 395–416

    Google Scholar 

  18. Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6, 271–298 (1999)

    Google Scholar 

  19. Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27–59 (2005)

    Article  MathSciNet  Google Scholar 

  20. Malinowski, J., Niebert, P.: SAT based bounded model checking with partial order semantics for timed automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 405–419. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_34

    Chapter  MATH  Google Scholar 

  21. MathSAT 5. http://mathsat.fbk.eu. Accessed 8 June 2018

  22. Möller, O.: CSMA/CD protocol specification (UPPAAL benchmark). https://www.it.uu.se/research/group/darts/uppaal/benchmarks/#CSMA. Accessed 8 June 2018

  23. Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley-Interscience, New York (1988)

    Book  Google Scholar 

  24. Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm and Olderog [10], pp. 225–244

    Google Scholar 

  25. M. Sorea. Bounded model checking for timed automata. Electron. Notes Theor. Comput. Sci. 68(5), 116–134 (2003). MTCS 2002, Models for Time-Critical Systems (CONCUR 2002 Satellite Workshop)

    Google Scholar 

  26. Wang, F.: Efficient verification of timed automata with BDD-like data structures. STTT 6(1), 77–97 (2004)

    Article  MathSciNet  Google Scholar 

  27. Yovine, S.: KRONOS: A verification tool for real-time systems. STTT 1(1–2), 123–133 (1997)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Toulouse - IRIT, 118 Route de Narbonne, 31062, Toulouse, France

    Iulian Ober

Authors
  1. Iulian Ober
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Iulian Ober .

Editor information

Editors and Affiliations

  1. Technical University of Dortmund, Dortmund, Germany

    Falk Howar

  2. Masaryk University, Brno, Czech Republic

    Jiří Barnat

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ober, I. (2018). Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00244-2_18

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00243-5

  • Online ISBN: 978-3-030-00244-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation