Verifying Finite-State Graph Grammars: an Unfolding-Based Approach


Paolo Baldan, Andrea Corradini, and Barbara König. Verifying finite-state graph grammars: an unfolding-based approach. In Proc. of CONCUR '04, pages 83–98. Springer-Verlag, 2004. LNCS 3170.


We propose a framework where behavioural properties of finite-state systems modelled as graph transformation systems can be expressed and verified. The technique is based on the unfolding semantics and it generalises McMillan's complete prefix approach, originally developed for Petri nets, to graph transformation systems. It allows to check properties of the graphs reachable in the system, expressed in a monadic second order logic.

Suggested BibTeX entry:

    author = {Paolo Baldan and Andrea Corradini and Barbara K{\"o}nig},
    booktitle = {Proc. of CONCUR '04},
    note = {{LNCS} 3170},
    pages = {83--98},
    publisher = {Springer-Verlag},
    title = {Verifying Finite-State Graph Grammars: an Unfolding-Based Approach},
    year = {2004}

GZipped PostScript (139 kB)PDF (231 kB)Tech report version
© University of Duisburg-Essen, Theoretical Computer Science group