A Logic for Analyzing Abstractions of Graph Transformation Systems

Reference

Paolo Baldan, Barbara König, and Bernhard König. A logic for analyzing abstractions of graph transformation systems. In Proc. of SAS '03 (International Static Analysis Symposium), pages 255–272. Springer-Verlag, 2003. LNCS 2694.

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 such that the validity of over a GTS is implied by the validity of the encoding of over the Petri net approximation of . This allows us to reuse existing verification techniques, originally developed for Petri nets, to model-check the logic, suitably enriched with temporal operators.

Suggested BibTeX entry:

@inproceedings{BKK03,
    author = {Paolo Baldan and Barbara K\"{o}nig and Bernhard K\"on{}ig},
    booktitle = {Proc. of SAS '03 (International Static Analysis Symposium)},
    note = {{LNCS} 2694},
    pages = {255--272},
    publisher = {Springer-Verlag},
    title = {A Logic for Analyzing Abstractions of Graph Transformation Systems},
    year = {2003}
}

GZipped PostScript (157 kB)PDF (264 kB)