Jour, heure et lieu

Le vendredi à 15h, online

Le calendrier des séances (format iCal).
Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.


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.


Prochaines séances


Graph Transformation Theory and Applications
Vendredi 22 octobre 2021, 15 heures, online
Frank Drewes, Berthold Hoffmann & Mark Minas (Department of Computing Science, Umeå University, Sweden; Department of Mathematics and Informatics, University of Bremen, Germany; Institute for Software Technology, Computer Science Department, Universität der Bundeswehr München , Germany) Contextual Hyperedge Replacement Grammars: Languages – Parsing – Grappa

Graph transformation allows to extend formal language theory to the generation of graph languages. This has applications in areas such as model-driven software engineering, natural language processing, and shape analysis of programs.

We start from the well-established theory of context-free grammars based on hyperedge replacement (HR) and introduces a modest extension, contextual hyperedge replacement (CHR), in order to extend their generative power. We discuss the generative power and other properties of CHR, and relate them to HR.

Then we consider parsing for CHR grammars. As for HR, parsing is NP-complete in general, so that efficient parsing algorithms can only be achieved for subclasses. We have devised two algorithms, called predictive top-down (PTD) and predictive shift-reduce (PSR), which are inspired by the well-known LL(k) and LR(k) parsing for strings, and are usually linear, at most quadratic. We illustrate the ideas of these algorithms by graph transformation rules.

Finally we demonstrate Mark Minas' graph parser generator Grappa, which implements not only PTD and PSR parsing, including the needed analysis tools, but also generalized PSR, where parallel parsing allows to cope with ambiguous grammars. Measurements of generated parsers validate our theoretical findings regarding complexity.

Zoom meeting registration link

YouTube live stream

Graph Transformation Theory and Applications
Vendredi 19 novembre 2021, 15 heures, online
Jens H. Weber (Department of Computer Science, University of Victoria, Canada) GRAPEpress - A Computational Notebook for Graph Transformations

Computational notebooks (CNs) have gained popularity in data science, artificial intelligence, and engineering. CNs are used to document experiments and make them repeatable by incorporating executable segments and renderings of computational results. Unfortunately, computations by graph transformations are not supported by current CNs. In order to close this gap, we have developed GRAPEPress, a tool that combines the GRAPE graph transformation language with the CN tool Gorilla. This talk introduces the GRAPE language as well as its integration with the CN tool Gorilla.

Zoom meeting registration link

YouTube live stream


Séances passées



Année 2021

Graph Transformation Theory and Applications
Vendredi 8 octobre 2021, 15 heures, online
Stefan Höppner & Raffaela Groner (Institute of Software Engineering and Programming Languages, University of Ulm, Germany) Model Transformation Languages and Performance Engineering

This event will consist of two talks: “Investigating claimed Advantages and Disadvantages of Model Transformation Languages” (by Stefan Höppner) and “Current State of Performance Engineering of Model Transformations” (by Raffaela Groner). Please refer to https://www.irif.fr/~greta/event/2021-oct-08 for the respective abstracts.

Zoom meeting registration link

YouTube live stream

Graph Transformation Theory and Applications
Vendredi 24 septembre 2021, 15 heures, online
Romain Pascual (MICS laboratory, CentraleSupélec, University Paris-Saclay, France) Combinatorial maps: transformations and application to geometric modeling

In the first part of the talk, I will present generalized maps that represent quasi-manifolds through their subdivision into topological cells (vertices,edges, faces, volumes). We defined generalized maps as constrained labeled graphs. Arc labels encode topological relations of the subparts modeled object while node labels describe the geometric data used to represent the object. Modeling operations are designed regardless of the object's underlying topology. Therefore, we generalize DPO rules with a functorial approach to encode semi-global relabeling with a product operation. Rules and their extensions (called rule schemes) are considered valid if any application to a well-formed graph results in an equally well-formed graph. We provide set-theoric conditions on rules and rule schemes to ensure the preservation of the model consistency. In the second part of the talk, I will present how this approach allows the design of geometric modelers (software used to create and edit geometric objects) in Jerboa. The set-theoric conditions can be checked via graph traversal in Jerboa's rule editor to ensure that the code derived from the rule will never break the model. The generated code can be used as an add-on in other software or Jerboa's generic viewer. 

Zoom meeting registration link

YouTube live stream

Graph Transformation Theory and Applications
Vendredi 10 septembre 2021, 15 heures, online
Mario Alvarez-Picallo (Department of Computer Science, University of Oxford, UK) Soundness for Automatic Differentiation via String Diagrams

Reverse-mode automatic differentiation, especially in the presence of complex language features, is notoriously hard to implement correctly, and most implementations focus on differentiating straight-line imperative first-order code. Generalisations exist, however, that can tackle more advanced features; for example, the algorithm described by Pearlmutter and Siskind in their 2008 paper can differentiate higher-order functions written in a pure functional language. We show that AD algorithms can benefit enormously from being translated into the language of string diagrams in two steps: first, we describe a Pearlmutter-Siskind style AD algorithm as a set of rules for transforming hierarchical graphs; rules which can -and indeed have been- be implemented correctly and efficiently for a non-trivial language. Then, we present a proof of soundness for it by reducing the above rewrite rules to a suitable graphical version of the axioms of Cartesian reverse differential categories, expressed as string diagrams.

Zoom meeting registration link

YouTube live stream

Graph Transformation Theory and Applications
Vendredi 16 juillet 2021, 15 heures, 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
Vendredi 2 juillet 2021, 15 heures, 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
Vendredi 4 juin 2021, 15 heures, 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
Vendredi 21 mai 2021, 15 heures, 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
Vendredi 7 mai 2021, 15 heures, 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
Mercredi 28 avril 2021, 18 heures, 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
Vendredi 23 avril 2021, 15 heures, 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
Vendredi 9 avril 2021, 15 heures, 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
Vendredi 26 mars 2021, 15 heures, 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
Vendredi 12 mars 2021, 15 heures, (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
Vendredi 26 février 2021, 15 heures, (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
Vendredi 12 février 2021, 15 heures, (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
Vendredi 29 janvier 2021, 15 heures, (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
Vendredi 15 janvier 2021, 15 heures, (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


Année 2020

Graph Transformation Theory and Applications
Vendredi 18 décembre 2020, 15 heures, (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
Vendredi 4 décembre 2020, 15 heures, (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
Vendredi 20 novembre 2020, 15 heures, (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