A Temporal Graph Logic for Abstractions of Graph Rewriting Systems

Paolo Baldan, Andrea Corradini, Barbara König, Alberto Lluch Lafuente

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We extend our approach for verifying properties of graph transformation systems using suitable abstractions. In the original approach properties are specified as formulae of a propositional temporal logic whose atomic predicates are monadic second-order graph formulae. We generalize this aspect by considering more expressive logics, where edge quantifiers and temporal modalities can be interleaved, a feature which allows, e.g., to trace the history of objects in time. This requires the use of graph transition systems, a generalization of transition systems where states and transitions are mapped to graphs and graph morphisms, respectively, and of a corresponding notion of abstraction. After characterizing fragments of the logic which can be safely checked on the approximations, we show how the verification of the logic over graph transformation systems can be reduced to the verification of a logic over suitably defined Petri nets.
Original languageEnglish
Title of host publicationRecent Trends in Algebraic Development Techniques : 18th International Workshop, WADT 2006, La Roche en Ardenne, Belgium, June 1-3, 2006, Revised Selected Papers
PublisherSpringer Berlin Heidelberg
Publication date2007
Pages1-20
ISBN (Print)978-3-540-71997-7
ISBN (Electronic)978-3-540-71998-4
DOIs
Publication statusPublished - 2007
Externally publishedYes
Event18th International Workshop on Algebraic Development Techniques - La Roche en Ardenne, Belgium
Duration: 1 Jun 20063 Jun 2006
Conference number: 18

Conference

Conference18th International Workshop on Algebraic Development Techniques
Number18
CountryBelgium
CityLa Roche en Ardenne
Period01/06/200603/06/2006
SeriesLecture Notes in Computer Science
Volume4409
ISSN0302-9743

Cite this

Baldan, P., Corradini, A., König, B., & Lluch Lafuente, A. (2007). A Temporal Graph Logic for Abstractions of Graph Rewriting Systems. In Recent Trends in Algebraic Development Techniques: 18th International Workshop, WADT 2006, La Roche en Ardenne, Belgium, June 1-3, 2006, Revised Selected Papers (pp. 1-20). Springer Berlin Heidelberg. Lecture Notes in Computer Science, Vol.. 4409 https://doi.org/10.1007/978-3-540-71998-4_1