Advertisement

Abstract

The automata-theoretic approach to LTL verification relies on an algorithm for finding accepting cycles in a Büchi automaton. Explicit-state model checkers typically construct the automaton “on the fly” and explore its states using depth-first search. We survey algorithms proposed for this purpose and identify two good algorithms, a new algorithm based on nested DFS, and another based on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

Keywords

Model Check Linear Temporal Logic Strongly Connect Component Software Model Check Minimal Exploration 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 222–235. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Černá, I., Pelánek, R.: Relating hierarchy of linear temporal properties to model checking. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318–327. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Clarke, E., Emerson, A., Sistla, P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8, 244–263 (1986)zbMATHCrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  5. 5.
    Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1(2/3), 275–288 (1992)CrossRefGoogle Scholar
  6. 6.
    Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit-state model checking in the validation of communication protocols. In: STTT (2004)Google Scholar
  8. 8.
    Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Gabow, H.N.: Path-based depth-first search for strong and biconnected components. Information Processing Letters 74(3–4), 107–114 (2000)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 92–108. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Geldenhuys, J., Valmari, A.: Tarjan’s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 205–219. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of PSTV. IFIP, pp. 3–18 (1996)Google Scholar
  13. 13.
    Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design 13(3), 289–307 (1998)CrossRefMathSciNetGoogle Scholar
  14. 14.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)Google Scholar
  15. 15.
    Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: Proc. 2nd SPIN Workshop, pp. 23–32 (1996)Google Scholar
  16. 16.
    Kupferman, O., Vardi, M.Y.: Freedom, weakness, and determinism: From linear-time to branching-time. In: Proc. of LICS, pp. 81–92. IEEE, Los Alamitos (1998)Google Scholar
  17. 17.
    Nuutila, E., Soisalon-Soininen, E.: On finding the strongly connected components in a directed graph. Information Processing Letters 49, 9–14 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Peled, D.A.: Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8(1), 39–64 (1996)CrossRefGoogle Scholar
  19. 19.
    Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. Technical Report 2004/06, Universität Stuttgart (November 2004)Google Scholar
  20. 20.
    Sharir, M.: A strong-connectivity algorithm and its applications in data flow analysis. Computers and Mathematics with Applications 7(1), 67–72 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  22. 22.
    Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Tauriainen, H.: Nested emptiness search for generalized Büchi automata. Technical Report A79, Helsinki University of Technology (July 2003)Google Scholar
  24. 24.
    Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. Journal of Computer and System Sciences 32, 183–221 (1986)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Stefan Schwoon
    • 1
  • Javier Esparza
    • 1
  1. 1.Institut für Formale Methoden der InformatikUniversität Stuttgart 

Personalised recommendations