
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Antonella Santone, "Heuristic Search + Local Model Checking in Selective muCalculus," IEEE Transactions on Software Engineering, vol. 29, no. 6, pp. 510523, June, 2003.  
BibTex  x  
@article{ 10.1109/TSE.2003.1205179, author = {Antonella Santone}, title = {Heuristic Search + Local Model Checking in Selective muCalculus}, journal ={IEEE Transactions on Software Engineering}, volume = {29}, number = {6}, issn = {00985589}, year = {2003}, pages = {510523}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2003.1205179}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Heuristic Search + Local Model Checking in Selective muCalculus IS  6 SN  00985589 SP510 EP523 EPD  510523 A1  Antonella Santone, PY  2003 KW  State explosion KW  model checking KW  heuristic search KW  temporal logic KW  local model checking KW  AND/OR graph. VL  29 JA  IEEE Transactions on Software Engineering ER   
Abstract—Many tools for the automatic analysis or verification of finitestate distributed systems are based on the construction of the global state graph of the system under consideration. Thus, they often fail because of the
[1] R. Alur and B.Y. Wang, Next Heuristic for OntheFly Model Checking Proc. 10th Int'l Conf. Concurrency Theory (CONCUR '99), pp. 98113, 1999.
[2] A. Aziz, T.R. Shiple, V. Singhal, and A.L. SangiovanniVincentelli, FormulaDependent Equivalence for Compositional CTL Model Checking Proc. Sixth Int'l Conf. ComputerAided Verification (CAV '94), pp. 324337, 1994.
[3] R. Barbuti, N. De Francesco, A. Santone, and G. Vaglini, Selective mucalculus and FormulaBased Abstractions of Transition Systems J. Computer and System Sciences, vol. 59, no. 3, pp. 537556, 1999.
[4] G. Behrmann, A. Fehnker, T.S. Hune, K. Larsen, P. Petterson, and J. Romijn, Efficient Guiding Towards CostOptimality in UPPAAL Proc. Seventh Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '01), pp. 174188, 2001.
[5] P. Bertoli, A. Cimatti, J. Slaney, and S. Thiebaux, Solving Power Supply Restoration Problems with Planning via Symbolic ModelChecking Proc. Sixth Int'l Conf. AI Planning and Scheduling (AIPS '02), pp. 2329, 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. ComputerAided Verification (CAV '99), pp. 222235, 1999.
[7] A. Bouajjani, J.C. Fernandez, and N. Halbwachs, Minimal Model Generation Proc. Int'l Conf. ComputerAided Verification (CAV '90), pp. 197203, 1990.
[8] J.C. Bradfield and C. Stirling, Local Model Checking for Infinite State Spaces Theoretical Computer Science, vol. 96, no. 1, pp. 157174, 1992.
[9] R.E. Bryant, GraphBased Algorithms for Boolean Function Manipulation IEEE Trans. Computers, vol. 35, no. 8, pp. 677691, 1986.
[10] E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic Verification of Finitestate Concurrent Systems using Temporal Logic Verification ACM Trans. Programming Languages and Systems, vol. 8, pp. 244263, 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. 15121542, 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. ComputerAided Verification (CAV '96), pp. 394397, 1996.
[14] N. De Francesco, A. Santone, and G. Vaglini, State Space Reduction by NonStandard Semantics for Deadlock Analysis Science of Computer Programming, vol. 30, no. 3, pp. 309338, 1998.
[15] S. Edelkamp and F. Reffel, OBDDs in Heuristic Search Proc. 22nd Ann. German Conf. Artificial Intelligence (KI '98), pp. 8192, 1998.
[16] S. Edelkamp, A. LluchLafuente, and S. Leue, Directed Explicit Model Checking with HSFSPIN Proc. Eighth Int'l SPIN Workshop Model Checking Software, pp. 5779, 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. 455460, 2002.
[19] P. Godefroid, PartialOrder 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. 266280, 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. 607616, 1996.
[22] A. Groce and W. Visser, Heuristic Model Checking for Java Programs Proc. Ninth Int'l SPIN Workshop (SPIN '02), pp. 242245, 2002.
[23] O. Grumberg and D.E. Long, Model Checking and Modular Verification ACM Trans. Programming Languages and Systems, vol. 16, no. 3, pp. 843871, 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 BDDBased Heuristic Search Algorithm Proc. 18th Nat'l Conf. Artificial Intelligence and 14th Conf. Innovative Applications of Artificial Intelligence (AAAI/IAAI '02), pp. 668673, 2002.
[26] R. Kaivola, Compositional Model Checking for LinearTime Temporal Logic Proc. Fourth Int'l Conf. ComputerAided Verification (CAV '92), pp. 248259, 1991.
[27] A. LluchLafuente, S. Edelkamp, and S. Leue, Partial Order Reduction in Directed Model Checking Proc. Ninth Int'l SPIN Workshop Model Checking Software, pp. 112127, 2002.
[28] A. Mahanti and A. Bagchi, AND/OR Graph Heuristic Search Methods J. ACM, vol. 32, no. 1, pp. 2851, 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. PrenticeHall, 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. 7185, 2001.
[33] J. Pearl, Heuristics: Intelligent Search Strategies for Computer Problem Solving. AddisonWesley, Jan. 1984.
[34] D. Peled, All from One, One for All, on ModelChecking Using Representatives Proc. Fifth Int'l Conf. ComputerAided Verification (CAV '93), pp. 409423, 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 FormulaBased Compositional Approach Acta Informatica, vol. 38, no. 8, pp. 531564, 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 MuCalculus Theoretical Computer Science, vol. 89, pp. 161177, 1991.
[39] A. Valmari, A Stubborn Attack on State Explosion Proc. Second Int'l Conf. ComputerAided Verification (CAV '90), pp. 156165, 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. 599604, 1998.