Search

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.

In order to define graph transformations by the simultaneous application of concurrent rules, we have adopted in previous work a structure of attributed graphs stable by unions. We analyze the consequences on parallel independence, a property that characterizes the possibility to resort to sequential rewriting. This property turns out to depend not only on the left-hand side of rules, as in algebraic approaches to graph rewriting, but also on their right-hand side. It is then shown that, of three possible definitions of parallel rewriting, only one is convenient in the light of parallel independence., Comment: In Proceedings TERMGRAPH 2020, arXiv:2102.01804

The paper presents a new application of the graph model of the game world and graph rules describing players’ actions in this world. This time, this model and rules are used to design storylines in multiplayer role-playing games. The proposed model is suitable for collaborative plot design, as the set of rules describing game actions can be divided into subsets corresponding to particular quests, which are then assigned to different plot writers. The main contributions of this paper are: firstly, a new type of graph transformation rules for construction of storylines in games that require competition or collaboration between multiple players, and secondly, a prototype networked application to validate the proposed ideas and to serve as a playtesting tool for the designed sets of rules. In the presented application, the graph world model is stored in a Neo4j graph database server. Application instances running on players’ computers communicate with this server. The paper presents the application’s operation on an example of a simple two-player game.

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.

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.

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.

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.

This paper deals with a Computer-Aided Design (CAD) tool supporting the conceptual phase of the design process. Design drawings are created by the designer with the use of a visual editor. It is possible to interactively define design requirements and/or visual design patterns, which are important features for expected/required characteristics of the task solution. Design drawings, requirements, and specified visual patterns have their internal graph representations, which are automatically obtained during the design process. Based on design actions taken by the designer during the design process, graph transformation rules, which are used to derive graphs representing design objects, are constructed. Additional graph transformation rules are created on the ground of design patterns and requirements specified by the designer. The obtained set of graph transformation rules, called a graph transformation system, is used to automatically generate graphs corresponding to new objects. The approach is illustrated by examples of designing indoor swimming pools.

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.

Current models of graph understanding typically address the encoding and interpretive processes involved during the course of comprehension and largely focus on the visual properties of the graph. An experiment comparing reasoning with two types of graph is presented. On the basis and scope of existing models, performance with the two graphs would not be predicted to differ substantially. There are substantial computational differences between the graphs, however. It is suggested, therefore, that an adequate model of graph use must incorporate different combinations of visual properties of the graphs, levels of graph complexity, interpretive schemas and task requirements.

13th International Workshop, WRLA 2020, Virtual Event, October 20-22, 2020, Revised Selected Papers; International audience; We define two graph transformations, one by parallelizing graph rewrite rules, the other by taking quotients of graphs. The former consists in the exhaustive application of local transformations defined by graph rewrite rules expressed in a set-theoretic framework. Compared with other approaches to parallel rewriting, we allow a substantial amount of overlapping only restricted by a condition called the effective deletion property. This transformation can be reduced by factoring out possibly many equivalent matchings by the automorphism groups of the rules. The second transformation is based on the use of equivalence relations over graph items and offers a new way of performing simultaneous merging operations. The relevance of combining the two transformations is illustrated on a running example.

We consider the recommendations of the World Wide Web Consortium (W3C) about RDF framework and its associated query language SPARQL. We propose a new formal framework based on category theory which provides clear and concise formal definitions of the main basic features of RDF and SPARQL. We define RDF graphs as well as SPARQL basic graph patterns as objects of some nested categories. This allows one to clarify, in particular, the role of blank nodes. Furthermore, we consider basic SPARQL CONSTRUCT and SELECT queries and formalize their operational semantics following a novel algebraic graph transformation approach called POIM., Comment: In Proceedings GCM 2020, arXiv:2012.01181. arXiv admin note: substantial text overlap with arXiv:1910.07519

International audience; This paper introduces SetUp, a theoretical and applied framework for the management of RDF/S database evolution on the basis of graph rewriting rules. Rewriting rules formalize instance or schema changes, ensuring graph’s consistency with respect to given constraints. Constraints considered in this paper are a well known variant of RDF/S semantic, but the approach can be adapted to user-defined constraints. Furthermore, SetUp manages updates by ensuring rule applicability through the generation of side-effects: new updates which guarantee that rule application conditions hold.We provide herein formal validation and experimental evaluation of SetUp.

This paper provides the results of experiments on process trees reconstruction using graph rewriting-based method, that is theoretically proved to reconstruct in polynomial time any configuration of process tree with different process' identifiers, sessions, process groups, reverse reparents and attributes with the same semantics of process tree changing. The datasets for experiments were generated synthetically, according to standard process' configurations in cases of terminal job control and daemon activity. Graph rewriting-based method results is compared with profiling results both on time-costs and reconstruction results. The corresponding experimental software package is also discussed in the paper.

model checking techniques are often used for the verification of software systems. Such techniques are accompanied with several advantages. However, state space explosion is one of the drawbacks to model checking. During recent years, several methods have been proposed based on evolutionary and meta-heuristic algorithms to solve this problem. In this paper, a hybrid approach is presented to cope with the SSE problem in model checking of systems modeled by GTS with an ample state space. Most of existence proposed methods that aim to verify systems are applied to detect deadlocks by graph transformations. The proposed approach is based on the fuzzy genetic algorithm and is designed to decline the safety property by verifying the reachability property and detecting deadlocks. In this solution, the state space of the system is searched by a fuzzy genetic algorithm to find the state in which the specified property is refuted/verified. To implement and evaluate the suggested approach, GROOVE is used as a powerful designing and model checking toolset in GTS. The experimental results indicate that the presented hybrid fuzzy method improves speed and performance by comparing other techniques

We present a proof-theoretic analysis of the logic NLλ (Barker & Shan 2014, Barker 2019). We notably introduce a novel calculus of proof nets and prove it is sound and complete with respect to the sequent calculus for the logic. We study decidability and complexity of the logic using this new calculus, proving a new upper bound for complexity of the logic (showing it is in NP) and a new lower bound for the class of formal language generated by the formalism (mildly context-sensitive languages extended with a permutation closure operation). Finally, thanks to this new calculus, we present a novel comparison between NLλ and the hybrid type-logical grammars of Kubota & Levine (2020). We show there is an unexpected convergence of the natural language analyses proposed in the two formalism. In addition to studying the proof-theoretic properties of NLλ, we greatly extends its linguistic coverage.

In this paper, we combine ideas from two different scientific traditions: 1) graph transformation systems (GTSs) stemming from the theory of formal languages and concurrency, and 2) mean field approximations (MFAs), a collection of approximation techniques ubiquitous in the study of complex dynamics. Using existing tools from algebraic graph rewriting, as well as new ones, we build a framework which generates rate equations for stochastic GTSs and from which one can derive MFAs of any order (no longer limited to the humanly computable). The procedure for deriving rate equations and their approximations can be automated. An implementation and example models are available online at https://rhz.github.io/fragger. We apply our techniques and tools to derive an expression for the mean velocity of a two-legged walker protein on DNA., Comment: to be presented at the 18th International Conference on Computational Methods in Systems Biology (CMSB 2020)

The autonomic composition of Virtual Networks (VNs) and Service Function Chains (SFCs) based on application requirements is significant for complex environments. In this paper, we use graph transformation in order to compose an Extended Virtual Network (EVN) that is based on different requirements, such as locations, low latency, redundancy, and security functions. The EVN can represent physical environment devices and virtual application and network functions. We build a generic Virtual Network Embedding (VNE) framework for transforming an Application Request (AR) to an EVN. Subsequently, we define a set of transformations that reflect preliminary topological, performance, reliability, and security policies. These transformations update the entities and demands of the VN and add SFCs that include the required Virtual Network Functions (VNFs). Additionally, we propose a greedy proactive heuristic for path-independent embedding of the composed SFCs. This heuristic is appropriate for real complex environments, such as industrial networks. Furthermore, we present an Industrail Internet of Things (IIoT) use case that was inspired by Industry 4.0 concepts, in which EVNs for remote asset management are deployed over three levels, manufacturing halls and edge and cloud computing. We also implement the developed methods in Alevin and show exemplary mapping results from our use case. Finally, we evaluate the chain embedding heuristic while using a random topology that is typical for such a use case, and show that it can improve the admission ratio and resource utilization with minimal overhead.

We present new algorithms to compute candidate keys and third normal form design of a relational database schema, using strategic port graph rewriting. More precisely, we define port graph rewriting rules and strategies that implement a candidate key definition and Ullman’s algorithm to decompose a relation schema into lossless 3NF schemata. We show the correctness of the resulting database schema by proving soundness, completeness and termination of our strategic graph programs. These rules and strategies provide a declarative and visual description of the algorithms, and permit a fine-grained analysis of the computation steps involved in the normalisation process. The algorithms have been implemented in Porgy, a visual, interactive modelling tool.

Quantitative and qualitative data derived from the analysis of genomes, genes, proteins or metabolites from tissue or cells are currently generated in huge volumes during biomedical research. Graphia is an open-source platform created for the graph-based analysis of such complex data, e.g. transcriptomics, proteomics, genomics data. The software imports data already defined as a network or a similarity matrix and is designed to rapidly visualise very large graphs in 2D or 3D space, providing a wide range of functionality for graph exploration. An extensive range of analysis algorithms, routines for graph transformation, and options for the visualisation of node and edge attributes are also available. Graphia’s core is extensible through the deployment of plugins, supporting rapid development of additional computational analyses and features necessary for a given analysis task or data source. A plugin for correlation network analysis is distributed with the core application, to support the generation of correlation graphs from any tabular matrix of continuous or discrete values. This provides a powerful analysis solution for the interpretation of high-dimensional data from many sources. Several use cases of Graphia are described, to showcase its wide range of applications. Graphia runs on all major desktop operating systems and is freely available to download fromhttps://graphia.app/.

The task of automatically extracting insights or building computational models fromknowledge on complex systems greatly relies on the choice of appropriate representation.This work makes an effort towards building a framework suitable for representation offragmented knowledge on complex systems and its semi-automated curation---continuouscollation, integration, annotation and revision.We propose a knowledge representation system based on hierarchies of graphs relatedwith graph homomorphisms. Individual graphs situated in such hierarchies representdistinct fragments of knowledge and the homomorphisms allow relating these fragments.Their graphical structure can be used efficiently to express entities and their relations. Wefocus on the design of mathematical mechanisms, based on algebraic approaches to graphrewriting, for transformation of individual graphs in hierarchies that maintain consistentrelations between them. Such mechanisms provide a transparent audit trail, as well as aninfrastructure for maintaining multiple versions of knowledge.We describe how the developed theory can be used for building schema-aware graphdatabases that provide schema-data co-evolution capabilities. The proposed knowledgerepresentation framework is used to build the KAMI (Knowledge Aggregation and ModelInstantiation) framework for curation of cellular signalling knowledge. The frameworkallows for semi-automated aggregation of individual facts on protein-protein interactionsinto knowledge corpora, reuse of this knowledge for instantiation of signalling models indifferent cellular contexts and generation of executable rule-based models., L'extraction automatique des intuitions et la construction de modèles computationnels à partir de connaissances sur des systèmes complexes repose largement sur le choix d'une représentation appropriée. Ce travail s'efforce de construire un cadre adapté pour la représentation de connaissances fragmentées sur des systèmes complexes et sa curation semi-automatisé.Un système de représentation des connaissances basé sur des hiérarchies de graphes liés à l'aide d'homomorphismes est proposé. Les graphes individuels représentent des fragments de connaissances distincts et les homomorphismes permettent de relier ces fragments. Nous nous concentrons sur la conception de mécanismes mathématiques,basés sur des approches algébriques de la réécriture de graphes, pour la transformation de graphes individuels dans des hiérarchies qui maintient des relations cohérentes entre eux.De tels mécanismes fournissent une piste d'audit transparente, ainsi qu'une infrastructure pour maintenir plusieurs versions des connaissances.La théorie développée est appliquée à la conception des schémas pour les bases de données orientée graphe qui fournissent des capacités de co-évolution schémas-données.Ensuite, cette théorie est utilisée dans la construction du cadre KAMI, qui permet la curation des connaissances sur la signalisation dans les cellules. KAMI propose des mécanismes pour une agrégation semi-automatisée de faits individuels sur les interactions protéine-protéine en corpus de connaissances, la réutilisation de ces connaissances pour l'instanciation de modèles de signalisation dans différents contextes cellulaires et la génération de modèles exécutables basés sur des règles.

