Paper Info
Title
A logic for analyzing abstractions of graph transformation systems
Abstract
A technique for approximating the behaviour of graph transformation systems (GTSs) by means of Petri net-like structures has been recently defined 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 effectively verified. More specifically, we provide an encoding of such graph formulae into quantifier-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 verification techniques, originally developed for Petri nets, to model-check the logic, suitably enriched with temporal operators.
Year
DOI
Venue
2003
10.1007/3-540-44898-5_14
SAS
Keywords
Field
DocType
formulae f,quantifier-free formula,graph transformation system,typical graph property,petri net,monadic second-order logic,graph formula,existing verification technique,petri net-like structure,gts g,graph transformation,model checking
Discrete mathematics,Logic model,Petri net,Graph property,Second-order logic,Computer science,Theoretical computer science,Graph rewriting,Temporal logic,Clique-width,Monadic predicate calculus
Conference
Volume
ISSN
ISBN
2694
0302-9743
3-540-40325-6
Citations 
PageRank 
References 
21
1.24
12
Authors
3
Name
Order
Citations
PageRank
Paolo Baldan169651.95
Barbara König21468.23
Bernhard König3445.84