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
Buchaufsatz/Kapitel in Sammelwerk2003Informatik
Titel:
A Logic for Analyzing Abstractions of Graph Transformation Systems
Autor(in):
Baldan, Paolo; König, BarbaraLSF; König, Bernhard
Erscheinungsjahr
2003
WWW URL
Erschienen in:
Titel:
Static Analysis : Proceedings of the 10th International Symposium on International Static Analysis Symposium, SAS 2003. - (Lecture Notes in Computer Science ; 2694)
Erscheinungsort
Berlin [u.a.]
Verlag
Springer
Erscheinungsjahr
2003
in:
S. 1072 - 1073
ISBN:

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