Counterexample-guided Abstraction Renement for the Analysis of Graph Transformation Systems?

Abstract. Graph transformation systems are a general specication language for systems with dynamically changing topologies, such as mo-bile and distributed systems. Although in the last few years several anal-ysis and verication methods have been proposed for graph transforma-tion systems, counterexample-guided abstraction renement has not yet been studied in this setting. We propose a counterexample-guided abstraction renement technique which is based on the over-approximation of graph transformation sys-tems (gts) by Petri nets. We show that a spurious counterexample is caused by merging nodes during the approximation. We present a tech-nique for identifying these merged nodes and splitting them using ab-straction renement, which removes the spurious run. The technique has been implemented in the Augur tool and experimental results are dis-cussed.