Graph Transformation Meets Logic
Abstract
We review the integration of (first-order) logic respectively nested conditions into graph transformation. Conditions can serve various purposes: they can constrain graph rewriting, symbolically specify sets of graphs, be used in query languages and in verification (for instance in Hoare logic and for behavioural equivalence checking).
In the graph transformation community the formalism of nested graph conditions has emerged, that is, conditions which are equivalent to first-order logic, but directly integrate graphs and graph morphisms, in order to express constraints more succinctly.
In this talk we also explain how the notion of nested conditions can be lifted from graph transformation systems to the setting of reactive systems as defined by Leifer and Milner. It turns out that some constructions for graph transformation systems (such as computing weakest preconditions and strongest postconditions and showing local confluence by means of critical pair analysis) can be done quite elegantly in the more general setting.
Barbara König
Professor of Computer Science
Barbara König is a German computer scientist. She is head of the chair of Theoretical Computer Science at the Faculty of Engineering at the University of Duisburg-Essen. König studied at the Technical University of Munich from 1990 to 1995 and worked as a research assistant at the Department of Computer Science II until 2003. In 1999 she received her doctorate with a dissertation on “Description and Verification of Mobile Processes with Graph Rewriting Techniques” under Jürgen Eickel. From 2003 to 2006 she headed an Emmy Noether junior research group at the University of Stuttgart. Based on her habilitation thesis on “Analysis and verification of systems with dynamically evolving structure”, she was awarded the venia legendi there in 2005. In 2006, she accepted the offer of a professorship at the University of Duisburg-Essen, where she has since been head of the Chair of Theoretical Computer Science at the Faculty of Engineering on the Duisburg campus. Her main research interests are graph transformation, verification and analysis, fixpoint equations, as well as behavioural equivalences and coalgebra.