2011 | OriginalPaper | Buchkapitel
Sound and Complete Abstract Graph Transformation
verfasst von : Dominik Steenken, Heike Wehrheim, Daniel Wonisch
Erschienen in: Formal Methods, Foundations and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Graph transformation systems (GTS) are a widely used technique for the formal modeling of structures and structure changes of systems. To verify properties of GTS, model checking techniques have been developed, and to cope with the inherent infinity arising in GTS state spaces, abstraction techniques are employed.
In this paper, we introduce a novel representation for abstract graphs (which are shape graphs together with
shape constraints
) and define transformations (execution steps) on abstract graphs. We show that these abstract transformations are sound and complete in the sense that they capture exactly the transformations on the concrete graph level. Furthermore, abstract transformation can be carried out fully automatically. We thus obtain an effectively computable “best transformer” for abstract graphs which can be employed in an abstraction-based verification technique for GTS.