A game-based framework for CTL counterexamples and 3-valued abstraction-refinement

ABSTRACT

This work exploits and extends the game-based framework of CTL model checking for counterexample and incremental abstraction-refinement. We define a game-based CTL model checking for abstract models over the 3-valued semantics, which can be used for verification as well as refutation. The model checking process of an abstract model may end with an indefinite result, in which case we suggest a new notion of refinement, which eliminates indefinite results of the model checking. This provides an iterative abstraction-refinement framework. This framework is enhanced by an incremental algorithm, where refinement is applied only where indefinite results exist and definite results from prior iterations are used within the model checking algorithm. We also define the notion of annotated counterexamples, which are sufficient and minimal counterexamples for full CTL. We present an algorithm that uses the game board of the model checking game to derive an annotated counterexample in case the examined system model refutes the checked formula.

REFERENCES

• 1: Alexander Asteroth , Christel Baier , Ulrich Aßmann, Model Checking with Formula-Dependent Abstract Models, Proceedings of the 13th International Conference on Computer Aided Verification, p.155-168, July 18-22, 2001
• 2: Sharon Barner , Daniel Geist , Anna Gringauze, Symbolic Localization Reduction with Reconstruction Layering and Backtracking, Proceedings of the 14th International Conference on Computer Aided Verification, p.65-77, July 27-31, 2002
• 3: Benedikt Bollig , Martin Leucker , Michael Weber, Local Parallel Model Checking for the Alternation-Free µ-Calculus, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.128-147, April 11-13, 2002
• 4: Glenn Bruns , Patrice Godefroid, Model Checking Partial State Spaces with 3-Valued Temporal Logics, Proceedings of the 11th International Conference on Computer Aided Verification, p.274-287, July 06-10, 1999
• 5: Glenn Bruns , Patrice Godefroid, Generalized Model Checking: Reasoning about Partial State Spaces, Proceedings of the 11th International Conference on Concurrency Theory, p.168-182, August 22-25, 2000
• 6: Pankaj Chauhan , Edmund M. Clarke , James H. Kukula , Samir Sapra , Helmut Veith , Dong Wang, Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.33-51, November 06-08, 2002
• 7: Marsha Chechik , Benet Devereux , Steve Easterbrook, Implementing a Multi-valued Symbolic Model Checker, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.404-419, April 02-06, 2001
• 8: Marsha Chechik , Arie Gurfinkel , Benet Devereux, chi-Chek: A Multi-valued Model-Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.505-509, July 27-31, 2002
• 9: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 10: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 11: E. M. Clarke , O. Grumberg , K. L. McMillan , X. Zhao, Efficient generation of counterexamples and witnesses in symbolic model checking, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.427-432, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217565]
• 12: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 13: Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Shrichman, SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques, Proceedings of the 14th International Conference on Computer Aided Verification, p.265-279, July 27-31, 2002
• 14: Edmund M. Clarke , Somesh Jha , Yuan Lu , Helmut Veith, Tree-Like Counterexamples in Model Checking, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.19-29, July 22-25, 2002
• 15: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 16: Dennis Dams , Rob Gerth , Orna Grumberg, Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.253-291, March 1997 [doi>10.1145/244795.244800]
• 17: Satyaki Das , David L. Dill , Seungjoon Park, Experience with Predicate Abstraction, Proceedings of the 11th International Conference on Computer Aided Verification, p.160-171, July 06-10, 1999
• 18: Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., and Campenhout, D. V. 2003. Reasoning with temporal logic on truncated paths. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 2725. Springer, 27--39.
• 19: Emerson, E. and Clarke, E. 1982. Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241--266.
• 20: Patrice Godefroid , Michael Huth , Radha Jagadeesan, Abstraction-Based Model Checking Using Modal Transition Systems, Proceedings of the 12th International Conference on Concurrency Theory, p.426-440, August 20-25, 2001
• 21: Patrice Godefroid , Radha Jagadeesan, Automatic Abstraction Using Generalized Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.137-150, July 27-31, 2002
• 22: Patrice Godefroid , Radha Jagadeesan, On the Expressiveness of 3-Valued Models, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.206-222, January 09-11, 2002
• 23: Shankar G. Govindaraju , David L. Dill, Verification by approximate forward and backward reachability, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.366-370, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289055]
• 24: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 25: Gurfinkel, A. and Chechik, M. 2003a. Generating counterexamples for multivalued model-checking. In Proceedings of the IEEE International Symposium on Formal Methods Europe (FME'03). 503--521.
• 26: Gurfinkel, A. and Chechik, M. 2003b. Proof-like counter-examples. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03).
• 27: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 28: Michael Huth , Radha Jagadeesan , David A. Schmidt, Modal Transition Systems: A Foundation for Three-Valued Program Analysis, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.155-169, April 02-06, 2001
• 29: Orna Kupferman , Moshe Y. Vardi , Pierre Wolper, An automata-theoretic approach to branching-time model checking, Journal of the ACM (JACM), v.47 n.2, p.312-360, March 2000 [doi>10.1145/333979.333987]
• 30: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 31: Larsen, K. and Thomsen, B. 1988. A modal process logic. In Proceedings of 3rd Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 203--210.
• 32: K. G. Larsen, Modal specifications, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.232-246, February 1990, Grenoble, France
• 33: Woohyuk Lee , Abelardo Pardo , Jae-Young Jang , Gary Hachtel , Fabio Somenzi, Tearing based automatic abstraction for CTL model checking, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.76-81, November 10-14, 1996, San Jose, California, United States
• 34: Martin Leucker, Model Checking Games for the Alternation-Free µ-Calculus and Alternating Automata, Proceedings of the 6th International Conference on Logic Programming and Automated Reasoning, p.77-91, September 06-10, 1999
• 35: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 36: Jørn Lind-Nielsen , Henrik Reif Andersen, Stepwise CTL Model Checking of State/Event Systems, Proceedings of the 11th International Conference on Computer Aided Verification, p.316-327, July 06-10, 1999
• 37: C. Loiseaux , S. Graf , J. Sifakis , A. Bouajjani , S. Bensalem, Property preserving abstractions for the verification of concurrent systems, Formal Methods in System Design, v.6 n.1, p.11-44, Jan. 1995 [doi>10.1007/BF01384313]
• 38: Kedar S. Namjoshi, Certifying Model Checkers, Proceedings of the 13th International Conference on Computer Aided Verification, p.2-13, July 18-22, 2001
• 39: Kedar S. Namjoshi , Robert P. Kurshan, Syntactic Program Transformations for Automatic Abstraction, Proceedings of the 12th International Conference on Computer Aided Verification, p.435-449, July 15-19, 2000
• 40: Abelardo Pardo , Gary D. Hachtel, Automatic Abstraction Techniques for Propositional µ-calculus Model Checking, Proceedings of the 9th International Conference on Computer Aided Verification, p.12-23, June 22-25, 1997
• 41: Abelardo Pardo , Gary D. Hachtel, Incremental CTL model checking using BDD subsetting, Proceedings of the 35th annual conference on Design automation, p.457-462, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277171]
• 42: Jean-Pierre Queille , Joseph Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, p.337-351, April 06-08, 1982
• 43: Hassen Saïdi, Model Checking Guided Abstraction and Analysis, Proceedings of the 7th International Symposium on Static Analysis, p.377-396, June 29-July 01, 2000
• 44: Hassen Saïdi , Natarajan Shankar, Abstract and Model Check While You Prove, Proceedings of the 11th International Conference on Computer Aided Verification, p.443-454, July 06-10, 1999
• 45: Shoham, S. 2003. A game-based framework for CTL counterexamples and abstraction-refinement. M.S. thesis, Department of Computer Science, Technion---Israel Institute of Technology.
• 46: Colin Stirling, Modal and temporal properties of processes, Springer-Verlag New York, Inc., New York, NY, 2001
• 47: Li Tan , Rance Cleaveland, Evidence-Based Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.455-470, July 27-31, 2002

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Algorithms, Verification

Keywords:
3-valued semantics, Abstraction-Refinement, CTL, Counterexamples, Model checking games, Temporal logic