Unfolding-Based Verification for Graph Transformation Systems

Reference

Paolo Baldan, Andrea Corradini, and Barbara König. Unfolding-based verification for graph transformation systems. In Proc. of UniGra '03: Uniform Approaches to Graphical Specification Techniques (Warsaw), 2003.

Abstract

The unfolding semantics of graph transformation systems can represent a basis for their formal verification. For general, possibly infinite-state, graph transformation systems one can construct finite under- and over- approximations of the (infinite) unfolding, with arbitrary accuracy. Such approximations can be used to check properties of a graph transformation system, like safety and liveness properties, expressed in suitable fragments of the -calculus. For finite-state graph transformation systems, a variant of McMillan's approach (originally developed for Petri nets) allows us to single out a finite under-approximation which is a so-called complete prefix of the unfolding, i.e., which provides an "exact" representation of the behaviour the original system as far as reachable states are concerned. Some problems related to the constructive definition of the prefix are discussed.

Suggested BibTeX entry:

@inproceedings{BCK03,
    author = {Paolo Baldan and Andrea Corradini and Barbara K{\"o}nig},
    booktitle = {Proc. of UniGra '03: Uniform Approaches to Graphical Specification Techniques (Warsaw)},
    title = {Unfolding-Based Verification for Graph Transformation Systems},
    year = {2003}
}



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