Today's computing world features a growing number of cyber-physical systems that require the cooperation of many physical devices. Examples include autonomous cars and co-working robots, which are expected to appropriately adapt to any possible context they find themselves in (e.g. the presence of a nearby human). However, the controlling software continues to be developed using established object-oriented modelling techniques like UML, which do not natively possess a notion of context and thus may introduce accidental complexity. With increasing complexity, the probability of the introduction of software errors rises, which can have fatal consequences in cyber-physical systems. To address this, we envision a model-driven architecture for self-adaptive cyber-physical systems that explicitly models structured context. Entities are modelled as message-passing parallel processes and can play roles in specific contexts, which dynamically alter their behaviour and relationships with other parts of the system. Since the planning of complex adaptations can be cumbersome in real-world scenarios, we envision an intuitive formulation of adaptations as graph rewriting rules on the context model. This paper discusses the current state of research and identifies open research challenges. Based on this, the envisioned architecture as well as an evaluation strategy are presented.

With the wide application of graph theory in circuit layout, signal flow chart and power system, more and more attention has been paid to the network topology analysis method of graph theory. In this paper, we construct a graph transformation which can reflect the monotonicity of coefficients and reduce the number of graphs. A sharp lower bound for incidence energy in the tricyclic graphs is given and all the extremal structures are characterized. The most interesting things that we find two different classes tricyclic graphs have the same signless Laplacian characteristic polynomials and one of the extremal graphs beyond all expectations.

Recent advances in Graph Convolutional Neural Networks (GCNNs) have shown their efficiency for non-Euclidean data on graphs, which often require a large amount of labeled data with high cost. It it thus critical to learn graph feature representations in an unsupervised manner in practice. To this end, we propose a novel unsupervised learning of Graph Transformation Equivariant Representations (GraphTER), aiming to capture intrinsic patterns of graph structure under both global and local transformations. Specifically, we allow to sample different groups of nodes from a graph and then transform them node-wise isotropically or anisotropically. Then, we self-train a representation encoder to capture the graph structures by reconstructing these node-wise transformations from the feature representations of the original and transformed graphs. In experiments, we apply the learned GraphTER to graphs of 3D point cloud data, and results on point cloud segmentation/classification show that GraphTER significantly outperforms state-of-the-art unsupervised approaches and pushes greatly closer towards the upper bound set by the fully supervised counterparts. The code is available at: https://github.com/gyshgx868/graph-ter.

Kinetic transition networks (KTNs) of local minima and transition states are able to capture the dynamics of numerous systems in chemistry, biology, and materials science. However, extracting observables is numerically challenging for large networks and generally will be sensitive to additional computational discovery. To have any measure of convergence for observables, these sensitivities must be regularly calculated. We present a matrix formulation of the discrete path sampling framework for KTNs, deriving expressions for branching probabilities, transition rates, and waiting times. Using the concept of the quasi-stationary distribution, a clear hierarchy of expressions for network observables is established, from exact results to steady-state approximations. We use these results in combination with the graph transformation method to derive the sensitivity, with respect to perturbations of the known KTN, giving explicit terms for the pairwise sensitivity and discussing the pathwise sensitivity. These results provide guidelines for converging the network, with respect to additional sampling, focusing on the estimates obtained for the overall rate coefficients between product and reactant states. We demonstrate this procedure for transitions in the double-funnel landscape of the 38-atom Lennard-Jones cluster.

Graph canonization (that solves also the graph isomorphism question) is an old problem that still attracts a lot of attention today, mainly because of the ubiquitous aspect of graph-based structures in computer science applications. This article present the proofs of correctness for the SCOTT algorithm, a graph canonization algorithm designed to provide a Canonical form for general graphs, namely graphs for which vertices and edges are coloured (labelled). These proofs ensure that the three canonical forms provided by SCOTT are valid, namely a canonical adjacency matrix, a canonical rooted tree (or DAG) and a canonical string. In addition, some crude lower and upper complexity bounds are presented and discussed. Finally some empirical evaluation is provided on a difficult synthetic benchmark with some comparison with the state of the art algorithms.

