Graph Transformation: 16th International Conference, ICGT 2023, Held as Part of STAF 2023, Leicester, UK, July 19–20, 2023, Proceedings (Lecture Notes in Computer Science)

Preface
Organization
Contents
Theoretical Advances
A Monoidal View on Fixpoint Checks
	1 Introduction
	2 Motivation
	3 Preliminaries
	4 A Categorical View of the Approximation Framework
	5 Predicate Liftings
	6 Wasserstein Lifting and Behavioural Metrics
		6.1 Wasserstein Lifting
		6.2 A Compositional Representation
	7 GS-Monoidality
	8 UDEfix: A Tool for Fixpoints Checks
	9 Conclusion, Related and Future Work
	References
Specification and Verification of a Linear-Time Temporal Logic for Graph Transformation
	1 Introduction
	2 Counterpart Models
		2.1 Counterpart Relations and Traces
	3 Quantified Linear Temporal Logic
		3.1 Syntax and Semantics of QLTL
		3.2 Satisfiability
		3.3 Examples
	4 Positive Normal Form for QLTL
		4.1 Semantics of PNF
		4.2 Negation of QLTL and PNF
	5 Agda Formalisation
		5.1 Formalisation Aspects
		5.2 Intuitionistic Proof Assistant
		5.3 Automation
	6 Related Works
	7 Conclusions and Future Works
	References
.28em plus .1em minus .1emFinding the Right Way to Rome: Effect-Oriented Graph Transformation
	1 Introduction
	2 Running Example
	3 Preliminaries
	4 Effect-Oriented Rules and Transformations
		4.1 Effect-Oriented Rules as Representations of Rule Sets
		4.2 Matching Effect-Oriented Rules
	5 Locally Complete Matches—Algorithm and Implementation
		5.1 An Algorithm for Computing Locally Complete Matches
		5.2 Implementation
	6 Related Work
		6.1 Benefiting from Effect-Oriented Graph Transformation
		6.2 Relations to Other Graph Transformation Approaches
	7 Conclusion
	References
Moving a Derivation Along a Derivation Preserves the Spine
	1 Introduction
	2 Preliminaries
	3 Moving Derivations Along Derivations Using Independence
		3.1 Moving Forward Using Parallel Independence
		3.2 Moving Backward Using Sequential Independence
	4 Accessed Parts, Restrictions and Spines
		4.1 Accessed Parts
		4.2 Restrictions and Spines
	5 Moving Preserves the Spine
	6 Conclusion
	References
Termination of Graph Transformation Systems Using Weighted Subgraph Counting
	1 Introduction
	2 Preliminaries
		2.1 Basic Notions
		2.2 Termination
	3 PBPO+
	4 Decreasingness by Counting Weighted Elements
		4.1 Relating Rule and Step
		4.2 Determining w(A(T, GR).5-.5.5-.5.5-.5.5-.5w)
		4.3 Sliding Tiles Injectively
		4.4 The Main Result
	5 Examples
	6 Related Work
	7 Conclusion and Future Work
	References
Fuzzy Presheaves are Quasitoposes
	1 Preliminaries
	2 Fuzzy Presheaves are Quasitoposes
		2.1 Finite Limits and Colimits
		2.2 Regular-Subobject Classifier
		2.3 Cartesian Closed
		2.4 Locally Cartesian Closed
	3 Fuzzy Presheaves are Rm-Adhesive
	4 Examples and Applications
	5 Fuzzy Simple Graphs Form a Quasitopos
	6 Conclusion
	References
.28em plus .1em minus .1emMechanised DPO Theory: Uniqueness of Derivations and Church-Rosser Theorem
	1 Introduction
	2 Isabelle/HOL
	3 DPO Graph Transformation in Isabelle
	4 Uniqueness of Direct Derivations
	5 Church-Rosser Theorem
	6 Related Work
	7 Conclusion
	References
Application Domains
Formalisation, Abstraction and Refinement of Bond Graphs
	1 Introduction
	2 Classical Physical Theories for Classical Engineering
	3 Bond Graph Basics
	4 The Category of Bond Graph Patterns BGPatt
		4.1 Commentary
	5 Bond Graph Transformation
		5.1 Rule Based Bond Graph Transformation
		5.2 Bond Graph Transformation Confluence
	6 Bond Graph Abstraction and Refinement
	7 Conclusions
	References
