Advertisement

Flat Model Checking for Counting LTL Using Quantifier-Free Presburger Arithmetic

  • Normann Decker
  • Anton Pirogov
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

Abstract

This paper presents an approximation approach to verifying counter systems with respect to properties formulated in an expressive counting extension of linear temporal logic. It can express, e.g., that the number of acknowledgements never exceeds the number of requests to a service, by counting specific positions along a run and imposing arithmetic constraints. The addressed problem is undecidable and therefore solved on flat under-approximations of a system. This provides a flexibly adjustable trade-off between exhaustiveness and computational effort, similar to bounded model checking. Recent techniques and results for model-checking frequency properties over flat Kripke structures are lifted and employed to construct a parametrised encoding of the (approximated) problem in quantifier-free Presburger arithmetic. A prototype implementation based on the z3 SMT solver demonstrates the effectiveness of the approach based on problems from the RERS Challange.

Notes

Acknowledgement

We thank Daniel Thoma for valuable technical discussions.

References

  1. 1.
    Abdulla, P.A., Atig, M.F., Meyer, R., Salehi, M.S.: What’s decidable about availability languages? In: FSTTCS. LIPIcs, vol. 45, pp. 192–205 (2015)Google Scholar
  2. 2.
    Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005).  https://doi.org/10.1007/11562948_35CrossRefGoogle Scholar
  3. 3.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300–309. ACM (2007)Google Scholar
  4. 4.
    Biere, A.: Bounded model checking. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009)Google Scholar
  5. 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_14CrossRefGoogle Scholar
  6. 6.
    Bollig, B., Decker, N., Leucker, M.: Frequency linear-time temporal logic. In: TASE, pp. 85–92. IEEE (2012)Google Scholar
  7. 7.
    Borosh, I., Treybig, L.B.: Bounds on positive integral solutions of linear Diophantine equations. Proc. Am. Math. Soc. 55(2), 299–304 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  8. 8.
    Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS, pp. 123–133. IEEE (1995)Google Scholar
  9. 9.
    Caniart, N., Fleury, E., Leroux, J., Zeitoun, M.: Accelerating interpolation-based model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 428–442. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_32CrossRefGoogle Scholar
  10. 10.
    Cok, D.R., Stump, A., Weber, T.: The 2013 evaluation of SMT-COMP and SMT-LIB. J. Autom. Reason. 55(1), 61–90 (2015)MathSciNetzbMATHCrossRefGoogle Scholar
  11. 11.
    Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262–276. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44622-2_17CrossRefGoogle Scholar
  12. 12.
    Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and presburger arithmetic. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 268–279. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0028751CrossRefGoogle Scholar
  13. 13.
    Decker, N., Habermehl, P., Leucker, M., Sangnier, A., Thoma, D.: Model-checking counting temporal logics on flat structures. In: CONCUR. LIPIcs, vol. 85, pp. 29:1–29:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)Google Scholar
  14. 14.
    Demri, S., Dhar, A.K., Sangnier, A.: Equivalence between model-checking flat counter systems and Presburger arithmetic. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 85–97. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11439-2_7CrossRefGoogle Scholar
  15. 15.
    Demri, S., Dhar, A.K., Sangnier, A.: Taming past LTL and flat counter systems. Inf. Comput. 242, 306–339 (2015)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Demri, S., D’Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380–415 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Dhar, A.K.: Algorithms for model-checking flat counter systems. Ph.D. thesis, Université Paris Diderot (2014)Google Scholar
  18. 18.
    Čerāns, K.: Deciding properties of integral relational automata. In: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 35–46. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58201-0_56CrossRefGoogle Scholar
  19. 19.
    Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Softw. Pract. Exp. 30(11), 1203–1233 (2000)zbMATHCrossRefGoogle Scholar
  20. 20.
    Hoenicke, J., Meyer, R., Olderog, E.-R.: Kleene, Rabin, and Scott are available. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 462–477. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_32CrossRefGoogle Scholar
  21. 21.
    Hojjat, H., Iosif, R., Konečný, F., Kuncak, V., Rümmer, P.: Accelerating interpolants. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 187–202. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33386-6_16CrossRefGoogle Scholar
  22. 22.
    Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems - the RERS challenges 2012 and 2013. STTT 16(5), 457–464 (2014)CrossRefGoogle Scholar
  23. 23.
    Kroening, D., Weissenbacher, G.: Verification and falsification of programs with loops using predicate abstraction. Formal Asp. Comput. 22(2), 105–128 (2010)zbMATHCrossRefGoogle Scholar
  24. 24.
    Kuhtz, L., Finkbeiner, B.: Weak Kripke structures and LTL. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 419–433. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23217-6_28CrossRefGoogle Scholar
  25. 25.
    Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In: TIME, pp. 51–58. IEEE (2010)Google Scholar
  26. 26.
    Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. Log. Methods Comput. Sci. 9(1), 1–34 (2012)MathSciNetzbMATHGoogle Scholar
  27. 27.
    Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 402–416. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-28644-8_26CrossRefGoogle Scholar
  28. 28.
    Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc., Upper Saddle River (1967)zbMATHGoogle Scholar
  29. 29.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  30. 30.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)Google Scholar
  31. 31.
    Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa, pp. 92–101 (1929)Google Scholar
  32. 32.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.ISP, Universität zu LübeckLübeckGermany
  2. 2.RWTH Aachen UniversityAachenGermany

Personalised recommendations