.GReTA-seminar

We introduce a categorical formalism for rewriting surface-embedded graphs. Such graphs can represent string diagrams in a non-symmetric setting where we guarantee that the wires do not intersect each other. The main technical novelty is a new formulation of double pushout rewriting on graphs which explicitly records the boundary of the rewrite. Using this boundary structure we can augment these graphs with a rotation system, allowing the surface topology to be incorporated.

Graphs are key abstractions in science and engineering. They may represent linked data in graph databases or social networks, complex designs of cyber-physical systems, or critical validation scenarios for autonomous systems. Synthetic graph generators are essential when the use of real graph models is restricted (to respect privacy regulations or intellectual properties of companies) or impractical (to find corner-cases for safety assurance). In this talk, I will provide an overview of major challenges and recent research results on automated graph generation which aims to derive domain-specific graph models which are simultaneously consistent (CO), realistic (RE), diverse (DI) and scalable (SC). In particular, I will present a graph solver that combines advanced graph algorithms with 3-valued logic satisfiability techniques.

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules.

Previous work has shown that string diagrams for freely generated symmetric monoidal categories can be viewed as hypergraphs with interfaces, and the axioms of these categories can be realized by rewriting systems. This work proposes hierarchical hypergraphs as a suitable formalization of string diagrams for monoidal closed categories. We then show double pushout rewriting captures the axioms of these closed categories.

The transformation of graphs can be described using rules. They can also be expressed by an energy function that defines the steady state probabilities for different graph conformations. Years ago a result was obtained relating graph energy functions and systems of graph transformation rules. Implementating the algorithm that takes an energy function and generates the corresponding rules showed us that other options were also available, that is, that different algorithms could produce different systems of graph transformation rules for the same energy function. We wonder, then, what is the relationship between theses algorithms and why it would be preferable to use one or the other.

In the talk we present the Generalized Sketch Formalism à la Makkai/Diskin as a straightforward and quite natural generalization of specification formalisms based on graphs and graph transformations.
We discuss why traditional Ehresmann Sketches are not fully adequate for the formalization of Software Models and argue in favor of Generalized Sketches. Ehresmann Sketches utilize only the properties commutative, limit or colimit, respectively, while we are allowed to work with arbitrary “user defined” properties in Generalized Sketches. Makkai proposed Sketch Implications as a tool to axiomatize the meaning of “user defined” properties and we elucidate that especially limit and colimit properties can be expressed by means of Sketch Implications. On the other side, we can utilize Sketch Implications as a tool to describe the structure of Software Models.
Compared to Graph Transformations, Sketch Transformations give us a more refined and expressive tool at hand to formalize Model Transformations. It looks like, however, that only the use of cospan transformation rules instead of the traditional span transformation rules would enable us to derive full advantage of sketches.

Based on a new concept of first-order generalized sketches we coined lately “Logics of Statements in Context” to provide a unified view on formalisms like Algebraic Specifications, Prolog, First-Order Logic, Ehresmann Sketches, Description Logics, Generalized Sketches à la Makkai/Diskin, Diagram Predicate Framework, Graph Conditions, and others.
In the talk we present Generalized Sketches à la Makkai/Diskin as a quite natural generalization of traditional Ehresmann sketches. Generalized Sketches à la Makkai/Diskin can be defined in arbitrary categories. They built upon “atomic statements in context” and utilize sketch implications for axiomatization purposes. Going beyond atomic statements, we outline the definition of arbitrary first-order statements in arbitrary categories enabling us to enhance the expressiveness of Generalized Sketches. In analogy to first-order statements, we can also define arbitrary first-order sketch conditions generalizing thereby different kinds of “nested graph constraints and conditions”.
We intend to discuss, on the way, two essential constructions Makkai’s work on Generalized Sketches relies on: “Syntactic representation of models” and “internalization of atomic statements”.

Graph databases are now playing an important role because they allow us to overcome some limitations of relational databases. In particular, graph databases differ from relational databases in that the topology of data is as important as the data itself. Thus, typical graph database queries are navigational, asking whether some nodes are connected by paths satisfying some specific properties.
While relational databases were designed upon logical and algebraic foundations, the development of graph databases has been quite ad-hoc. In this sense, the aim of this paper is to provide them with some logical foundations. More precisely, in previous work we introduced a navigational logic, called GNL (Graph Navigational Logic) that allows us to describe graph navigational properties, and which is equipped with a deductive tableau method that we proved to be sound and complete.
In this presentation we will introduce a new formal model for property graphs. Then, we will show how graph queries à la Cypher can be expressed using a fragment of GNL, defining for them a logical and an operational semantics, based on the inference rules for GNL. Finally, we show that both semantics are equivalent.

This presentation outlines some ideas of my PhD about Global Transformations. These form a general method to describe local and synchronous spatialized dynamical systems such as Cellular Automata and Lindenmayer systems. This work originated from the goal of extending such systems to dynamical graphs. This talk first introduces the categorical formalism, and providing examples of such systems over different structures such as words or graphs. It also give simple instances of many categorical constructions, such as comma categories, colimits and Kan extensions. These tools are then used to relate the local specification of a system and its global behavior. The extension of this formalism to non-deterministic computations is finally considered.

Domain-specific modelling languages (DSMLs) are “little” languages that are developed for a particular domain of interest and allow capturing descriptions of problems and systems in terminology close to that domain. So-called executable DSMLs (xDSMLs) come with a high-level specification of their semantics, often as an operational semantics, so that models expressed in the xDSML can be executed directly. Graph transformations are one mechanism that can be used to capture such semantics. A challenge with xDSMLs is that a new such language needs to be developed for every new domain, making the approach potentially costly. If we were able to better reuse existing xDSMLs, we could bring the cost of language development down. One area where this is particularly interesting is in the specification and analysis of non-functional properties of systems (eg, performance properties). In this talk, I will show how such properties can be modularised into their own xDSML and how these language modules can be woven into a given base xDSML via the amalgamation of graph transformation systems. I will give an overview of the concepts and some interesting properties, and will then show GTSMorpher, a tool implementing these ideas in the Eclipse ecosystem.