Skip to main content
SpringerLink
Log in

Lazy Reachability Checking for Timed Automata Using Interpolants

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

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

Abstract

To solve the reachability problem for timed automata, model checkers usually apply forward search and zone abstraction. To ensure efficiency and termination, the computed zones are generalized using maximal constants obtained from guards either by static analysis or lazily for a given path. In this paper, we propose a lazy method based on zone abstraction that, instead of the constants in guards, considers the constraints themselves. The method is a combination of forward search, backward search and interpolation over zones: if the zone abstraction is too coarse, we propagate a zone representing bad states backwards using backward search, and use interpolation to extract a relevant zone to strengthen the current abstraction. We propose two refinement strategies in this framework, and evaluate our method on the usual benchmark models for timed automata. Our experiments show that the proposed method compares favorably to known methods based on efficient lazy non-convex abstractions.

T. Tóth—This work was partially supported by Gedeon Richter’s Talentum Foundation (Gyömrői út 19-21, 1103 Budapest, Hungary).

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.

    http://theta.inf.mit.bme.hu.

  2. 2.

    http://www.comp.nus.edu.sg/~pat/bddlib/timedexp.html.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). doi:10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  2. 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–270. Springer, Heidelberg (2003). doi:10.1007/3-540-36577-X_18

    Chapter  Google Scholar 

  3. 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). doi:10.1007/978-3-540-24730-2_25

    Chapter  Google Scholar 

  4. Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27755-2_3

    Chapter  Google Scholar 

  5. Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods Syst. Des. 24(3), 281–320 (2004). doi:10.1023/B:FORM.0000026093.21513.31

    Article  MATH  Google Scholar 

  6. Bouyer, P., Laroussinie, F., Reynier, P.-A.: Diagonal constraints in timed automata: forward analysis of timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 112–126. Springer, Heidelberg (2005). doi:10.1007/11603009_10

    Chapter  Google Scholar 

  7. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 397–412. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_30

    Chapter  Google Scholar 

  8. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003). doi:10.1145/876638.876643

    Article  MathSciNet  MATH  Google Scholar 

  9. Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998). doi:10.1007/BFb0054180

    Chapter  Google Scholar 

  10. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2012, pp. 58–70. ACM (2002). doi:10.1145/503272.503279

  11. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 990–1005. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_71

    Chapter  Google Scholar 

  12. Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: FSTTCS 2011. LIPIcs, vol. 13, pp. 78–89 (2011). doi:10.4230/LIPIcs.FSTTCS.2011.78

  13. Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. In: LICS 2012, pp. 375–384. IEEE (2012). doi:10.1109/LICS.2012.48

  14. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_1

    Chapter  Google Scholar 

  15. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). doi:10.1007/11817963_14

    Chapter  Google Scholar 

  16. McMillan, K.L.: Lazy annotation for program testing and verification. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 104–118. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_10

    Chapter  Google Scholar 

  17. Tóth, T., Majzik, I.: Timed automata verification using interpolants. In: Proceedings of the 24th PhD Mini-Symposium, pp. 82–85. BUTE DMIS (2017). doi:10.5281/zenodo.291907

  18. Wang, W., Jiao, L.: Difference bound constraint abstraction for timed automata reachability checking. In: Graf, S., Viswanathan, M. (eds.) FORTE 2015. LNCS, vol. 9039, pp. 146–160. Springer, Cham (2015). doi:10.1007/978-3-319-19195-9_10

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary

    Tamás Tóth & István Majzik

Authors
  1. Tamás Tóth
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. István Majzik
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tamás Tóth .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, United Kingdom

    Alessandro Abate

  2. Dept. d’Informatique, Université Libre de Bruxelles, Brussels, Belgium

    Gilles Geeraerts

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Tóth, T., Majzik, I. (2017). Lazy Reachability Checking for Timed Automata Using Interpolants. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65765-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65764-6

  • Online ISBN: 978-3-319-65765-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation