Abstract
Flow Logic is an approach to the static analysis of programs that has been developed for functional, imperative and object-oriented programming languages and for concurrent, distributed, mobile and cryptographic process calculi. In this paper we extend it to deal with modal logics and prove that it can give an exact characterisation of the semantics of formulae in a modal logic. This shows that model checking can be performed by means of state-of-the-art approaches to static analysis and allow us to conclude that the problems of model checking and static analysis are reducible to each other. In terms of computational complexity we show that model checking by means of static analysis gives the same complexity bounds as are known for traditional approaches to model checking.
Download to read the full chapter text
Chapter PDF
References
Apt, K., Blair, H., Walker, A.: A theory of declarative programming. In: Foundations of Deductive Databases and Logic Programming, pp. 89–148. Morgan-Kaufman, San Francisco (1988)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Balbin, I., Ramamohanarao, K.: A generalization of the differential approach to recursive query evaluation. Journal of Logic Programming 4(3), 259–262 (1987)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Riis Nielson, H.: Static validation of security protocols. Journal of Computer Security 13, 347–390 (2005)
Chandra, A., Harel, D.: Computable queries for relational data bases. Journal of Computer and System Sciences 21(2), 156–178 (1980)
Le Charlier, B., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Technical report, CS-92-25, Brown University (1992)
Fecht, C., Seidl, H.: Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. Nordic Journal of Computing 5(4), 304–329 (1998)
Hankin, C., Nielson, F., Riis Nielson, H.: Advice from Belnap policies. In: Computer Security Foundations Symposium. IEEE Computer Society, Los Alamitos (2009)
Hecht, M.S.: Flow Analysis of Computer Programs. North Holland, Amsterdam (1977)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Lamprecht, A.-L., Margaria, T., Steffen, B.: Data-flow analysis as model checking within the jABC. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 101–104. Springer, Heidelberg (2006)
De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Nielson, F., Riis Nielson, H., Hankin, C.: Principles of Program Analysis, 2nd edn. Springer, Berlin (2005)
Nielson, F., Riis Nielson, H., Hansen, R.R.: Validating firewalls using flow logics. Theoretical Computer Science 283(2), 381–418 (2002)
Nielson, F., Riis Nielson, H., Seidl, H.: A succinct solver for ALFP. Nordic Journal of Computing 9, 335–372 (2002)
Nielson, F., Riis Nielson, H., Sun, H., Buchholtz, M., Hansen, R.R., Pilegaard, H., Seidl, H.: The Succinct Solver Suite. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 251–265. Springer, Heidelberg (2004)
Riis Nielson, H., Nielson, F.: Flow Logic: a multi-paradigmatic approach to static analysis. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 223–244. Springer, Heidelberg (2002)
Riis Nielson, H., Nielson, F., Pilegaard, H.: Spatial analysis of BioAmbients. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 69–83. Springer, Heidelberg (2004)
Paige, R.: Symbolic finite differencing - part i. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol. 432, pp. 36–56. Springer, Heidelberg (1990)
Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: POPL 1998, pp. 38–48 (1998)
Schmidt, D.A., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)
Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–365. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nielson, F., Nielson, H.R. (2010). Model Checking Is Static Analysis of Modal Logic. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)