Abstract Interpretation of Graph Transformation

The semantics of many dynamic systems can be described by evolving graphs. Graph transformation systems (GTS) are a natural, intuitive, and formally defined method to specify systems of evolving graphs, whereas verification techniques for GTS are scarce. We present an abstract interpretation based approach for GTS verification. Single graphs are abstracted in two steps. First similar nodes within a connected component, then similar abstracted connected components are summarized. Transformation rules are applied directly to abstract graphs yielding a bounded set of abstract graphs of bounded size that over-approximates the concrete GTS and can be used for further verification. Since our abstraction is homomorphic, existential positive properties are preserved under abstraction. Furthermore, we identify automatically checkable completeness criteria for the abstraction. The technique is implemented and successfully tested on the platoon case study