Nested Emptiness Search for Generalized Büchi Automata

• Autorzy: Tauriainen H.
• Języki publikacji: EN

Abstrakty

EN

We generalize the classic explicit-state emptiness checking algorithm for Büchi word automata (the nested depth-first search) into Büchi automata with multiple acceptance conditions. Avoiding a degeneralization step improves the algorithm's worst-case memory requirements and reduces the worst-case number of state visits during the search. We give experimental results and discuss changes needed to make the generalized algorithm compatible with well-known probabilistic explicit-state model checking techniques.

Słowa kluczowe

EN

model checking; Büchi automata; nested depth-first search

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 127--154
• Opis fizyczny: wykr., bibliogr. 32 poz.

Twórcy

autor

Tauriainen H.

• Helsinki University of Technology Laboratory for Theoretical Computer Science, P.O. Box 5400, FIN-02015 TKK, Finland,

Bibliografia

• [1] Aggarwal, S., Courcoubetis, C., Wolper, P.: Adding liveness properties to coupled finite-state machines, ACM Transactions on Programming Languages and Systems, 12(2), 1990, 303-339.
• [2] Bošnački, D.: A nested depth first search algorithm for model checking with symmetry reduction, Proceedings of the 22nd IFIPWG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002) (D. A. Peled, M. Y. Vardi, Eds.), LNCS 2529, Springer-Verlag, 2002.
• [3] Bošnački, D.: A light-weight algorithm for model checking with symmetry reduction and weak fairness, Proceedings of the 10th International SPIN Workshop on Model Checking Software (SPIN 2003) (T. Ball, S. K. Rajamani, Eds.), LNCS 2648, Springer-Verlag, 2003.
• [4] Brim, L., čern´a, I., Nečesal, M.: Randomization helps in LTL model checking, Proceedings of the Joint InternationalWorkshop on Process Algebra and ProbabilisticMethods, Performance Modeling and Verification (PAPM-PROBMIV 2001) (L. de Luca, S. Gilmore, Eds.), LNCS 2165, Springer-Verlag, 2001.
• [5] Choueka, Y.: Theories of automata on 􀀀-tapes: A simplified approach, Journal of Computer and System Sciences, 8(2), 1974, 117-141.
• [6] Clarke, E., Grumberg, O., Peled, D.: Model checking, The MIT Press, 1999.
• [7] 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), 1992, 275-288.
• [8] Couvreur, J.-M.: On-the-fly verification of linear temporal logic, Proceedings of the FM'99 World Congress on FormalMethods in the Development of Computing Systems, Volume I (J.M.Wing, J.Woodcock, J. Davies, Eds.), LNCS 1708, Springer-Verlag, 1999.
• [9] Daniele, M., Giunchiglia, F., Vardi, M. Y.: Improved automata generation for linear temporal logic, Proceedings of the 11th International Conference on Computer Aided Verification (CAV 1999), LNCS 1633, Springer-Verlag, 1999.
• [10] Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols, International Journal on Software Tools for Technology Transfer (STTT), 5(2-3), 2004, 247-267.
• [11] Emerson, E. A., Sistla, A. P.: Deciding full branching time logic, Information and Control, 61(3), 1984, 175-201.
• [12] Francez, N.: Fairness, Texts and Monographs in Computer Science, Springer-Verlag, 1986.
• [13] Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in SPIN, Proceedings of the 11th International SPIN Workshop on Model Checking Software (SPIN 2004) (S. Graf, L. Mounier, Eds.), LNCS 2989, Springer-Verlag, 2004.
• [14] Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation, Proceedings of the 13th International Conference on Computer Aided Verification (CAV 2001) (G. Berry, H. Comon, A. Finkel, Eds.), LNCS 2102, Springer-Verlag, 2001.
• [15] Geldenhuys, J., Valmari, A.: Tarjan's algorithm makes on-the-fly LTL verification more efficient, Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) (K. Jensen, A. Podelski, Eds.), LNCS 2988, Springer-Verlag, 2004.
• [16] Gerth, R., Peled, D., Vardi, M. Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic, Proceedings of the 15th IFIP WG6.1 International Symposium on Protocol Specification, Testing, and Verification (PSTV 1995) (P. Dembinski, M. Sredniawa, Eds.), Chapman & Hall, 1995.
• [17] Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Büchi automata, Proceedings of the 22nd IFIP WG6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2002) (D. A. Peled, M. Y. Vardi, Eds.), LNCS 2529, Springer-Verlag, 2002.
• [18] Godefroid, P., Holzmann, G. J.: On the verification of temporal properties, Proceedings of the 13th IFIP TC6/WG6.1 International Symposium on Protocol Specification, Testing, and Verification (PSTV 1993) (A. A. S. Danthine, G. Leduc, P. Wolper, Eds.), North-Holland, 1993.
• [19] Godefroid, P., Holzmann, G. J., Pirottin, D.: State space caching revisited, FormalMethods in System Design, 7(3), 1995, 227-241.
• [20] Holzmann, G. J.: Design and validation of computer protocols, Prentice-Hall, 1991.
• [21] Holzmann, G. J., Peled, D., Yannakakis, M.: On nested depth first search, Proceedings of the Second Workshop on the SPIN Verification System (J.-C. Grégoire, G. J. Holzmann, D. A. Peled, Eds.), Volume 32 in DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, 1997.
• [22] Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications, Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP 1998) (K. G. Larsen, S. Skyum, G. Winskel, Eds.), LNCS 1443, Springer-Verlag, 1998.
• [23] Latvala, T., Heljanko, K.: Coping with strong fairness, Fundamenta Informaticae, 43(1-4), 2000, 175-193.
• [24] Pelánek, R.: Typical structural properties of state spaces, Proceedings of the 11th International SPIN Workshop on Model Checking Software (SPIN 2004) (S. Graf, L. Mounier, Eds.), LNCS 2989, Springer-Verlag, 2004.
• [25] Peled, D. A.: Combining partial order reductions with on-the-fly model checking, Formal Methods in System Design, 8(1), 1996, 39-64.
• [26] Rönkkö, M., Mäkelä, M., Tauriainen, H.: LBT: LTL to Büchi conversion, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Available on the World Wide Web at <http://tcs.hut.fi/Software/maria/tools/lbt>.
• [27] Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms, Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005) (N. Halbwachs, L. Zuck, Eds.), LNCS 3440, Springer-Verlag, 2005.
• [28] Stern, U., Dill, D.: A new scheme for memory-efficient probabilistic verification, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques and Protocol Specification, Testing and Verification (FORTE/PSTV 1996) (R. Gotzhein, J. Bredereke, Eds.), Kluwer, 1996.
• [29] Tarjan, R.: Depth-first search and linear graph algorithms, SIAMJournal on Computing, 1(2), 1972, 146-160.
• [30] Vardi, M. Y., Wolper, P.: An automata-theoretic approach to automatic program verification, Proceedings of the Symposium on Logic in Computer Science (LICS 1986), IEEE Computer Society Press, 1986.
• [31] Wang, C., Bloem, R., Hachtel, G. D., Somenzi, F.: Divide and compose: SCC refinement for language emptiness, Proceedings of the 12th International Conference on Concurrency Theory (CONCUR 2001), LNCS 2154, Springer-Verlag, 2001.
• [32] Wolper, P., Leroy, D.: Reliable hashing without collision detection, Proceedings of the 5th International Conference on Computer Aided Verification (CAV 1993) (C. Courcoubetis, Ed.), LNCS 697, Springer-Verlag, 1993.