Online seminar

The calendar of events (iCal format).
In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.


Contact(s)

Reiko Heckel
Jean Krivine


The GReTA – Graph TRansformation Theory and Applications virtual seminar series aims to serve as a platform for the international graph rewriting community, to promote recent developments and trends in the field, and to permit a regular networking and interaction between members of this community. Seminars are held twice a month in the form of Zoom sessions (some of which will be live-streamed to YouTube).

Please refer to GReTA homepage for further information on how to participate in this seminar via Zoom or via YouTube live streams.


Previous talks



Year 2021

Graph Transformation Theory and Applications
Friday July 16, 2021, 3PM, online
Aleks Kissinger (Department of Computer Science, University of Oxford, UK) Picturing Quantum Software

Quantum circuits give a de facto “assembly language” for quantum computation. Hence, the design, optimisation, and verification of quantum circuits is an important task in developing efficient, correct software to run on quantum computers. In this talk, I will survey some of the latest developments in applying the ZX-calculus - a graphical theory of interacting quantum processes - to three important problems in quantum software: the optimisation of quantum circuits, functional verification of circuits, and development of heuristics for efficient classical simulation.

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Friday July 2, 2021, 3PM, online
Filippo Bonchi (Dipartimento di Informatica, Università degli Studi di Pisa, Italy) The Logic of Hypergraphs

A celebrated theorem of Chandra and Merlin states that Conjunctive Queries inclusion is decidable. Its proof transforms logical formulas to hypergraphs: each query has a natural model – a kind of graph – and query inclusion reduces to the existence of a graph homomorphism between natural models. In this talk, we introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as Conjunctive Queries. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters’ notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin’s insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Friday June 4, 2021, 3PM, online
Vincent Danos (CNRS & Ecole Normale Supérieure, Paris, France) Global Order Routing on Exchange Networks

We propose an abstract notion of networks of exchanges modelling the global money market of decentralised finance. We formalise routing and arbitrage on such networks as convex optimisation problems. We provide bounds with closed formulas in the specific case of “constant product” automated markets and a restricted form of cyclic arbitrage. We compute the associated lower bounds on actual data derived from the Ethereum blockchain. (joint work with Hamza El Khalloufi and Julien Prat)

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Friday May 21, 2021, 3PM, online
Andrea Corradini (Computer Science Department, University of Pisa, Italy) From Petri Nets to Graph Rewriting Systems: aspects of truly concurrent semantics

Graph rewriting systems are naturally endowed with a notion of parallelism due to the locality of the effect of rules. These aspects have been studied in the classical theory from an interleaving perspective, based on sequential independence, shift equivalence and related notions. In the last three decades the theory has been enriched with notions, constructions and results which provide a direct account of causality and non-determinism in graph derivations, borrowed from (and extending) the theory of Petri Nets. In the talk I will present a personal overview of the development of this theory starting from the basic structural relation between nets and graph rewriting systems, and I will survey some more recent developments.

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Friday May 7, 2021, 3PM, online
James Fairbanks (Department of Computer & Information Science & Engineering, University of Florida, USA) Computational Categorical Algebra with Catlab

A vast swath of computation and computer science theory takes place on combinatorial data structures, which are often presented as variations on the theme of graphs. Catlab.jl is a Julia package for computational category theory, which includes an implementation of C-Sets, also known as copresheafs or category actions. C-Sets always form an adhesive category and can be used for general rewriting systems. This talk will present the theory and implementation of C-Sets along with some examples. In particular, Colored Graphs and String Diagrams (syntax for symmetric monoidal categories) will be shown.

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Wednesday April 28, 2021, 6PM, online
Stephen Wolfram (Wolfram Research, Champaign, USA) GReTA Special Event: Graph Rewriting as a Foundation for Science and Technology (and the Universe)

About the speaker:

Stephen Wolfram is the creator of Mathematica, Wolfram|Alpha and the Wolfram Language; the author of “A New Kind of Science”; the originator of the Wolfram Physics Project; and the founder and CEO of Wolfram Research. Over the course of more than four decades, he has been a pioneer in the development and application of computational thinking—and has been responsible for many discoveries, inventions and innovations in science, technology and business.