A Rule-Based Procedure for Graph Query Solving
	1 Introduction
	2 A Graph Query Algebra
	3 Patterns and Queries
		3.1 Patterns
		3.2 Queries
	4 A Sound and Complete Calculus
	5 Conclusion and Related Work
	References
Advanced Consistency Restoration with Higher-Order Short-Cut Rules
	1 Introduction
	2 Fundamentals
	3 Higher-Order Short-Cut Rules
		3.1 Exemplifying the Need for Higher-Order Short-Cut Rules
		3.2 Deriving Higher-Order Short-Cut Rules On-the-Fly
		3.3 Discussion
	4 Evaluation
	5 Related Work
	6 Conclusion
	References
Formalization and Analysis of BPMN Using Graph Transformation Systems
	1 Introduction
	2 Preliminaries
		2.1 BPMN
		2.2 Theoretical Background
	3 BPMN Semantics Formalization
		3.1 BPMN Execution Metamodel
		3.2 Process Instantiation and Termination
		3.3 Activities and Subprocesses
		3.4 Gateways
		3.5 Message Events
	4 Model Checking BPMN
		4.1 General BPMN Properties
		4.2 Custom Properties
	5 Implementation
		5.1 BPMN Analyzer Tool
		5.2 Experiments
	6 Related Work
	7 Conclusion and Future Work
	References
Computing k-Bisimulations for Large Graphs: A Comparison and Efficiency Analysis
	1 Introduction
	2 Related Work
	3 Preliminaries
		3.1 Data Structures
		3.2 Bisimulation
		3.3 Graph Summaries for Bisimulation
	4 Algorithms
		4.1 Native Schätzle et al. Algorithm
		4.2 Native Kaushik et al. Algorithm
		4.3 Generic BRS Algorithm
	5 Experimental Apparatus
		5.1 Datasets
		5.2 Procedure
		5.3 Implementation
		5.4 Measures
	6 Results
	7 Discussion
	8 Conclusion and Future Work
	References
Dominant Eigenvalue-Eigenvector Pair Estimation via Graph Infection
	1 Introduction
	2 Our Method: Inspired by Euler Method for Graph Infection ODE
		2.1 Graph Infection and Adjacency Matrix
		2.2 General Solution to Graph Infection ODE
		2.3 Fastest Growing Term and Perron-Frobenius Theorem
		2.4 Euler Method to Approximate Matrix ODE
		2.5 Secant Line of Euler Method
	3 Theoretical Comparison with Power Iteration
	4 Experimental Results
		4.1 Tree Graph
		4.2 Bipartite Graph
		4.3 Directed Graph with Period of Two
		4.4 Markov Chain with Spider-Trap
	5 Discussion
		5.1 Relationship with NetworkX Eigenvector-Centrality Implementation (Workaround on Power Iteration)
		5.2 Matrix-Free Implementation
		5.3 Extension to Dynamic Graphs
		5.4 Limitations
	6 Conclusion
	References
Tool Presentation
Implementing the GT Language: A Functional Language with Graphs as First-Class Data
	1 Introduction
	2 The Syntax and Semantics of GT
		2.1 Syntax of GT
		2.2 Structural Congruence
		2.3 Operational Semantics of GT
	3 Examples
	4 Implementation
	5 Related and Future Work
	References
Blue Skies
A Living Monograph for Graph Transformation
	1 Towards a Living Monograph
		1.1 Surveys in the Graph Transformation Literature
		1.2 Shortcomings of Surveys in an Active Literature
	2 Technical Challenges of a Living Monograph
		2.1 Categorical Reasoning in a Proof Assistant
		2.2 Categorical Reasoning with a Proof Assistant
	3 Advantages of a Living Monograph
	References
Graph Rewriting for Graph Neural Networks
	1 Introduction
	2 A Recommender System GReNN
	3 Discussion: GReNN Vs GNN
	References
Author Index