Abstract
Effective program abstraction is needed to successfully apply model checking in practice. This paper studies the question of constructing abstractions that preserve branching time properties. The key challenge is to simultaneously preserve the existential and universal aspects of a property, without relying on bisimulation. To achieve this, our method abstracts an alternating transition system (ATS) formed by the product of a program with an alternating tree automaton for a property. The AND-OR distinction in the ATS is used to guide the abstraction, weakening the transition relation at AND states, and strengthening it at OR states. We show semantic completeness: i.e., whenever a program satisfies a property, this can be shown using a finite-state abstract ATS produced by the method. To achieve completeness, the method requires choice predicates that help resolve nondeterminism at OR states, and rank functions that help preserve progress properties. Specializing this result to predicate abstraction, we obtain exact characterizations of the types of properties provable with these methods.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, p. 23. Springer, Heidelberg (1998); Journal version in JACM
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 260. Springer, Heidelberg (2001)
Bensalem, S., Lakhnech, Y., Owre, S.: InVeST: A tool for the verification of invariants. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531. Springer, Heidelberg (1990)
Browne, I.A., Manna, Z., Sipma, H.B.: Generalized temporal verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026. Springer, Heidelberg (1995)
Bruns, G., Godefroid, P.: Generalized model checking: Reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 168. Springer, Heidelberg (2000)
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., Long, D.E.: Model checking and abstraction. TOPLAS 16(5) (1994)
Cleaveland, R., Iyer, S.P., Yankelevich, D.: Optimality in abstractions of model checking. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983. Springer, Heidelberg (1995)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE (2001)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1997)
Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology (1996)
Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. TOPLAS 19(2) (1997)
Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM 18(8) (1975)
Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model-checking for fragments of μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: FOCS (1991)
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., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal 5(2) (2000)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163(1) (2000)
Kesten, Y., Pnueli, A., Vardi, M.: Verification by augmented abstraction: The automata-theoretic view. JCSS 62(4) (2001)
Kozen, D.: Results on the propositional mu-calculus. In: ICALP (1982)
Lee, D., Yannakakis, M.: Online minimization of transition systems. In: STOC (1992)
Milner, R.: An algebraic definition of simulation between programs. In: 2nd IJCAI (1971)
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.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 174–188. Springer, Heidelberg (2002)
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. Springer, Heidelberg (2000)
Sipma, H.B., Uribe, T.E., Manna, Z.: Deductive model checking. Formal Methods in System Design 15(1) (1999)
Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, Springer, Heidelberg (1984); Full version in Inf. and Comp. 81(3), 249-264 (1989)
Uribe, T.E.: Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University (1999)
Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: ICSE (2000)
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
Namjoshi, K.S. (2003). Abstraction for Branching Time Properties. 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_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-45069-6_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40524-5
Online ISBN: 978-3-540-45069-6
eBook Packages: Springer Book Archive