An Unfolding-based Approach for the Verification of Finite-State ...


Paolo Baldan, Andrea Corradini, and Barbara König. An unfolding-based approach for the verification of finite-state graph grammars. Technical Report CS-2004-10, Dipartimento di Informatica, Università Ca' Foscari di Venezia, 2004.


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},
    institution = {Dipartimento di Informatica, Universit\`{a} Ca' Foscari di Venezia},
    number = {CS-2004-10},
    title = {An Unfolding-based Approach for the Verification of Finite-State Graph Grammars},
    year = {2004}

GZipped PostScript (225 kB)PDF (343 kB)See ...Conference version
© University of Duisburg-Essen, Theoretical Computer Science group