Zoom registration

YouTube live stream

Graph Transformation Theory and Applications
Friday April 23, 2021, 3PM, online
Paweł Sobociński (Department of Computer Science, Tallinn University of Technology, Estonia) Rewriting Modulo Symmetric Monoidal Structure

String diagrams are an elegant, convenient and powerful syntax for arrows of symmetric monoidal categories. In recent years, they have been used as compositional descriptions of computational systems from various fields, including quantum foundations, linear algebra, control theory, automata theory, concurrency theory, and even linguistics. All of these applications rely on diagrammatic reasoning, which is to string diagrams as equational reasoning is to ordinary terms.

If we are to take string diagrams out of research papers and into practical applications, we need understand how to implement diagrammatic reasoning. This is the focus of my talk.

There is a tight correspondence between symmetric monoidal categories where every object has a coherent special Frobenius algebra structure and categories of cospans of hypergraphs. This correspondence, therefore, takes us from a topological understanding of string diagrams to a combinatorial data-structure-like description. Moreover, diagrammatic reasoning translates via this correspondence exactly to DPO rewriting with interfaces.

The obvious follow-up question is: how much of this correspondence survives if we drop the assumption about Frobenius structure? Can we use this correspondence to implement diagrammatic reasoning on vanilla symmetric monoidal categories? The answer is yes, but we need to restrict the kinds of cospans we consider: the underlying hypergraph has to be acyclic and satisfy an additional condition called monogamy. Moreover, we must restrict the DPO rewriting mechanism to a variant that we call convex DPO rewriting. The good news is that none of these modifications come with a significant algorithmic cost.

The material in this talk is joint work with Filippo Bonchi, Fabio Gadducci, Aleks Kissinger and Fabio Zanasi, and has been published in a series of papers:

- “Rewriting modulo symmetric monoidal structure”, Proceedings of LiCS 2016

- “Confluence of Graph Rewriting with Interfaces”, Proceedings of ESOP 2017

- “Rewriting with Frobenius”, Proceedings of LiCS 2018

YouTube recording

Graph Transformation Theory and Applications
Friday April 9, 2021, 3PM, online
Jonathan Gorard (University of Cambridge and Wolfram Research, UK) Hypergraph Rewriting and the Wolfram Model

This talk will summarize some recent results obtained in connection with the Wolfram Physics Project: a systematic attempt to reduce fundamental physics to the problem of hypergraph rewriting. Specifically, we will discuss the construction of an efficient hypergraph rewriting scheme using the formalism of Wolfram model multiway systems, with a categorical semantics defined via double-pushout rewrites over selective adhesive categories, and equipped with a dagger-symmetric monoidal structure that exhibits surprising formal connections to categorical quantum mechanics. We will also demonstrate that, by equipping such a multiway system with an additional notion of causal structure (defined via the semantics of precausal categories), we are able to introduce new inference rules of selective resolution, paramodulation and factoring that generalize the standard Knuth-Bendix completion rules for term rewriting systems, and significantly improve the efficiency of automated diagrammatic reasoning algorithms over hypergraphs. Time permitting, we will discuss some near-term practical applications of these methods for quantum information theory (allowing for more efficient diagrammatic simplification of quantum circuits), as well as numerical general relativity (allowing for more explicit numerical simulation of graph-theoretic models of space and time).

YouTube recording

Graph Transformation Theory and Applications
Friday March 26, 2021, 3PM, online
Hans-Jörg Kreowski & Aaron Frederick Lye (University of Bremen, Germany) Formal Graph Language Theory & Fusion Grammars

In the first part of the presentation, some aspects of formal graph language theory are discussed. A few variants of graph grammars were introduced in the early 1970s as generalizations of Chomsky grammars. This first step into a formal graph language theory was further developed by the investigation of edge and hyperedge replacement on one hand and on some variants of node replacement on the other hand starting in the late 1970s. Since then, a good number of structural and decidability properties were proved. In particular, it turned out that hyperedge replacement grammars behave to a large degree in a context-free manner. In the second part of the presentation, the novel approach of fusion grammars is surveyed.

A fusion grammar is a hypergraph grammar which provides a start hypergraph of small connected components. To derive hypergraphs, connected components can be copied multiple times and can be fused by the application of fusion rules (where such an application removes two complementary hyperedges and merges their attachment vertices). The generated hypergraph language contains all terminal connected components of derived hypergraphs. The main results for various kinds of fusion grammars concern their generative power.

YouTube live stream recording

Graph Transformation Theory and Applications
Friday March 12, 2021, 3PM, (online)
Jean-Pierre Jouannaud (Laboratoire d'Informatique (LIX), École Polytechnique) Composition-based Graph Rewriting

Double Pushout (DPO) rewriting, the dominant model for graph rewriting, emerged in the early 70’s, strongly influenced at that time by graph grammars. Developed by Hartmut Ehrig and his many collaborators, graph rewriting was from the beginning based on category theory, with the major insight that the two basic rewriting constructions, namely matching and replacement, were intimately related to graph morphisms and their pushouts. A new model has emerged recently, so-called Composition based rewriting (Core), in which rewriting is based on a composition operator over directed rooted labelled graphs (drags), so that matching a drag G against a drag L amounts to compose L with some context drag C, and rewriting G with L → R to compose R with C. We will describe Core for drags before to relate it precisely to DPO and extend it to adhesive categories of graphs and beyond. We will also show how to define composition abstractly in any category of graphs satisfying appropriate properties among which adhesivity (wrt monomorphisms). Major differences between DPO and Core will be discussed.

YouTube live stream recording

Graph Transformation Theory and Applications
Friday February 26, 2021, 3PM, (online)
Detlef Plump & Graham Campbell (University of York, UK & Newcastle University, UK) Fast Graph Programs

This will be an overview of our ongoing work on fast graph programs in the language GP 2. We will present programs which in some cases match the time complexity of graph algorithms in imperative languages. In other cases we need to assume that input graphs have a bounded degree, to reach the speed of conventional algorithms.

YouTube live stream recording

Graph Transformation Theory and Applications
Friday February 12, 2021, 3PM, (online)
Alexandru Burdusel & Steffen Zschaler (Department of Informatics, King's College London, UK) MDEOptimiser: Searching for optimal models with EMF and Henshin

An overview presentation of the work we have been doing over the past years on MDEOptimiser, a tool that uses evolutionary search over EMF models to solve multi-objective optimisation problems. Graph transformations are used to encode mutation operators, opening interesting opportunities for automatically generating domain-specific mutation operators.

YouTube live recording

Graph Transformation Theory and Applications
Friday January 29, 2021, 3PM, (online)
Leen Lambers & Fernando Orejas (Hasso-Plattner-Institut Potsdam, Germany & Technical University of Catalonia (UPC), Spain) Confluence of Graph Transformation

Confluence has been studied for graph transformation since several decades now. Confluence analysis has been applied, for example, to determining uniqueness of model transformation results in model-driven engineering. It is strongly related to conflict analysis for graph transformation, i.e. detecting and inspecting all possible conflicts that may occur for a given set of graph transformation rules. The latter finds applications, for example, in software analysis and design. Both conflict and confluence analysis rely on the existence and further analysis of a finite and representative set of conflicts for a given set of graph transformation rules.

Traditionally, the set of critical pairs has been shown to constitute such a set. It is representative in the sense that for each conflict a critical pair exists, representing the conflict in a minimal context, such that it can be extended injectively to this conflict (M-completeness). Recently, it has been shown that initial conflicts constitute a considerably reduced subset of critical pairs, being still representative in a slightly different way. In particular, for each conflict there exists a unique initial conflict that can be extended (possibly non-injectively) to the given conflict (completeness). Compared to the set of critical pairs, the smaller set of initial conflicts allows for more efficient conflict as well as confluence analysis.

We continue by demonstrating that initial conflicts (critical pairs) are minimally complete (resp. minimally M-complete), and thus are both optimally reduced w.r.t. representing conflicts in a minimal context via general (resp. injective) extension morphisms. We proceed with showing that it is impossible to generalize this result to the case of rules with application conditions (equivalent to FOL on graphs). We therefore revert to a symbolic setting, where finiteness and minimal (M-)completeness can again be guaranteed. Finally, we describe important special cases (e.g. rules with negative application conditions), where we are able to obtain minimally complete (resp. M-complete) sets of conflicts in the concrete setting again.

YouTube live recording of the seminar

Graph Transformation Theory and Applications
Friday January 15, 2021, 3PM, (online)
Christoph Bockisch & Gabriele Taentzer (Fachbereich Mathematik und Informatik, Philipps-Universität Marburg, Germany) Java Bytecode Verification and Manipulation based on Model Driven Engineering

Program transformations are frequently developed, e.g., to realize programming language extensions or dynamic program analyses such as profiling. They are typically implemented by manipulating bytecode as the availability of source code is not guaranteed. There are standard libraries such as ASM that are typically used for implementing Java bytecode manipulations. To check their correctness, they are usually tested by applying them to different programs, running the manipulated programs and observing their behaviors. As part of the second step, the Java virtual machine verifies the bytecode, which can uncover errors in the bytecode introduced by the manipulation. That approach uses different technologies that are not well linked making the process of developing and testing bytecode manipulations difficult. In this talk, we intend to perform bytecode manipulation by using concepts and techniques of model-driven engineering. We are convinced that the declarative nature of model transformation rules allows the debugging and analyzing of bytecode manipulations in more details than classically done. Following this path, a meta-model for bytecode is needed including OCL constraints for bytecode verification. We show that basing bytecode manipulation on model transformation can provide more immediate guidance and feedback to the developer, especially when model transformation is formally based on graph transformation. Bytecode verification can take place directly in the manipulated model with the help of OCL checking, eliminating the need to use multiple technologies. In some cases, it is even possible to automatically determine application conditions under which bytecode manipulations are correct by construction; then bytecode verification after a bytecode manipulation can be avoided altogether.

YouTube live recording of the seminar


Year 2020

Graph Transformation Theory and Applications
Friday December 18, 2020, 3PM, (online)
Maribel Fernandez & Bruno Pinaud (King's College London, UK & Université de Bordeaux, France) Hierarchical port graphs & PORGY - port graph rewriting as a modelling tool

Graph rewriting systems are natural verification and validation tools: they provide visual, intuitive representations of complex systems while specifying the dynamic behaviour of the system in a formal way. In this talk we will describe the use of strategic port graph rewriting as a basis for the implementation of a visual modelling tool: PORGY. We will present attributed hierarchical port graphs (AHP) and a notion of strategic AHP-rewriting as a mechanism to model the behaviour of dynamic systems. The system modelled is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions in the graph. In the second part of the talk, we describe PORGY and give examples of application in the areas of biochemistry, social networks and finance.

This is joint work with members of the PORGY team at Bordeaux and King’s College London.

YouTube live recording of the seminar

Graph Transformation Theory and Applications
Friday December 4, 2020, 3PM, (online)
Daniel Merkle & Jakob Lykke Andersen (Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark) Chemical Graph Transformation and Applications

Any computational method in chemistry must choose some level of precision in the modeling. One choice is made in the methods of quantum chemistry based on quantum field theory. While highly accurate, the methods are computationally very demanding, which restricts their practical use to single reactions of molecules of moderate size even when run on supercomputers. At the same time, most existing computational methods for systems chemistry and biology are formulated at the other abstraction extreme, in which the structure of molecules is represented either not at all or in a very rudimentary fashion that does not permit the tracking of individual atoms across a series of reactions.

In this talk, we present our on-going work on creating a practical modelling framework for chemistry based on Double Pushout graph transformation, and how it can be applied to analyse chemical systems. We will address important technical design decisions as well as the importance of methods inspired from Algorithm Engineering in order to reach the required efficiency of our implementation. We will present chemically relevant features that our framework provides (e.g. automatic atom tracing) as well as a set of chemical systems we investigated are currently investigating. If time allows we will discuss variations of graph transformation rule compositions and their chemical validity.

video recording of the seminar on YouTube

Graph Transformation Theory and Applications
Friday November 20, 2020, 3PM, (online)
Barbara König (Fakultät für Ingenieurwissenschaften, Universität Duisburg-Essen, Germany) Graph Transformation Meets Logic

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.

video recording of the seminar on YouTube