nach oben

2021 | Buch

Kapitel lesen Erstes Kapitel lesen

Graph Transformation

14th International Conference, ICGT 2021, Held as Part of STAF 2021, Virtual Event, June 24–25, 2021, Proceedings

herausgegeben von: Prof. Fabio Gadducci, Timo Kehrer

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 14th International Conference on Graph Transformation, ICGT 2021, which took place virtually during June 24-25, 2021.

The 14 full papers and 2 tool papers presented in this book were carefully reviewed and selected from 26 submissions. They deal with the following topics: theoretical advances; application domains; and tool presentations.

Inhaltsverzeichnis

Frontmatter

Theoretical Advances

Frontmatter

Concurrency Theorems for Non-linear Rewriting Theories

Abstract

Sesqui-pushout (SqPO) rewriting along non-linear rules and for monic matches is well-known to permit the modeling of fusing and cloning of vertices and edges, yet to date, no construction of a suitable concurrency theorem was available. The lack of such a theorem, in turn, rendered compositional reasoning for such rewriting systems largely infeasible. We develop in this paper a suitable concurrency theorem for non-linear SqPO-rewriting in categories that are quasi-topoi (subsuming the example of adhesive categories) and with matches required to be regular monomorphisms of the given category. Our construction reveals an interesting “backpropagation effect” in computing rule compositions. We derive in addition a concurrency theorem for non-linear double pushout (DPO) rewriting in rm-adhesive categories. Our results open non-linear SqPO and DPO semantics to the rich static analysis techniques available from concurrency, rule algebra and tracelet theory.

Nicolas Behr, Russ Harmer, Jean Krivine

A Generalized Concurrent Rule Construction for Double-Pushout Rewriting

Abstract

Double-pushout rewriting is an established categorical approach to the rule-based transformation of graphs and graph-like objects. One of its standard results is the construction of concurrent rules and the Concurrency Theorem pertaining to it: The sequential application of two rules can equivalently be replaced by the application of a concurrent rule and vice versa. We extend and generalize this result by introducing generalized concurrent rules (GCRs). Their distinguishing property is that they allow identifying and preserving elements that are deleted by their first underlying rule and created by the second one. We position this new kind of composition of rules among the existing ones and obtain a Generalized Concurrency Theorem for it. We conduct our work in the same generic framework in which the Concurrency Theorem has been presented, namely double-pushout rewriting in \(\mathcal {M}\)-adhesive categories via rules equipped with application conditions.

Jens Kosiol, Gabriele Taentzer

Transformations of Reaction Systems Over Categories by Means of Epi-Mono Factorization and Functors

Abstract

A categorical approach to reaction systems is a generalization and unification of the intensely studied set-based and graph-based reaction systems such that a wider spectrum of data structures becomes available on which reaction systems can be based. Many types of graphs, hypergraphs, and graph-like structures are covered. As a class of suitable categories, \( eiu \)-categories have been introduced, which are closely related to well-known adhesive categories. In this paper, transformations of reaction systems over \( eiu \)-categories by means of epi-mono factorization and functors are investigated.

Aaron Lye

Graph Rewriting and Relabeling with PBPO

Abstract

We extend the powerful Pullback-Pushout (PBPO) approach for graph rewriting with strong matching. Our approach, called PBPO\(^{+}\), exerts more control over the embedding of the pattern in the host graph, which is important for a large class of graph rewrite systems. In addition, we show that PBPO\(^{+}\) is well-suited for rewriting labeled graphs and certain classes of attributed graphs. For this purpose, we employ a lattice structure on the label set and use order-preserving graph morphisms. We argue that our approach is simpler and more general than related relabeling approaches in the literature.

Roy Overbeek, Jörg Endrullis, Aloïs Rosset

Incorrectness Logic for Graph Programs

Abstract

Program logics typically reason about an over-approximation of program behaviour to prove the absence of bugs. Recently, program logics have been proposed that instead prove the presence of bugs by means of under-approximate reasoning, which has the promise of better scalability. In this paper, we present an under-approximate program logic for a nondeterministic graph programming language, and show how it can be used to reason deductively about program incorrectness, whether defined by the presence of forbidden graph structure or by finitely failing executions. We prove this ‘incorrectness logic’ to be sound and complete, and speculate on some possible future applications of it.

Christopher M. Poskitt

Powerful and NP-Complete: Hypergraph Lambek Grammars

Abstract

