Abstract
State-of-the-art algorithms for on-the-fly automata-theoretic LTL model checking make use of nested depth-first search to look for accepting cycles in the product of the system and the Büchi automaton. Here we present a new algorithm based on Tarjan’s algorithm for detecting strongly connected components. We show its correctness, describe how it can be efficiently implemented, and discuss its interaction with other model checking techniques, such as bitstate hashing. The algorithm is compared to the old algorithms through experiments on both random and actual state spaces, using random and real formulas. Our measurements indicate that our algorithm investigates at most as many states as the old ones. In the case of a violation of the correctness property, the algorithm often explores significantly fewer states.
Chapter PDF
Similar content being viewed by others
Keywords
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
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 233–242. Springer, Heidelberg (1991)
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)
Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear time temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. 2nd ACM Workshop Formal Methods in Software Practice, March 1998, pp. 7–15 (1998), Related site: http://www.cis.ksu.edu/santos/spec-patterns (Last updated September 1998)
Edelkamp, S., Leue, S., Lluch Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Tech. Rep. 161, Institut für Informatik, Albert-Ludwigs-Universität Freiburg (October 2001)
Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 154–167. Springer, Heidelberg (2000)
Eve, J., Kurki-Suonio, R.: On computing the transitive closure of a relation. Acta Informatica 8, 303–314 (1977)
Gabow, H.N.: Path-based depth-first search for strong and biconnected components. Tech. Rep. CU–CS–890–99, Dept. Computer Science, Univ. of Colorado at Boulder (February 2000)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. 15th IFIP Symp. Protocol Specification, Testing, and Verification, June 1995, pp. 3–18 (1995)
Godefroid, P.: Partial-order Methods for the Verification of Concurrent Systems, An Approach to the State-explosion Problem. PhD thesis, University of Liège (December 1994); Also published as Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)
Godefroid, P., Holzmann, G.J., Pirottin, D.: State space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 175–186. Springer, Heidelberg (1993)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall Software Series (1991)
Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. 2nd Spin Workshop, August 1996, pp. 23–32 (1996)
Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. Computer Communication Review 17(5), 126–135 (1987)
Nuutila, E., Soisalon-Soininen, E.: On finding the strongly connected components in a directed graph. Information Processing Letters 49(1), 9–14 (1994)
Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)
Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 39–54. Springer, Heidelberg (2001)
Sharir, M.: A strong-connectivity algorithm and its application in data flow analysis. Computer and Mathematics with Applications 7(1), 67–72 (1981)
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–267. Springer, Heidelberg (2000)
Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal of Computing 1(2), 146–160 (1972)
Tauriainen, H.: A randomized testbench for algorithms translating linear temporal logic formulae into Büchi automata. In: Proc. Workshop Concurrency, Specifications, and Programming, September 1999, pp. 251–262 (1999)
Tel, G.: Introduction to Distributed Algorithms, 2nd edn. Cambridge University Press, Cambridge (2000)
Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1(1), 297–322 (1992)
Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. Symp. Foundations of Computer Science, November 1983, pp. 185–194 (1983)
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. 35th ACM/IEEE Conf. Design Automation, June 1998, pp. 599–604 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Geldenhuys, J., Valmari, A. (2004). Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive