In: Holger Hermanns, Jens Palsberg (Eds.): Lecture Notes in Computer Science, 3920: Tools and Algorithms for the Construction and Analysis of Systems: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006., pages 197-211. Springer-Verlag, January 2006. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1169137213,.
Abstract: Graph transformation systems are a general specification language for systems with dynamically changing topologies, such as mobile and distributed systems. We propose a counterexample-guided abstraction refinement technique which is based on the over-approximation of graph transformation systems (gts) by Petri nets. We show that a spurious counterexample is caused by merging nodes during the approximation. We present a technique for identifying these merged nodes and splitting them using abstraction refinement, which removes the spurious run. The technique has been implemented in the Augur tool and experimental results are discussed.