Proving Correctness of Logically Decorated Graph Rewriting Systems

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.
 

Online Copy

Online version

BibTeX Entry

@inproceedings{brenas16:_provin_correc_logic_decor_graph_rewrit_system,
  author    = {Jon Ha{\"{e}}l Brenas and
               Rachid Echahed and
               Martin Strecker},
  title     = {Proving Correctness of Logically Decorated Graph Rewriting Systems},
  booktitle = {1st International Conference on Formal Structures for Computation
               and Deduction, {FSCD} 2016, June 22-26, 2016, Porto, Portugal},
  editor    = {Delia Kesner and Brigitte Pientka},
  series    = {LIPIcs},
  volume    = {52},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  pages     = {14:1--14:15},
  year      = 2016,
  url       = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.14},
  doi       = {10.4230/LIPIcs.FSCD.2016.14}
}