Abstract
The goal of this work is to improve the efficiency and effectiveness of the abstraction-refinement framework for CTL over the 3-valued semantics. We start by proposing a symbolic (BDD-based) approach for this framework. Next, we generalize the definition of abstract models in order to provide a monotonic abstraction-refinement framework. To do so, we introduce the notion of hyper-transitions. For a given set of abstract states, this results in a more precise abstract model in which more CTL formulae can be proved or disproved.
We suggest an automatic construction of an initial abstract model and its successive refined models. We complete the framework by adjusting the BDD-based approach to the new monotonic framework. Thus, we obtain a monotonic, symbolic framework that is suitable for both verification and falsification of full CTL.
Chapter PDF
Similar content being viewed by others
References
Barner, S., Geist, D., Gringauze, A.: Symbolic localization reduction with reconstruction layering and backtracking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 65. 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)
Chechik, M., Devereux, B., Gurfinkel, A., Easterbrook, S.: Multi-valued symbolic modelchecking. Technical Report CSRG-448, University of Toronto (April 2002)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (December 1999)
Clarke, E.M., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction-refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 265. Springer, Heidelberg (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)
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)
Godefroid, P., Jagadeesan, R.: Automatic abstraction using generalized model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 137. 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)
Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for threevalued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001)
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 (July 1988)
Lee, W., Pardo, A., Jang, J., Hachtel, G.D., Somenzi, F.: Tearing based automatic abstraction for CTL model checking. In: ICCAD, pp. 76–81 (1996)
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.: Abstraction for branching time properties. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 288–300. Springer, Heidelberg (2003)
Pardo, A., Hachtel, G.D.: Automatic abstraction techniques for propositional mu-calculus model checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 12–23. Springer, Heidelberg (1997)
Pardo, A., Hachtel, G.D.: Incremental CTL model checking using BDD subsetting. In: Design Automation Conference, pp. 457–462 (1998)
Shoham, S., Grumberg, O.: A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 275–287. Springer, Heidelberg (2003)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. (1955)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shoham, S., Grumberg, O. (2004). Monotonic Abstraction-Refinement for CTL. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_40
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive
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.
