Graph Transformation: 13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25–26, 2020, Proceedings (Lecture Notes in Computer Science Book 12150)

This book constitutes the refereed proceedings of the 13th International Conference on Graph Transformation, ICGT 2020, in Bergen, Norway, in June 2020.\*The 16 research papers and 4 tool paper presented in this book were carefully reviewed and selected from 40 submissions. One invited paper is also included. The papers deal with the following topics: theoretical advances; application domains; and tool presentations. \*The conference was held virtually due to the COVID-19 pandemic. Preface 6 Organization 8 Quantum Natural Language Processing (on Actual Quantum Hardware): (Abstract of Invited Paper) 10 Contents 13 Theoretical Advances 15 Conditional Bigraphs 16 1 Introduction 16 2 Bigraphs 18 2.1 Bigraphical Reactive Systems 19 3 Application Conditions for Bigraphs 21 4 Implementation 23 5 Examples 23 5.1 Uniqueness of Entities 24 5.2 Non-existence and Counting in Multisets 24 5.3 Encoding Control Flow 25 6 Discussion and Limitations 26 6.1 Matching on Names 26 6.2 Matches Can Be Too Large 27 6.3 Matching Specific Places 28 6.4 Handling Overlaps 29 6.5 Related Work 29 7 Conclusion 30 References 31 Confluence up to Garbage 33 1 Introduction 33 2 Preliminaries 34 2.1 Abstract Reduction Systems 34 2.2 Labelled Graphs and Morphisms 34 2.3 Double-Pushout Graph Transformation 35 2.4 Graph Languages 35 2.5 Confluence Checking 36 3 Closedness and Confluence up to Garbage 37 3.1 Closedness and Garbage 38 3.2 Confluence up to Garbage 38 4 Generalised Critical Pair Lemma 40 4.1 Subgraph Closure 40 4.2 Non-garbage Critical Pairs 41 4.3 Checking for Confluence up to Garbage 42 5 Language Recognition 42 5.1 Confluent Recognition 43 5.2 Extended Flow Diagrams 44 5.3 Series-Parallel Graphs 46 6 Conclusion and Future Work 47 References 48 Computing Embeddings of Directed Bigraphs 51 1 Introduction 51 2 Reactive Systems on Directed Bigraphs 52 2.1 Directed Bigraphs 52 2.2 Reactive Systems over Directed Bigraphs 55 3 Directed Bigraph Embeddings 56 4 Implementing the Embedding Problem in CSP 59 4.1 Directed Link Graphs 59 4.2 Place Graphs 63 4.3 Bigraphs 64 5 Experimental Results 65 6 Conclusions and Future Works 67 References 67 A Categorical Semantics for Guarded Petri Nets 70 1 Introduction 70 2 Guarded Nets 71 3 Internalizing Guards 73 4 Properties of Internalizations 76 5 Internalization as a Functor 80 6 Conclusion and Future Work 81 References 87 Unfolding Symbolic Attributed Graph Grammars 88 1 Introduction 88 2 Symbolic Attributed Graph Transformation 89 3 DPO Occurrence Graph Grammars and Unfolding 95 4 Attributed Occurrence Grammars 97 5 Unfolding Attributed Graph Grammars 99 6 Related Work and Conclusion 102 References 103 Single Pushout Rewriting in Comprehensive Systems 104 1 Introduction and Motivation 104 2 SPO Rewriting 106 2.1 Graph-Like Structures 106 2.2 Partial Map Categories 107 2.3 Rewriting Rule and Derivation 109 3 Comprehensive Systems 109 3.1 Definitions and Background 109 3.2 Why Must Definedness Be Reflected? 111 3.3 Important Properties 111 4 The Partial Map Category of Comprehensive Systems Admits All Pushouts 115 4.1 Upper Adjoints in General ... 115 4.2 ...and in CS 116 4.3 The Main Theorem 118 5 Related and Future Work 119 References 119 Initial Conflicts for Transformation Rules with Nested Application Conditions 122 1 Introduction 122 2 Related Work 124 3 Preliminaries 125 3.1 Graphs and High-Level Structures 125 3.2 Rules with Application Conditions and Parallel Independence 126 3.3 Critical Pairs 128 3.4 Initial Conflicts for Plain Rules 130 3.5 Initial Parallel Independent Transformation Pairs for Plain Rules 131 4 Initial Conflicts 132 4.1 Conflict Inheritance 132 4.2 Complete Subset of Conflicts 133 4.3 Initial Conflicts 133 4.4 Completeness 134 5 Unfoldings of Initial Conflicts 135 5.1 Finite and Complete Unfolding 135 5.2 Unfolding for Rules with NACs 136 6 Conclusion and Outlook 137 References 138 Patch Graph Rewriting 141 1 Introduction 141 2 Intuitive Semantics 142 3 Formal Semantics 145 4 Modeling Wait-for Graphs and Deadlock Detection 151 4.1 Wait-for Graph Grammar 152 4.2 System Modeling 152 4.3 Deadlock Detection 154 5 Comparison 154 6 Conclusion 156 References 157 Hypergraph Basic Categorial Grammars 159 1 Introduction 159 2 Basic Categorial Grammars (for Strings) 160 3 Hypergraphs and Operations on Them 161 3.1 Hypergraphs, Sub-hypergraphs 161 3.2 Operations on Graphs 162 3.3 Hyperedge Replacement Grammars 163 4 Hypergraph Basic Categorial Grammars 164 4.1 Types 164 4.2 D-Isomorphism 164 4.3 Rule () 165 4.4 Hypergraph Basic Categorial Grammar 166 5 Embedding of BCG 167 6 Equivalence of HRGs and HBCGs 168 6.1 Greibach Normal Form for HRGs 168 6.2 The Equivalence Theorems 169 7 Structural Properties 170 7.1 HBCGs with One Primitive Type 170 7.2 Counters 171 8 Lambda Semantics 172 9 Cross-serial Dependencies 172 10 Conclusions and Related Work 174 References 175 Multilevel Typed Graph Transformations 176 1 Introduction 176 2 Typing Chains and Multilevel Typing of Graphs 178 3 Multilevel Typed Graph Transformations 182 4 Conclusions, Related and Future Work 192 References 193 Application Domains 196 Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics 197 1 Motivation 197 2 Compositional Rewriting Theories with Conditions 198 2.1 Category-Theoretical Prerequisites 198 2.2 Conditions 200 2.3 Compositional Rewriting with Conditions 200 3 Rule Algebras for Compositional Rewriting with Conditions 202 4 Stochastic Mechanics Formalism 204 5 Application Scenario 1: Biochemistry with Kappa 208 6 Application Scenario 2: Organic Chemistry with MØD 211 7 Conclusion and Outlook 212 References 213 Algebras for Tree Decomposable Graphs 215 1 Introduction 215 2 Background 217 2.1 Strong Network Algebras 218 2.2 Tree Decomposition 220 3 Loose Specification 221 3.1 Initial Loose Algebra of Binding Bigraphs 221 4 Dynamic Programming 223 4.1 Networks as Optimisation Problems 223 4.2 Evaluation Complexity 224 4.3 Elementary Tree Decompositions 226 4.4 A Type System for l-canonical Terms 227 4.5 Computing l-canonical Forms 229 5 Conclusion 230 References 231 Graph Parsing as Graph Transformation 233 1 Introduction 233 2 Preliminaries 234 3 Hyperedge Replacement Graph Grammars 236 4 Threaded HR Grammars 237 5 General Top-Down Parsing for HR Grammars 241 6 Predictive Top-Down Parsing for HR Grammars 245 7 Conclusions 248 References 249 Graph Consistency as a Graduated Property 251 1 Introduction 251 2 Example 253 3 Preliminaries 254 4 Consistency-Sustaining and Consistency-improving Rules and Transformations 257 4.1 Partial Consistency 257 4.2 Consistency Sustainment and Improvement 258 4.3 Direct Consistency Sustainment and Improvement 259 5 Static Analysis for Direct Consistency Sustainment and Improvement 262 6 Related Work 265 7 Conclusions 266 References 267 Formal Verification of Invariantspg for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions 269 1 Introduction 269 2 Invariant Verification Using k-Induction 271 3 Modelling and Specifying Graph Transformation 274 4 Invariant Analysis for Graph Transformation Systems 280 5 Conclusion and Future Work 285 References 285 Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic 288 1 Introduction 288 2 Symbolic Graphs and Graph Logic 290 3 Metric Temporal Graph Logic 292 4 On-the-fly Analysis for MTGL 295 5 Related Work 303 6 Conclusion and Future Work 304 References 304 Tool Presentations 307 A Flexible and Easy-to-Use Library for the Rapid Development of Graph Tools in Java 308 1 Introduction 308 2 Components and Features 310 2.1 Components Overview 310 2.2 Detailed Description of the Java-Graph Component 311 3 Existing Tools Using the Library 313 3.1 DPOdactic 313 3.2 DrAGoM 314 3.3 Grez 314 3.4 Further Tools 315 4 Future Work 315 References 316 Multiscale Graph Grammars Can Generate Cayley Graphs of Groups and Monoids 318 1 Introduction 318 2 Method and Result 319 2.1 The Graph Model 319 2.2 The Grammar 320 3 Discussion 325 References 326 The Glasgow Subgraph Solver: Using Constraint Programming to Tackle Hard Subgraph Isomorphism Problem Variants 327 1 Introduction 327 2 Subgraph Isomorphism Problems and Variants 328 3 The Glasgow Subgraph Solver 329 3.1 Algorithmic Details 329 3.2 Future Directions 332 References 333 A Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies 336 1 Introduction 336 2 Preliminaries 337 3 Simulator 340 3.1 Simulation Engine 340 3.2 Generation of GT Type Graph and Rules 342 4 Evaluation 343 5 Conclusion and Future Work 344 References 344 Author Index 346 Front Matter ....Pages i-xiv Front Matter ....Pages 1-1 Conditional Bigraphs (Blair Archibald, Muffy Calder, Michele Sevegnani)....Pages 3-19 Confluence up to Garbage (Graham Campbell, Detlef Plump)....Pages 20-37 Computing Embeddings of Directed Bigraphs (Alessio Chiapperini, Marino Miculan, Marco Peressotti)....Pages 38-56 A Categorical Semantics for Guarded Petri Nets (Fabrizio Genovese, David I. Spivak)....Pages 57-74 Unfolding Symbolic Attributed Graph Grammars (Maryam Ghaffari Saadat, Reiko Heckel, Fernando Orejas)....Pages 75-90 Single Pushout Rewriting in Comprehensive Systems (Harald König, Patrick Stünkel)....Pages 91-108 Initial Conflicts for Transformation Rules with Nested Application Conditions (Leen Lambers, Fernando Orejas)....Pages 109-127 Patch Graph Rewriting (Roy Overbeek, Jörg Endrullis)....Pages 128-145 Hypergraph Basic Categorial Grammars (Tikhon Pshenitsyn)....Pages 146-162 Multilevel Typed Graph Transformations (Uwe Wolter, Fernando Macías, Adrian Rutle)....Pages 163-182 Front Matter ....Pages 183-183 Rewriting Theory for the Life Sciences: A Unifying Theory of CTMC Semantics (Nicolas Behr, Jean Krivine)....Pages 185-202 Algebras for Tree Decomposable Graphs (Roberto Bruni, Ugo Montanari, Matteo Sammartino)....Pages 203-220 Graph Parsing as Graph Transformation (Frank Drewes, Berthold Hoffmann, Mark Minas)....Pages 221-238 Graph Consistency as a Graduated Property (Jens Kosiol, Daniel Strüber, Gabriele Taentzer, Steffen Zschaler)....Pages 239-256 Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions (Sven Schneider, Johannes Dyck, Holger Giese)....Pages 257-275 Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic (Sven Schneider, Lucas Sakizloglou, Maria Maximova, Holger Giese)....Pages 276-294 Front Matter ....Pages 295-295 A Flexible and Easy-to-Use Library for the Rapid Development of Graph Tools in Java (H. J. Sander Bruggink, Barbara König, Marleen Matjeka, Dennis Nolte, Lars Stoltenow)....Pages 297-306 Multiscale Graph Grammars Can Generate Cayley Graphs of Groups and Monoids (Winfried Kurth)....Pages 307-315 The Glasgow Subgraph Solver: Using Constraint Programming to Tackle Hard Subgraph Isomorphism Problem Variants (Ciaran McCreesh, Patrick Prosser, James Trimble)....Pages 316-324 A Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies (Christian Zöllner, Matthias Barkowsky, Maria Maximova, Melanie Schneider, Holger Giese)....Pages 325-334 Back Matter ....Pages 335-335 This book constitutes the refereed proceedings of the 13th International Conference on Graph Transformation, ICGT 2020, in Bergen, Norway, in June 2020.* The 16 research papers and 4 tool paper presented in this book were carefully reviewed and selected from 40 submissions. One invited paper is also included. The papers deal with the following topics: theoretical advances; application domains; and tool presentations. *The conference was held virtually due to the COVID-19 pandemic.