International audience; This paper presents an approach to automatically and transparently parallelize algorithms to build 2D or 3D virtual objects in geometric modeling: In particular, we show that subdivision and Iterated Function System constructions can be parallelized, without any explicit parallelization study by their developer. These operations are described in the framework Jerboa, where each operation is expressed as a graph transformation and objects are topologically described using generalized maps. All transformations are handled by a generic engine that can handle structure changes in parallel. The obtained results allow any designer of virtual environments to rely on modern multi-core and multi-processor architectures to get faster constructions of complex objects without any skills on parallelism.

The termination issue we tackle is rooted in natural language processing where graph rewriting systems (GRS) may contain a large number of rules, often in the order of thousands. Decidable concepts thus become mandatory to verify the termination of such systems. The notion of graph rewriting consider does not make any assumption on the structure of graphs (they are not “term graphs”, “port graphs” nor drags). The lack of algebraic structure in our setting led us to proposing two orders on graphs inspired from language theory: the matrix multiset-path order and the rational embedding order. We show that both are stable by context, which we then use to obtain the main contribution of the paper: under a suitable notion of “interpretation”, a GRS is terminating if and only if it is compatible with an interpretation.

The double pushout approach for graph transformation naturally allows an abstraction level of biochemical systems in which individual atoms of molecules can be traced automatically within chemical reaction networks. Aiming at a mathematical rigorous approach for isotope labeling design, we convert chemical reaction networks (represented as directed hypergraphs) into transformation semigroups. Symmetries within molecules correspond to permutations, whereas (not necessarily invertible) chemical reactions define the transformations of the semigroup. An approach for the automatic inference of informative labeling of atoms is presented, which allows to distinguish the activity of different pathway alternatives within reaction networks. To illustrate our approaches, we apply them to the reaction network of glycolysis, which is an important and well-understood process that allows for different alternatives to convert glucose into pyruvate.

This special issue contains extended versions of four selected papers from the 11th International Conference on Graph Transformation (ICGT 2018). The articles cover a tool for computing core graphs via SAT/SMT solvers (graph language definition), graph transformation through graph surfing in reaction systems (a new graph transformation formalism), the essence and initiality of conflicts in M -adhesive transformation systems, and a calculus of concurrent graph-rewriting processes (theory on conflicts and parallel independence).

International audience; Graph transformation is a specification technique suitable for a wide range of applications, specially the ones that require a sophisticated notion of state. In graph transformation, states are represented by graphs and actions are specified by rules. Most algebraic approaches to graph transformation proposed in the literature ensure that if an item is preserved by a rule, so are its connections with the graph where it is embedded. But there are applications in which it is desirable to specify different embeddings. For example when cloning an item, there may be a need to handle the original and the copy in different ways. We propose a new algebraic approach to graph transformation, AGREE: Algebraic Graph Rewriting with controllEd Embedding, where rules allow one to specify how the embedding should be carried out. We define this approach in the framework of classified categories which are categories endowed with partial map classifiers. This new approach leads to graph transformations in which effects may be non-local, e.g. a rewrite step may alter a node of the host graph which is outside the image of the left-hand side of the considered rule. We propose a syntactic condition on AGREE rules which guarantees the locality of transformations. We also compare AGREE with other algebraic approaches to graph transformation.

We build on the correspondence between Petri nets and free symmetric strict monoidal categories already investigated in the literature, and present a categorical semantics for Petri nets with guards. This comes in two flavors: Deterministic and with side-effects. Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself.

Implementing graph algorithms efficiently in a rule-based language is challenging because graph pattern matching is expensive. In this paper, we present a number of linear-time implementations of graph algorithms in GP 2, an experimental programming language based on graph transformation rules which aims to facilitate program analysis and verification. We focus on two classes of rule-based graph programs: graph reduction programs which check some graph property, and programs using a depth-first search to test some property or perform an operation such as producing a 2-colouring or a topological sorting. Programs of the first type run in linear time without any constraints on input graphs while programs of the second type require input graphs of bounded degree to run in linear time. Essential for achieving the linear time complexity are so-called rooted rules in GP 2, which, in many situations, can be matched in constant time. For each of our programs, we prove both correctness and complexity, and also give empirical evidence for their run time., Comment: 47 pages, 2020

