Verifying a Behavioural Logic for Graph Transformation Systems


Paolo Baldan, Andrea Corradini, Barbara König, and Bernhard König. Verifying a behavioural logic for graph transformation systems. In Proc. of COMETA '03, volume 104 of ENTCS, pages 5–24. Elsevier, 2004.


We propose a framework for the verification of behavioural properties of systems modelled as graph transformation systems. The properties can be expressed in a temporal logic which is basically a -calculus where the state predicates are formulae of a monadic second order logic, describing graph properties. The verification technique relies on an algorithm for the construction of finite over-approximations of the unfolding of a graph transformation system.

Suggested BibTeX entry:

    author = {Paolo Baldan and Andrea Corradini and Barbara K{\"o}nig and Bernhard K{\"o}nig},
    booktitle = {Proc. of COMETA '03},
    pages = {5--24},
    publisher = {Elsevier},
    series = {ENTCS},
    title = {Verifying a Behavioural Logic for Graph Transformation Systems},
    volume = {104},
    year = {2004}

GZipped PostScript (183 kB)PDF (301 kB)
© University of Duisburg-Essen, Theoretical Computer Science group