Advertisement

Memory-Efficient Tactics for Randomized LTL Model Checking

  • Kim LarsenEmail author
  • Doron Peled
  • Sean Sedwards
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

We study model checking of LTL properties by means of random walks, improving on the efficiency of previous results. Using a randomized algorithm to detect accepting paths makes it feasible to check extremely large models, however a naive approach may encounter many non-accepting paths or require the storage of many explicit states, making it inefficient. We study here several alternative tactics that can often avoid these problems. Exploiting probability and randomness, we present tactics that typically use only a small fraction of the memory of previous approaches, storing only accepting states or an arbitrarily small number of “token” states visited during executions. Reducing the number of stored states generally increases the expected execution time until a counterexample is found, but we demonstrate that the trade-off is biased in favor of our tactics. By applying our memory-efficient tactics to scalable models from the literature, we show that the increase in time is typically less than proportional to the saving in memory and may be exponentially smaller.

References

  1. 1.
    Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441–461 (1990)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Brim, L., Černá, I., Nečesal, M.: Randomization helps in LTL model checking. In: de Alfaro, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 105–119. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44804-7_7 CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  4. 4.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, pp. 3–18 (1995)Google Scholar
  5. 5.
    Grosu, R., Smolka, S.: Monte Carlo model checking. In: 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, pp. 271–286 (2005)Google Scholar
  6. 6.
    Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_8 CrossRefGoogle Scholar
  7. 7.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006).  https://doi.org/10.1007/11691372_29 CrossRefGoogle Scholar
  8. 8.
    Holzmann, G.J.: The SPIN Model Checker. Pearson Education, Boston (2003)Google Scholar
  9. 9.
    Lehmann, D.J., Rabin, M.O.: On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, Williamsburg, Virginia, USA, January 1981, pp. 133–138 (1981)Google Scholar
  10. 10.
    Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pp. 141–154 (1983)Google Scholar
  11. 11.
    Oudinet, J., Denise, A., Gaudel, M., Lassaigne, R., Peyronnet, S.: Uniform Monte-Carlo model checking. In: 14th International Conference on Fundamental Approaches to Software Engineering, FASE 2011, pp. 127–140 (2011)Google Scholar
  12. 12.
    Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4(2), 177–192 (1970)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733–749 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–192. MIT Press, Cambridge (1990)Google Scholar
  15. 15.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of IEEE Symposium on Logic in Computer Science, Boston, July 1986, pp. 332–344 (1986)Google Scholar
  16. 16.
    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_17 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of AalborgAalborgDenmark
  2. 2.Department of ScienceBar Ilan UniversityRamat GanIsrael
  3. 3.National Institute of InformaticsTokyoJapan

Personalised recommendations