Graph-based reaction systems were recently introduced as a generalization of the intensely studied set-based reaction systems. They deal with simple edge-labeled directed graphs, and dynamic semantics of graph-based reaction systems is defined by graph surfing as a novel kind of graph transformation where, in a single surf step, reactions are applied to a subgraph of a given background graph yielding a successor subgraph. In this paper, we propose a categorical approach to reaction systems so that a wider spectrum of data structures becomes available on which reaction systems can be based. In this way, many types of graphs, hypergraphs, and graph-like structures are covered., Comment: In Proceedings GCM 2020, arXiv:2012.01181

We extend the theory of initial conflicts in the framework of \(\mathcal {M}\)-adhesive categories to transformation rules with ACs. We first show that for rules with ACs, conflicts are in general neither inherited from a bigger context any more, nor is it possible to find a finite and complete subset of finite conflicts as illustrated for the category of graphs. We define initial conflicts to be special so-called symbolic transformation pairs, and show that they are minimally complete (and in the case of graphs also finite) in this symbolic way. We show that initial conflicts represent a proper subset of critical pairs again. We moreover demonstrate that (analogous to the case of rules without ACs) for each conflict a unique initial conflict exists representing it. We conclude with presenting a sufficient condition illustrating important special cases for rules with ACs, where we do not only have initial conflicts being complete in a symbolic way, but also find complete (and in the case of graphs also finite) subsets of conflicts in the classical sense.

The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of the system from one state to another is described by a finite set of graph transformation rules. GTSs with small finite state spaces can be analyzed with ease but analysis is intractable/undecidable for GTSs inducing large/infinite state spaces due to the inherent expressiveness of GTSs. Hence, automatic analysis procedures do not terminate or return indefinite or incorrect results.

Future cyber-physical systems, like networks of autonomous vehicles, will result in a huge number of collaborating systems acting together on large-scale topologies. Modeling them requires capturing timed and probabilistic behavior as well as structure dynamics. In [9], we introduced Probabilistic Timed Graph Transformation Systems (PTGTSs) as a means of modeling a high-level view of these systems of systems and provided model checking support. However, given the scale of emerging systems of systems and their often complex topologies, analyzing only small or medium size models using model checking is insufficient. To close this gap, we developed a simulator for PTGTSs that can import real-world topologies, automatically detect violations of state properties, and handle the graph pattern matching as well as time and probabilities efficiently so that complex large-scale topologies can be considered.

With the rapid growth of Internet media, content tagging has become an important topic with many multimedia understanding applications, including efficient organisation and search. Nevertheless, existing visual tagging approaches are susceptible to inherent privacy risks in which private information may be exposed unintentionally. The use of anonymisation and privacy-protection methods is desirable, but with the expense of task performance. Therefore, this paper proposes an end-to-end framework (SGTN) using Graph Transformer and Convolutional Networks to significantly improve classification and privacy preservation of visual data. Especially, we employ several mechanisms such as differential privacy based graph construction and noise-induced graph transformation to protect the privacy of knowledge graphs. Our approach unveils new state-of-the-art on MS-COCO dataset in various semi-supervised settings. In addition, we showcase a real experiment in the education domain to address the automation of sensitive document tagging. Experimental results show that our approach achieves an excellent balance of model accuracy and privacy preservation on both public and private datasets.

The Kappa biochemistry and the M{\O}D organo-chemistry frameworks are amongst the most intensely developed applications of rewriting theoretical methods in the life sciences to date. A typical feature of these types of rewriting theories is the necessity to implement certain structural constraints on the objects to be rewritten (a protein is empirically found to have a certain signature of sites, a carbon atom can form at most four bonds, ...). In this paper, we contribute to the theoretical foundations of these types of rewriting theory a number of conceptual and technical developments that permit to implement a universal theory of continuous-time Markov chains (CTMCs) for stochastic rewriting systems. Our core mathematical concepts are a novel rule algebra construction for the relevant setting of rewriting rules with conditions, both in Double- and in Sesqui-Pushout semantics, augmented by a suitable stochastic mechanics formalism extension that permits to derive dynamical evolution equations for pattern-counting statistics., Comment: 18+6 pages, LNCS style; ICGT 2020 conference paper extended version

