Locality in Reasoning about Graph Transformations

This paper explores how to reason locally about global properties of graph transformations, in particular properties involving transitive closure of the edge relations of the graph. We show under which conditions we can soundly reduce reasoning about all nodes in the graph to reasoning about a finite set of nodes. We then give an effective procedure to turn this reduced problem into a Boolean satisfiability problem.
 

Online Copy

Conference version: PDF

BibTeX Entry

@incollection{strecker11:_local_reason_graph_trans,
year={2012},
isbn={978-3-642-34175-5},
booktitle={Applications of Graph Transformations with Industrial Relevance},
volume={7233},
series={Lecture Notes in Computer Science},
editor={Schürr, Andy and Varró, Dániel and Varró, Gergely},
doi={10.1007/978-3-642-34176-2_15},
title={Locality in Reasoning about Graph Transformations},
url={https://www.irit.fr/~Martin.Strecker/Publications/agtive11.html},
publisher={Springer Berlin Heidelberg},
keywords={Graph transformations; formal methods; verification},
author={Strecker, Martin},
pages={169-181}
}