Abstract
The core challenge in a Hoare- or Dijkstra-style proof system for graph programs is in defining a weakest liberal precondition construction with respect to a rule and a postcondition. Previous work addressing this has focused on assertion languages for first-order properties, which are unable to express important global properties of graphs such as acyclicity, connectedness, or existence of paths. In this paper, we extend the nested graph conditions of Habel, Pennemann, and Rensink to make them equivalently expressive to monadic second-order logic on graphs. We present a weakest liberal precondition construction for these assertions, and demonstrate its use in verifying non-local correctness specifications of graph programs in the sense of Habel et al.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Habel, A., Pennemann, K.-H., Rensink, A.: Weakest preconditions for high-level programs. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 445–460. Springer, Heidelberg (2006)
Pennemann, K.H.: Development of Correct Graph Transformation Systems. Doctoral dissertation, Universität Oldenburg (2009)
Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science 19(2), 245–296 (2009)
Poskitt, C.M., Plump, D.: Hoare-style verification of graph programs. Fundamenta Informaticae 118(1-2), 135–175 (2012)
Poskitt, C.M.: Verification of Graph Programs. PhD thesis, University of York (2013)
Plump, D.: The design of GP 2. In: Escobar, S. (ed.) WRS 2011. EPTCS, vol. 82, pp. 1–16 (2012)
Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press (2012)
Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs: Extended version (2014), http://arxiv.org/abs/1405.5927
Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer (2006)
Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation 85(1), 12–75 (1990)
Courcelle, B.: Graph rewriting: An algebraic and logic approach. In: Handbook of Theoretical Computer Science, vol. B. Elsevier (1990)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)
Poskitt, C.M., Plump, D.: Verifying total correctness of graph programs. In: Echahed, R., Habel, A., Mosbah, M. (eds.) GCM 2012. Electronic Communications of the EASST, vol. 61 (2013)
Habel, A., Radke, H.: Expressiveness of graph conditions with variables. In: Ermel, C., Ehrig, H., Orejas, F., Taentzer, G. (eds.) GraMoT 2010. Electronic Communications of the EASST, vol. 30 (2010)
Radke, H.: HR* graph conditions between counting monadic second-order and second-order graph formulas. In: Echahed, R., Habel, A., Mosbah, M. (eds.) GCM 2012. Electronic Communications of the EASST, vol. 61 (2013)
Percebois, C., Strecker, M., Tran, H.N.: Rule-level verification of graph transformations for invariants based on edges’ transitive closure. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 106–121. Springer, Heidelberg (2013)
Inaba, K., Hidaka, S., Hu, Z., Kato, H., Nakano, K.: Graph-transformation verification using monadic second-order logic. In: Schneider-Kamp, P., Hanus, M. (eds.) PPDP 2011, pp. 17–28. ACM (2011)
Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. Software Tools for Technology Transfer 14(1), 15–40 (2012)
König, B., Kozioura, V.: Augur 2 - a new version of a tool for the analysis of graph transformation systems. In: Bruni, R., Varró, D. (eds.) GT-VMT 2006. ENTCS, vol. 211, pp. 201–210 (2008)
Pennemann, K.H.: Resolution-like theorem proving for high-level conditions. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 289–304. Springer, Heidelberg (2008)
Lambers, L., Orejas, F.: Tableau-based reasoning for graph properties. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 17–32. Springer, Heidelberg (2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Poskitt, C.M., Plump, D. (2014). Verifying Monadic Second-Order Properties of Graph Programs. In: Giese, H., König, B. (eds) Graph Transformation. ICGT 2014. Lecture Notes in Computer Science, vol 8571. Springer, Cham. https://doi.org/10.1007/978-3-319-09108-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-09108-2_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09107-5
Online ISBN: 978-3-319-09108-2
eBook Packages: Computer ScienceComputer Science (R0)