Counterexample-guided Abstraction Refinement for the Analysis of ...


Barbara König and Vitali Kozioura. Counterexample-guided abstraction refinement for the analysis of graph transformation systems. In Proc. of TACAS '06, pages 197–211. Springer, 2006. LNCS 3920.


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.

Suggested BibTeX entry:

    author = {Barbara K{\"o}nig and Vitali Kozioura},
    booktitle = {Proc. of TACAS '06},
    note = {LNCS 3920},
    pages = {197--211},
    publisher = {Springer},
    title = {Counterexample-guided Abstraction Refinement for the Analysis of Graph Transformation Systems},
    year = {2006}

PDF (222 kB)Tech report version
© University of Duisburg-Essen, Theoretical Computer Science group