Abstract
We show that the model checking problem of the μ-calculus can be viewed as an instance of static analysis. We propose Succinct Fixed Point Logic (SFP) within our logical approach to static analysis as an extension of Alternation-free Least Fixed Logic (ALFP). We generalize the notion of stratification to weak stratification and establish a Moore Family result for the new logic as well. The semantics of the μ-calculus is encoded as the intended model of weakly stratified clause sequences in SFP.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Emerson, E.A., Lei, C.-L.: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). In: LICS 1986, pp. 267–278 (1986)
Cleaveland, R., Steffen, B.: A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. Formal Methods in System Design 2(2), 121–147 (1993)
Andersen, H.R.: Model Checking and Boolean Graphs. Theor. Comput. Sci. 126(1), 3–30 (1994)
Baier, C., Katoen, J.-P.: Principles of model checking, pp. I-XVII, 1-975. MIT Press (2008)
Kozen, D.: Results on the Propositional mu-Calculus. Theor. Comput. Sci. 27, 333–354 (1983)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis (2. corr. print), pp. I-XXI, 1-452. Springer (2005)
Nielson, H.R., 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)
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)
Steffen, B.: Generating Data Flow Analysis Algorithms from Modal Specifications. Sci. Comput. Program. 21(2), 115–139 (1993)
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)
Schmidt, D.A.: Data Flow Analysis is Model Checking of Abstract Interpretations. In: POPL 1998, pp. 38–48 (1998)
Nielson, F., Nielson, H.R.: Model Checking Is Static Analysis of Modal Logic. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 191–205. Springer, Heidelberg (2010)
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., Seidl, H., Nielson, H.R.: A Succinct Solver for ALFP. Nord. J. Comput. 9(4), 335–372 (2002)
Nielson, F.: Two-Level Semantics and Abstract Interpretation. Theor. Comput. Sci. 69(2), 117–242 (1989)
Filipiuk, P., Nielson, H.R., Nielson, F.: Explicit Versus Symbolic Algorithms for Solving ALFP Constraints. Electr. Notes Theor. Comput. Sci. 267(2), 15–28 (2010)
Nielson, H.R., Nielson, F., Pilegaard, H.: Flow Logic for Process Calculi. ACM Comput. Surv. 44(1), 3 (2012)
Apt, K.R., Blair, H.A., Walker, A.: Towards a Theory of Declarative Knowledge. In: Foundations of Deductive Databases and Logic Programming, pp. 89–148 (1988)
Chandra, A.K., Harel, D.: Computable Queries for Relational Data Bases. J. Comput. Syst. Sci. 21(2), 156–178 (1980)
Zhang, F., Nielson, F., Nielson, H.R.: Fixpoints vs. Moore Families. Student Research Forum at SOFSEM 2012 (2012)
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient Model Checking Using Tabled Resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 143–154. Springer, Heidelberg (1997)
Ramakrishnan, C.R.: A Model Checker for Value-Passing Mu-Calculus Using Logic Programming. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 1–13. Springer, Heidelberg (2001)
Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Dong, Y., Du, X., Roychoudhury, A., Venkatakrishnan, V.N.: XMC: A Logic-Programming-Based Verification Toolset. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 576–580. Springer, Heidelberg (2000)
Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 223–239. Springer, Heidelberg (1999)
Delzanno, G., Podelski, A.: Constraint-based deductive model checking. STTT 3(3), 250–270 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, F., Nielson, F., Nielson, H.R. (2012). Model Checking as Static Analysis: Revisited. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds) Integrated Formal Methods. IFM 2012. Lecture Notes in Computer Science, vol 7321. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30729-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-30729-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30728-7
Online ISBN: 978-3-642-30729-4
eBook Packages: Computer ScienceComputer Science (R0)