Document Open Access Logo

Proving Correctness of Logically Decorated Graph Rewriting Systems

Authors Jon Haël Brenas, Rachid Echahed, Martin Strecker

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2016.14.pdf
  • Filesize: 0.59 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Graph Rewriting
  • Hoare Logic,Combinatory PDL
  • Rewrite Strategies
  • Program Verification

Metrics

Abstract

We first introduce the notion of logically decorated rewriting systems where the left-hand sides are endowed with logical formulas which help to express positive as well as negative application  conditions, in addition to classical pattern-matching. These systems are defined using graph structures and an extension of combinatory propositional
dynamic logic, CPDL, with restricted universal programs, called C2PDL. In a second step, we tackle the  problem of proving the correctness of logically decorated graph rewriting systems by using a Hoare-like calculus. We  introduce a notion  of specification defined as a tuple (Pre, Post, R, S) with Pre and Post being formulas of C2PDL, R a rewriting  system and S a rewriting strategy. We provide a sound  calculus which infers proof obligations of the considered specifications and establish the decidability of the verification problem of the (partial) correctness of the considered specifications.

Cite As Get BibTex

Jon Haël Brenas, Rachid Echahed, and Martin Strecker. Proving Correctness of Logically Decorated Graph Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.14

Author Details

Jon Haël Brenas
Rachid Echahed
Martin Strecker

References

  1. Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson. On the logic of theory change: Partial meet contraction and revision functions. J. Symb. Log., 50(2):510-530, 1985. URL: http://dx.doi.org/10.2307/2274239.
  2. Carlos Areces and Balder ten Cate. Hybrid logics. In Studies in Logic and Practical Reasoning, volume 3, pages 821-868. Elsevier, 2007. Google Scholar
  3. Philippe Balbiani, Rachid Echahed, and Andreas Herzig. A dynamic logic for termgraph rewriting. In 5th International Conference on Graph Transformations (ICGT), volume 6372 of Lecture Notes in Computer Science, pages 59-74. Springer, 2010. Google Scholar
  4. Jon Haël Brenas, Rachid Echahed, and Martin Strecker. A Hoare-like calculus using the SROIQ σ logic on transformations of graphs. In Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings, pages 164-178, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44602-7_14.
  5. Jon Hael Brenas, Rachid Echahed, and Martin Strecker. C2PDLS: A combination of combinatory and converse PDL with substitutions. 2015. URL: http://lig-membres.imag.fr/echahed/c2pdls.pdf.
  6. Ricardo Caferra, Rachid Echahed, and Nicolas Peltier. A term-graph clausal logic: Completeness and incompleteness results. Journal of Applied Non-classical Logics, 18(4):373-411, 2008. Google Scholar
  7. Rachid Echahed. Inductively sequential term-graph rewrite systems. In 4th International Conference on Graph Transformations, ICGT, volume 5214 of Lecture Notes in Computer Science, pages 84-98. Springer, 2008. Google Scholar
  8. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: http://dx.doi.org/10.1016/0022-0000(79)90046-1.
  9. Annegret Habel, Reiko Heckel, and Gabriele Taentzer. Graph grammars with negative application conditions. Fundam. Inform., 26(3/4):287-313, 1996. URL: http://dx.doi.org/10.3233/FI-1996-263404.
  10. Annegret Habel and Karl-Heinz Pennemann. Correctness of high-level transformation systems relative to nested conditions. MSCS, 19:245-296, 2009. Google Scholar
  11. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: http://dx.doi.org/10.1145/363235.363259.
  12. Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, and Greta Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, volume 3210 of Lecture Notes in Computer Science, pages 160-174. Springer Berlin / Heidelberg, 2004. URL: http://www.cs.umass.edu/~immerman/pub/cslPaper.pdf.
  13. Kazuhiro Inaba, Soichiro Hidaka, Zhenjiang Hu, Hiroyuki Kato, and Keisuke Nakano. Graph-transformation verification using monadic second-order logic. In Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20-22, 2011, Odense, Denmark, pages 17-28, 2011. URL: http://dx.doi.org/10.1145/2003476.2003482.
  14. Barbara König and Javier Esparza. Verification of graph transformation systems with context-free specifications. In Graph Transformations - 5th International Conference, ICGT 2010, Enschede, The Netherlands, September 27 - October 2, 2010. Proceedings, pages 107-122, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15928-2_8.
  15. Solomon Passy and Tinko Tinchev. An essay in combinatory dynamic logic. Inf. Comput., 93(2):263-332, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90026-X.
  16. Christopher M. Poskitt and Detlef Plump. Verifying monadic second-order properties of graph programs. In Graph Transformation - 7th International Conference, ICGT 2014, Held as Part of STAF 2014, York, UK, July 22-24, 2014. Proceedings, pages 33-48, 2014. URL: http://dx.doi.org/10.1007/978-3-319-09108-2_3.
  17. Arend Rensink, Ákos Schmidt, and Dániel Varró. Model checking graph transformations: A comparison of two approaches. In Graph Transformations, Second International Conference, ICGT 2004, Rome, Italy, September 28 - October 2, 2004, Proceedings, pages 226-241, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30203-2_17.
  18. Grzegorz Rozenberg, editor. Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact