Baldan, Paolo; Corradini, Andrea; König, Barbara:
Unfolding-Based Verification for Graph Transformation Systems
In: Proceedings of Uniform Approaches to Graphical Specification Techniques, UniGra 2003 - Warsaw, 2003
2003Buchaufsatz/Kapitel in Sammelwerk
Informatik
Titel:
Unfolding-Based Verification for Graph Transformation Systems
Autor*in:
Baldan, Paolo;Corradini, Andrea;König, BarbaraUDE
GND
1050396502
LSF ID
15982
ORCID
0000-0002-4193-2889ORCID iD
Sonstiges
der Hochschule zugeordnete*r Autor*in

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.