Baldan, Paolo; König, Barbara; König, Bernhard:

A Logic for Analyzing Abstractions of Graph Transformation Systems

In: Static Analysis : Proceedings of the 10th International Symposium on International Static Analysis Symposium, SAS 2003. - (Lecture Notes in Computer Science ; 2694)
Berlin [u.a.]: Springer (2003), S. 1072-1073
ISBN: 978-3-540-40325-8
Buchaufsatz / Kapitel / Fach: Informatik
Abstract:
A technique for approximating the behaviour of graph transformation
systems (GTSs) by means of Petri net-like structures has been
recently dened in the literature. In this paper we introduce a monadic
second-order logic over graphs expressive enough to characterise typical
graph properties, and we show how its formulae can be eectively
veried. More specically, we provide an encoding of such graph formulae
into quantier-free formulae over Petri net markings and we characterise,
via a type assignment system, a subclass of formulae F such
that the validity of F over a GTS G is implied by the validity of the
encoding of F over the Petri net approximation of G. This allows us to
reuse existing verication techniques, originally developed for Petri nets,
to model-check the logic, suitably enriched with temporal operators.
1 I