We consider two approaches to generating formal string languages: context-free grammars and Lambek grammars, which are based on the Lambek calculus. They are equivalent in the sense that they generate the same set of languages (disregarding the empty word). It is well known that context-free grammars can be generalized to hyperedge replacement grammars (HRGs) preserving their main principles and properties. In this paper, we study a generalization of the Lambek grammars to hypergraphs and investigate the recognizing power of the new formalism. We show how to define the hypergraph Lambek calculus (\(\mathrm {HL}\)), and then introduce hypergraph Lambek grammars based on \(\mathrm {HL}\). It turns out that such grammars recognize all isolated-node bounded languages generated by HRGs. However, they are more powerful than HRGs: they recognize at least finite intersections of such languages. Thus the Pentus theorem along with the pumping lemma and the Parikh theorem have no place for hypergraph Lambek grammars. Besides, it can be shown that hypergraph Lambek grammars are NP-complete, so they constitute an attractive alternative to HRGs, which are also NP-complete.

Tikhon Pshenitsyn

Evaluation Diversity for Graph Conditions

Abstract

Graphs are used as a universal data structure in various domains. Sets of graphs (and likewise graph morphisms) can be specified using the graph logic

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-78946-6_7/MediaObjects/509475_1_En_7_Figa_HTML.gif

of Graph Conditions (GCs). The evaluation of a graph against a GC results in a satisfaction judgement on whether the graph is specified by the GC.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-78946-6_7/MediaObjects/509475_1_En_7_Figb_HTML.gif

is as expressive as first-order logic on graphs and infinitely many graphs may be evaluated against a given GC. Therefore, a complete compact overview of how a given GC may be evaluated for varying graphs can support GC validation, testing, debugging, and repair.

As a main contribution, we generate such an overview for a given GC in the form of a complete finite set of diverse evaluations for varying associated graphs formally given by so called Evaluation Trees (ETs). Each of these ETs concretely describes how its associated graph is evaluated against the given GC by presenting each evaluation step. The returned ETs are complete since each possible ET subsumes one of the returned ETs and diverse by not containing superfluous ETs subsuming smaller ETs. We apply an implementation of our ET generation procedure in the tool

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-78946-6_7/MediaObjects/509475_1_En_7_Figc_HTML.gif

to a running example.

Sven Schneider, Leen Lambers

Application Domains

Frontmatter

Host-Graph-Sensitive RETE Nets for Incremental Graph Pattern Matching

Abstract

Efficient querying of large graph structures is a problem at the heart of several application domains such as social networks and model driven engineering. In particular in the context of model driven engineering, where the same query is executed frequently over an evolving graph structure, incremental techniques based on discrimination networks such as RETE nets are a popular solution. However, the construction of adequate RETE nets for a specific problem instance is a challenge in and of itself. In this paper, we propose an approach to RETE net construction for queries in the form of simple graph patterns that considers not only the structure of the query, but also the structure of the graph the query is being executed over in order to improve the net’s performance with respect to execution time and memory consumption. Furthermore, we suggest a technique for adapting the net structure to changing characteristics of the underlying graph. We evaluate the presented concepts empirically based on queries and data from two independent benchmarks.

Matthias Barkowsky, Holger Giese

Rule-Based Top-Down Parsing for Acyclic Contextual Hyperedge Replacement Grammars

Abstract

Contextual hyperedge replacement (CHR) strengthens the generative power of hyperedge replacement (HR) significantly, thus increasing its usefulness for practical modeling. We define top-down parsing for CHR grammars by graph transformation, and prove that it is correct as long as the generation and use of context nodes in productions does not create cyclic dependencies. An efficient predictive version of this algorithm can be obtained as in the case of HR grammars.

Frank Drewes, Berthold Hoffmann, Mark Minas

Nets with Mana: A Framework for Chemical Reaction Modelling

Abstract

We use categorical methods to define a new flavor of Petri nets where transitions can only fire a limited number of times, specified by a quantity that we call mana. We do so with chemistry in mind, looking at ways of modelling the behavior of chemical reactions that depend on enzymes to work. We prove that such nets can be either obtained as a result of a comonadic construction, or by enriching them with extra information encoded into a functor. We then use a well-established categorical result to prove that the two constructions are equivalent, and generalize them to the case where the firing of some transitions can “regenerate” the mana of others. This allows us to represent the action of catalysts and also of biochemical processes where the byproducts of some chemical reaction are exactly the enzymes that another reaction needs to work.

Fabrizio Genovese, Fosco Loregian, Daniele Palombi

A Case Study on the Graph-Transformational Modeling and Analysis of Puzzles

Abstract

In this paper, we start a case study on the use and usefulness of graph transformation in modeling and analyzing games and puzzles beginning with logic puzzles. More explicitly, we consider Sudoku, Hashiwokakero, Arukone, and Maze aka Labyrinth. In these cases, the underlying data structures can be represented by graphs and the puzzles have start configurations and goals besides the solving rules. Sometimes it is meaningful to regulate the rule application by some control conditions. These are the ingredients of graph transformation units which are therefore applied as modeling framework. Based on the graph-transformational models, one can show that Labyrinth can be solved in polynomial time and solvability of the other three is NP-complete.

