Modeling and Verifying Graph Transformations in Proof Assistants

Abstract

This paper takes first steps towards a formalization of graph transformations in a general setting of interactive theorem provers, which will form the basis for proofs of correctness of graph transformation systems. Whereas graph rewriting is usually performed by mapping a pattern graph into a source graph by means of a graph morphism and then carrying out operations on the image node and edge set, this article generalises the notion of pattern graph to path expressions, which are formulae in a fragment of first-order logic. We examine the correspondence with traditional graph rewriting and show that this interpretation is beneficial when formally reasoning about model transformations with the aid of proof assistants.

Online Copy

Available as PDF

DOI reference

BibTeX Entry

@InProceedings{strecker07:_model_verif_graph_trans_proof_assis,
  author = {Martin Strecker},
  title = {Modeling and Verifying Graph Transformations in Proof Assistants},
  booktitle =	"{International Workshop on Computing with Terms and
		 Graphs (TERMGRAPH), Braga/Portugal, 31/03/2007}",
  editor =	"Ian Mackie and Detlef Plump",
  year = 2008,
  publisher =	"Elsevier Science",
  address =	"http://www.elsevier.com",
  volume =	203,
  series =	"Electronic Notes in Theoretical Computer Science",
  pages =	"135--148"
}