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 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. It 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.
A fuller version appears in http://www.cs.technion.ac.il/users/orna/publications.html
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
Asteroth, A., Baier, C., Assmann, U.: Model checking with formula-dependent abstract models. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 155–168. Springer, Heidelberg (2001)
Barner, S., Geist, D., Gringauze, A.: Symbolic localization reduction with reconstruction layering and backtracking. In: Computer Aided Verification (2002)
Bollig, B., Leucker, M., Weber, M.: Local parallel model checking for the alternation-free mu-calculus. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, p. 128. Springer, Heidelberg (2002)
Chauhan, P., Clarke, E.M., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, Springer, Heidelberg (2002)
Clarke, E., Grumberg, O., McMillan, K., Zhao, X.: Efficient generation of counterexamples and witnesses in symbolic model checking. In: DAC 1995, IEEE Computer Society Press, Los Alamitos (1995)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification. LNCS, Chicago, USA (July 2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Computer-Aided Verification (July 2002)
Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Seventeenth Annual IEEE Symposium on Logic In Computer Science (LICS) (July 2002)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: popl4, pp. 238–252 (1977)
Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems (TOPLAS) 19(2) (March 1997)
Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: FSTTCS (2001)
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 137–150. Springer, Heidelberg (2002)
Godefroid, P., Jagadeesan, R.: On the expressiveness of 3-valued models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2002)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 426. Springer, Heidelberg (2001)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)
Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM (JACM) 47(2), 312–360 (2000)
Kurshan, R.P.: Computer-Aided-Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210 (1988)
Lee, W., Pardo, A., Jang, J.-Y., Hachtel, G.D., Somenzi, F.: Tearing based automatic abstraction for CTL model checking. In: ICCAD, pp. 76–81 (1996)
Leucker, M.: Model checking games for the alternation free mu-calculus and alternating automata. In: Conf. on Logic for Programming and Automated Reasoning, LPAR (1999)
Lind-Nielsen, J., Andersen, H.R.: Stepwise CTL model checking of state/event systems. In: Computer Aided Verification, pp. 316–327 (1999)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design (1995)
Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 2. Springer, Heidelberg (2001)
Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 435–449. Springer, Heidelberg (2000)
Pardo, A., Hachtel, G.D.: Automatic abstraction techniques for propositional mu-calculus model checking. In: Computer Aided Verification, pp. 12–23 (1997)
Pardo, A., Hachtel, G.D.: Incremental CTL model checking using BDD subsetting. In: Design Automation Conference (DAC), pp. 457–462 (1998)
Peled, D., Zuck, L.: From model checking to a temporal proof. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 1. Springer, Heidelberg (2001)
Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 443–454. Springer, Heidelberg (1999)
Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)
Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 455. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shoham, S., Grumberg, O. (2003). A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement. In: Hunt, W.A., Somenzi, F. (eds) Computer Aided Verification. CAV 2003. Lecture Notes in Computer Science, vol 2725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45069-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive