Skip to main content
SpringerLink
Log in

Verifying Monadic Second-Order Properties of Graph Programs

  • Conference paper
Book cover Graph Transformation (ICGT 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8571))

Included in the following conference series:

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. Pennemann, K.H.: Development of Correct Graph Transformation Systems. Doctoral dissertation, Universität Oldenburg (2009)

    Google Scholar 

  3. 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)

    Article  MATH  MathSciNet  Google Scholar 

  4. Poskitt, C.M., Plump, D.: Hoare-style verification of graph programs. Fundamenta Informaticae 118(1-2), 135–175 (2012)

    MATH  MathSciNet  Google Scholar 

  5. Poskitt, C.M.: Verification of Graph Programs. PhD thesis, University of York (2013)

    Google Scholar 

  6. Plump, D.: The design of GP 2. In: Escobar, S. (ed.) WRS 2011. EPTCS, vol. 82, pp. 1–16 (2012)

    Google Scholar 

  7. Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Cambridge University Press (2012)

    Google Scholar 

  8. Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs: Extended version (2014), http://arxiv.org/abs/1405.5927

  9. Flum, J., Grohe, M.: Parameterized Complexity Theory. Springer (2006)

    Google Scholar 

  10. Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation 85(1), 12–75 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  11. Courcelle, B.: Graph rewriting: An algebraic and logic approach. In: Handbook of Theoretical Computer Science, vol. B. Elsevier (1990)

    Google Scholar 

  12. Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)

    Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. 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)

    Article  Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zürich, Switzerland

    Christopher M. Poskitt

  2. Department of Computer Science, The University of York, UK

    Detlef Plump

Authors
  1. Christopher M. Poskitt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Detlef Plump
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Hasso Plattner Institut an der Universität Potsdam, Prof.-Dr.-Helmert-Strasse 2-3, 14482, Potsdam, Germany

    Holger Giese

  2. Fakultät für Ingenieurwissenschaften, Abteilung für Informatik und Angewandte Kognitionswissenscaft, Universität Duisburg-Essen, Lotharstraße 65, 47057, Duisburg, Germany

    Barbara König

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation