This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Heuristic Search + Local Model Checking in Selective mu-Calculus
June 2003 (vol. 29 no. 6)
pp. 510-523

Abstract—Many tools for the automatic analysis or verification of finite-state distributed systems are based on the construction of the global state graph of the system under consideration. Thus, they often fail because of the state explosion problem: The state space of a distributed system potentially increases exponentially in the number of its parallel components. To overcome this problem in this paper, we present a model checking procedure, based on the combination of heuristic searches with ideas taken from local model checking. We use heuristic mechanisms for the exploration of the search space in order to avoid the construction of the complete state graph.

[1] R. Alur and B.-Y. Wang, Next Heuristic for On-the-Fly Model Checking Proc. 10th Int'l Conf. Concurrency Theory (CONCUR '99), pp. 98-113, 1999.
[2] A. Aziz, T.R. Shiple, V. Singhal, and A.L. Sangiovanni-Vincentelli, Formula-Dependent Equivalence for Compositional CTL Model Checking Proc. Sixth Int'l Conf. Computer-Aided Verification (CAV '94), pp. 324-337, 1994.
[3] R. Barbuti, N. De Francesco, A. Santone, and G. Vaglini, Selective mu-calculus and Formula-Based Abstractions of Transition Systems J. Computer and System Sciences, vol. 59, no. 3, pp. 537-556, 1999.
[4] G. Behrmann, A. Fehnker, T.S. Hune, K. Larsen, P. Petterson, and J. Romijn, Efficient Guiding Towards Cost-Optimality in UPPAAL Proc. Seventh Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '01), pp. 174-188, 2001.
[5] P. Bertoli, A. Cimatti, J. Slaney, and S. Thiebaux, Solving Power Supply Restoration Problems with Planning via Symbolic Model-Checking Proc. Sixth Int'l Conf. AI Planning and Scheduling (AIPS '02), pp. 23-29, 2002.
[6] R. Bloem, K. Ravi, and F. Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties Proc. 11th Int'l Conf. Computer-Aided Verification (CAV '99), pp. 222-235, 1999.
[7] A. Bouajjani, J.C. Fernandez, and N. Halbwachs, Minimal Model Generation Proc. Int'l Conf. Computer-Aided Verification (CAV '90), pp. 197-203, 1990.
[8] J.C. Bradfield and C. Stirling, Local Model Checking for Infinite State Spaces Theoretical Computer Science, vol. 96, no. 1, pp. 157-174, 1992.
[9] R.E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation IEEE Trans. Computers, vol. 35, no. 8, pp. 677-691, 1986.
[10] E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic Verification of Finite-state Concurrent Systems using Temporal Logic Verification ACM Trans. Programming Languages and Systems, vol. 8, pp. 244-263, 1986.
[11] E.M. Clarke, O. Grumberg, and D.E. Long, Model Checking and Abstraction ACM Trans. Programming Languages and Systems, vol. 16, no. 5, pp. 1512-1542, 1994.
[12] E.M. Clarke, D.E. Long, and K.L. McMillan, “Compositional Model Checking,” Proc. Fourth Ann. Symp. Logic in Computer Science, June 1989.
[13] R. Cleaveland and S. Sims, The NCSU Concurrency Workbench Proc. Eighth Int'l Conf. Computer-Aided Verification (CAV '96), pp. 394-397, 1996.
[14] N. De Francesco, A. Santone, and G. Vaglini, State Space Reduction by Non-Standard Semantics for Deadlock Analysis Science of Computer Programming, vol. 30, no. 3, pp. 309-338, 1998.
[15] S. Edelkamp and F. Reffel, OBDDs in Heuristic Search Proc. 22nd Ann. German Conf. Artificial Intelligence (KI '98), pp. 81-92, 1998.
[16] S. Edelkamp, A. Lluch-Lafuente, and S. Leue, Directed Explicit Model Checking with HSF-SPIN Proc. Eighth Int'l SPIN Workshop Model Checking Software, pp. 57-79, 2001.
[17] S. Edelkamp, Symbolic Pattern Databases in Heuristic Search Planning Proc. Sixth Int'l Conf. AI Planning and Scheduling (AIPS '02), 2002.
[18] Z. Feng and E. Hansen, Symbolic Heuristic Search for Factored Markov Decision Processes Proc. 18th Nat'l Conf. Artificial Intelligence (AAAI '02), pp. 455-460, 2002.
[19] P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems Springer Verlag, Mar. 1996.
[20] P. Godefroid and S. Khurshid, Exploring Very Large State Spaces Using Genetic Algorithms Proc. Eighth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '02), pp. 266-280, 2002.
[21] S. Graf, B. Steffen, and G. Luttgen, Compositional Minimization of Finite State Systems Using Interface Specifications Formal Aspects of Computing, vol. 8, no. 5, pp. 607-616, 1996.
[22] A. Groce and W. Visser, Heuristic Model Checking for Java Programs Proc. Ninth Int'l SPIN Workshop (SPIN '02), pp. 242-245, 2002.
[23] O. Grumberg and D.E. Long, Model Checking and Modular Verification ACM Trans. Programming Languages and Systems, vol. 16, no. 3, pp. 843-871, 1994.
[24] Handbook of Automated Reasoning. J.A. Robinson and A. Voronkov, eds., Elsevier and MIT Press, 2001.
[25] R.M. Jensen, R.E. Bryant, and M.M. Veloso, SetA*: An Efficient BDD-Based Heuristic Search Algorithm Proc. 18th Nat'l Conf. Artificial Intelligence and 14th Conf. Innovative Applications of Artificial Intelligence (AAAI/IAAI '02), pp. 668-673, 2002.
[26] R. Kaivola, Compositional Model Checking for Linear-Time Temporal Logic Proc. Fourth Int'l Conf. Computer-Aided Verification (CAV '92), pp. 248-259, 1991.
[27] A. Lluch-Lafuente, S. Edelkamp, and S. Leue, Partial Order Reduction in Directed Model Checking Proc. Ninth Int'l SPIN Workshop Model Checking Software, pp. 112-127, 2002.
[28] A. Mahanti and A. Bagchi, AND/OR Graph Heuristic Search Methods J. ACM, vol. 32, no. 1, pp. 28-51, 1985.
[29] B. Beizer, Software Testing Techniques. Int'l Thomson Computer Press, 1990.
[30] K. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[31] R. Milner, Communication and Concurrency. Prentice-Hall, 1989.
[32] M.O. Moller and R. Alur, Heuristics for Hierarchical Partitioning with Application to Model Checking Proc. 11th IFIP WG 10. 5, Advanced Research Working Conf. Correct Hardware Design and Verification Methods (CHARME '01), pp. 71-85, 2001.
[33] J. Pearl, Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, Jan. 1984.
[34] D. Peled, All from One, One for All, on Model-Checking Using Representatives Proc. Fifth Int'l Conf. Computer-Aided Verification (CAV '93), pp. 409-423, 1993.
[35] A. Pnueli, In Transition for Global to Modular Temporal Reasoning about Programs Logics and Models of Concurrent Systems, NATO ASI Series. Series F, Computer and System Sciences, vol. 13, 1984.
[36] A. Santone, Automatic Verification of Concurrent Systems using a Formula-Based Compositional Approach Acta Informatica, vol. 38, no. 8, pp. 531-564, 2002.
[37] C. Stirling, An Introduction to Modal and Temporal Logics for CCS Concurrency: Theory, Language, and Architecture, 1989.
[38] C. Stirling and D. Walker, Local Model Checking in the Modal Mu-Calculus Theoretical Computer Science, vol. 89, pp. 161-177, 1991.
[39] A. Valmari, A Stubborn Attack on State Explosion Proc. Second Int'l Conf. Computer-Aided Verification (CAV '90), pp. 156-165, 1990.
[40] C.H. Yang and D.L. Dill, Validation with Guided Search of the State Space Proc. 35th Conf. Design Automation (DAC '98), pp. 599-604, 1998.

Index Terms:
State explosion, model checking, heuristic search, temporal logic, local model checking, AND/OR graph.
Citation:
Antonella Santone, "Heuristic Search + Local Model Checking in Selective mu-Calculus," IEEE Transactions on Software Engineering, vol. 29, no. 6, pp. 510-523, June 2003, doi:10.1109/TSE.2003.1205179
Usage of this product signifies your acceptance of the Terms of Use.