Abstract Interpretation of Graph Transformation

Abstract

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.