Hyperedge replacement (HR) allows to define context-free graph languages, but parsing is NP-hard in the general case. Predictive top-down (PTD) is an efficient, backtrack-free parsing algorithm for subclasses of HR and contextual HR grammars, which has been described and implemented in earlier work, based on a representation of graphs and grammar productions as strings. In this paper, we define PTD parsers for HR grammars by graph transformation rules and prove that they are correct.

When software systems evolve, their model-level representations have to evolve with them to maintain consistency. A program change, for example, may induce a change to its control flow graph. The application of a design pattern may result in a change to the class structure of a software component. A new requirement may introduce a change to the associated analysis model. Since these models are based on graphs, this raises the need for a systematic specification, implementation and analysis of graph manipulations.

We present a programming library for the rapid development of graph tools, with applications in graph transformation and related fields. Features include working with graphs, graph morphisms, basic categorical constructions such as computing pushouts and pushout complements or enumerating all morphisms with certain properties, but also applications such as executing graph transformation steps. Additionally, we offer graphical user interface widgets for visualization and manipulation of graphs, morphisms and categorical diagrams. Our objective is to allow users to quickly develop graph tools for both simple and complex problems, to allow easy embedding into existing software, and to have comprehensible code especially for the main algorithms. Existing tools that demonstrate the versatility and ease of use of the library include: DPOdactic (a didactic tool for teaching double-pushout graph transformation), DrAGoM (a tool to handle multiply annotated type graphs for abstract graph rewriting), and Grez (termination analysis of graph transformation systems). © 2020, Springer Nature Switzerland AG.

One motivation for software models is the ability to analyse them, for example to validate requirements and verify the consistency of models with each other or with respect to an implementation. Since we want to use graph transformation systems as software engineering models, we have to provide analysis techniques to answer questions about these systems that arise in their applications to software engineering problems.

In Domain-Specific Modelling (DSM) the general goal is to provide Domain-Specific Modelling Languages (DSMLs) for domain users to model systems using concepts and notations they are familiar with, in their problem domain. Verifying whether a model satisfies a set of requirements is considered to be an important challenge in DSM, but is nevertheless mostly neglected. We present a solution in the form of ProMoBox, a framework that integrates the definition and verification of temporal properties in discrete-time behavioural DSMLs, whose semantics can be described as a schedule of graph rewrite rules. Thanks to the expressiveness of graph rewriting, this covers a very large class of problems. With ProMoBox, the domain user models not only the system with a DSML, but also its properties, input model, run-time state and output trace. A DSML is thus comprised of five sublanguages, which share domain-specific syntax, and are generated from a single metamodel. Generic transformations to and from a verification backbone ensure that both the language engineer and the domain user are shielded from underlying notations and techniques. We explicitly model the ProMoBox framework's process in the paper. Furthermore, we evaluate ProMoBox to assert that it supports the specification and verification of properties in a highly flexible and automated way.

The concept of adverse conditions addresses systems interacting with an adversary environment and finds use also in the development of new technologies. We present an approach for modeling adverse conditions by graph transformation systems. In contrast to other approaches for graph-transformational interacting systems, the presented main constructs are graph transformation systems. We introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we introduce notions of (partial) correctness under adverse conditions, which contain the correctness of the system and a recovery condition. As main result, we show that two instances of correctness, namely k-step correctness (recovery in at most k steps after an environment intervention) and last-minute correctness (recovery until next environment intervention) are expressible in LTL (linear temporal logic), and that a weaker notion of k-step correctness is expressible in CTL (computation tree logic)., Comment: In Proceedings GCM 2020, arXiv:2012.01181

In conceptual design of any engineering system, decisions are made regarding which technologies to include and where. One of the first stages of that process is constructing the technology compatibility matrix (TCM), which indicates the compatibility of each pair in a technology set. Rather than constructing a TCM with expert judgment, this study develops a method based on graph transformation rules, allowing for a formal description of technologies. The TCM is then automatically derived. An ontology based on the Basic Formal Ontology is developed to describe systems and technologies, and provides axioms to derive statements about these descriptions. The method is demonstrated with four inference examples, showing how the inferences are made. An industry case study demonstrates the method's ability to mimic human expert reasoning. Although the approach is labour-intensive during setup, it enables knowledge capturing, automated reasoning and can be extended to provide quantitative analysis, to save time and effort.