Abstract
We present an algorithm that constructs a finite state “abstract” program from a given, possibly infinite state, “concrete” program by means of a syntactic program transformation. Starting with an initial set of predicates from a specification, the algorithm iteratively computes the predicates required for the abstraction relative to that specification. These predicates are represented by boolean variables in the abstract program. We show that the method is sound, in that the abstract program is always guaranteed to simulate the original. We also show that the method is complete, in that, if the concrete program has a finite abstraction with respect to simulation (bisimulation) equivalence, the algorithm can produce a finite simulation-equivalent (bisimulation-equivalent) abstract program. Syntactic abstraction has two key advantages: it can be applied to infinite state programs or programs with large data paths, and it permits the effective application of other reduction methods for model checking. We show that our method generalizes several known algorithms for analyzing syntactically restricted, data-insensitive programs.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Browne, M.C., Clarke, E.M., Grümberg, O.: Characterizing finite Kripke structures in Propositional Temporal Logic. Theoretical Computer Science 59 (1988)
Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First- order-CTL model checking. In: Arvind, V., Sarukkai, S. (eds.) FST TCS 1998. LNCS, vol. 1530. Springer, Heidelberg (1998)
Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663. Springer, Heidelberg (1993); Full version in Science of Computer Programming 18 (1992)
Bultan, T., Gerber, R., Pugh, W.: Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Chan, W., Anderson, R., Beame, P., Notkin, D.: Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logics of Programs. LNCS, vol. 131. Springer, Hidelberg (1981)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic. TOPLAS 8(2) (1986)
Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. TOPLAS (1994)
Colon, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Dams, D., Gerth, R., Grumberg, O.: Generation of reduced models for checking fragments of CTL. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Dijkstra, E.W.: Guarded commands, nondeterminacy, and formal deriva- tion of programs. C. ACM 18 (1975)
Emerson, E.A., Halpern, J.: “Sometimes” and “Not Never” revisited: On branching versus linear time temporal logic. J. ACM 33 (1986)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS (1986)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–157. Springer, Heidelberg (1999)
Grumberg, O., Long, D.: Model checking and modular verification. TOPLAS 16 (1994)
German, S., Sistla, A.P.: Reasoning about systems with many processes. J. ACM (1992)
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Hojati, R., Brayton, R.K.: Automatic datapath abstraction of hardware systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939. Springer, Heidelberg (1995)
Hungar, H., Grumberg, O., Damm, W.: What if model checking must be truly symbolic. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987. Springer, Heidelberg (1995)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: IEEE FOCS (1995)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design (1996)
Keller, R.M.: Formal verification of parallel programs. C. ACM (1976)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation, Earlier version at MFCS, published in LNCS 1450 (2000) (to appear)
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. C. ACM (August 1974)
Lazić, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University (1999)
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)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104. Springer, Heidelberg (1981)
Pnueli, A.: The temporal logic of programs. In: FOCS (1977)
Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding equality formulas by small domains instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 455–469. Springer, Heidelberg (1999)
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137. Springer, Heidelberg (1982)
Sajid, K., Goel, A., Zhou, H., Aziz, A., Barber, S., Singhal, V.: Bdd- based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Sipma, H., Uribe, T., Manna, Z.: Deductive model checking. CAV 1996 15 (1999); Earlier version at Alur, R., Henzinger, T.A. (eds.): CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)
Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: POPL (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Namjoshi, K.S., Kurshan, R.P. (2000). Syntactic Program Transformations for Automatic Abstraction. In: Emerson, E.A., Sistla, A.P. (eds) Computer Aided Verification. CAV 2000. Lecture Notes in Computer Science, vol 1855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722167_33
Download citation
DOI: https://doi.org/10.1007/10722167_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67770-3
Online ISBN: 978-3-540-45047-4
eBook Packages: Springer Book Archive