Hans-Jörg Kreowski, Aaron Lye

Interval Probabilistic Timed Graph Transformation Systems

Abstract

For complex distributed embedded probabilistic real-time systems, ensuring correctness of their software components is of great importance. The rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) allows for modeling and analysis of such systems where states can be represented by graphs and where timed and probabilistic behavior is important. In PTGTSs, probabilistic behavior is specified by assigning precise probabilities to rules. However, for embedded systems, only lower and upper probability bounds may be estimated because unknown physical effects may influence the probabilities possibly changing them over time.

In this paper, we (a) introduce the formalism of Interval Probabilistic Timed Graph Transformation Systems (IPTGTSs) in which rules are equipped with probability intervals rather than precise probabilities and (b) extend the preexisting model checking approach for PTGTSs to IPTGTSs w.r.t. worst-case/best-case probabilistic timed reachability properties using an encoding of probability intervals. Moreover, we ensure that this adapted model checking approach is applicable to IPTGTSs for which the finiteness of the state space may only be a consequence of the timing constraints. Finally, in our evaluation, we apply an implementation of our model checking approach in AutoGraph to a running example.

Maria Maximova, Sven Schneider, Holger Giese

Verifying Graph Programs with Monadic Second-Order Logic

Abstract

To verify graph programs in the language GP 2, we present a monadic second-order logic with counting and a Hoare-style proof calculus. The logic has quantifiers for GP 2’s attributes and for sets of nodes or edges. This allows to specify non-local graph properties such as connectedness, k-colourability, etc. We show how to construct a strongest liberal postcondition for a given graph transformation rule and a precondition. The proof rules establish the total correctness of graph programs and are shown to be sound. They allow to verify more programs than is possible with previous approaches. In particular, many programs with nested loops are covered by the calculus.

Gia S. Wulandari, Detlef Plump

On the Complexity of Simulating Probabilistic Timed Graph Transformation Systems

Abstract

To develop future cyber-physical systems, like networks of autonomous vehicles, the modeling and simulation of huge networks of collaborating systems acting together on large-scale topologies is required. Probabilistic Timed Graph Transformation Systems (PTGTSs) have been introduced as a means of modeling a high-level view of these systems of systems. In our previous work, we proposed a simulation scheme based on local search incremental graph matching that can handle large-scale real-world topologies. However, the prohibitive complexity of the graph matching problem underlying the simulation of any GTS variant makes this setup potentially problematic.

In this paper, we present an improved simulation algorithm and identify restrictions that hold for PTGTS high-level models of cyber-physical systems and real-world topologies, for which we can establish favorable worst-case complexity bounds. We show that the worst-case amortized complexity per simulation step is only logarithmic in the number of active collaborating systems (like vehicles) and constant concerning the size of the topology. The theoretical results are confirmed by experiments.

Christian Zöllner, Matthias Barkowsky, Maria Maximova, Holger Giese

Tool Presentations

Frontmatter

Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars

Abstract

We present a tool that checks for a given context-free graph grammar whether the corresponding graph reduction system in which all rules are applied backward, is confluent—a question that arises when using graph grammars to guide state space abstractions for analyzing heap-manipulating programs; confluence of the graph reduction system then guarantees the abstraction’s uniqueness. If a graph reduction system is not confluent, our tool provides symbolic representations of counterexamples to confluence, i.e., non-joinable critical pairs, for manual inspection. Furthermore, it features a heuristics-based completion procedure that attempts to turn a graph reduction system into a confluent one without invalidating the properties mandated by the abstraction framework. We evaluate our implementation on various graph grammars for verifying data structure traversal algorithms from the literature.

Ira Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte

GrapePress - A Computational Notebook for Graph Transformations

Abstract

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. Graphs and computations by graph transformations have applications in many problem domains but they are not supported by current CNs. Existing graph transformation tools require a steep learning curve and are not integrated with CNs. In order to close this gap, we have developed GrapePress a CN that incorporates graphs and computations by graph transformations. We present the fundamental concepts for GrapePress and describe its use in documenting executable experiments involving graph transformations to approach real world problems in science and engineering.

Jens H. Weber

Backmatter

Titel: Graph Transformation
herausgegeben von: Prof. Fabio Gadducci
Timo Kehrer
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-78946-6
Print ISBN: 978-3-030-78945-9
DOI: https://doi.org/10.1007/978-3-030-78946-6