Graphs are widely used in various domains to model complex relationships, often requiring the specification and verification of their properties. These properties may involve complex conditions placing, e.g., structural requirements on subgraphs of unbounded size. In this paper, we propose graph formulas as a new formalism for specifying graph properties, providing a higher level of "graphical" abstraction compared to well-known approaches such as monadic second-order logic. We show how these graph formulas can be translated into alternating graph automata, allowing to check computationally difficult graph properties, such as the existence or non-existence of Hamiltonian paths.
Many well-established threat modeling approaches use graphs as underlying structures. However, the formalism of graph-transformation is not applied. In this paper, we propose a graph-transformational approach to threat modeling. We take a more detailed look at a transformation from attack-defense trees to stochastic games. This leads us to further research questions that we believe are suitable to be answered in the language of graph transformations.
Conflict and dependency analysis is an important static analysis tool for gaining an overview of potential interactions of graph transformation rules. The analysis is based on critical pairs, which represent conflicting transformations in a minimal context. For many applications, however, the computation of complete critical pairs is unnecessarily complex. Instead, the crucial information about a conflicting pair of transformations is already contained in much smaller structures, called conflict reasons or disabling essences in existing research. So far, these structures have only been introduced for plain rules; in practical scenarios, however, transformation rules are regularly equipped with (application) conditions. In this paper, we fill this gap by lifting the computation of disabling essences to rules with conditions. It turns out that the situation is much more complex than for plain rules, where a pair of transformations is in conflict if and only if a non-trivial disabling essence embeds into the pair. However, we can show that, for every conflicting pair of transformations via rules with conditions, there is a disabling essence that embeds into this pair. For the special case of negative application conditions we can even show that a disabling essence is embeddable if and only if the transformation pair is in conflict. We work within the general context of adhesive HLR categories, which include several types of graph-like structures.
Traced monoidal closed categories are a model for higher-order functional computation. We develop a formal language of string diagrams for these categories, and a faithful interpretation in terms of certain hypergraphs. We then use the interpretation to show that string diagram rewriting can be implemented as double-pushout rewriting in a sound and complete way. Finally, we showcase our approach on the λ -calculus with explicit recursion.
Personalized learning is most effective as individuals have different learning styles and support needs. Many e-learning systems rely on static dialogue management, which offer limited flexibility to adapt to user behaviors and open discourse. This paper proposes a graph rewriting framework to adapt dialogue flow to user states in real-time. We propose its application in virtual job interviews-a key step toward employment-where personalized simulation training can be particularly valuable for individuals with diverse needs, including autistic users who may face challenges in social communication. Our framework leverages real-time multimodal data-speech, eye gaze, and physiology (e.g., heart rate)-to infer user states. We identified three key states in interviews: engagement, stress, and stuckness. Dialogue scripts are modeled as attributed, directed graphs, incorporating constraints to ensure consistency. Each interview question is represented as a node, with edges reflecting the flow of dialogue. The interview structure (host graph) was designed in collaboration with domain experts. Using graph rewriting, the framework dynamically modifies dialogue flows to enable contextually appropriate adaptations such as redirecting focus when the user goes off-topic, providing hints when stuck, or rephrasing questions for clarity-actions typically performed by coaches during mock interviews. Functionality of the grammar is demonstrated using interview scripts developed with experts, showcasing feasibility for virtual job interviews with simulated user states. This approach offers a personalized simulation experience that enhances realism, supports learning, and promotes the need for inclusive interviews.
In this paper, the parallelization of parallel independent rule applications within the double-pushout approach over adhesive categories is generalized in such a way that doubling can be avoided. If two rule applications to the same object delete the same part of the commonly accessed part, then independence is restored by removing the deletion part of one of the rule applications. Similarly, one can avoid that certain insertions are doubled. It turns out that parallelization with doubling avoidance is closely related to synchronization by means of amalgamated rules.
Graph databases have surged in popularity, and applications increasingly employ them to store and retrieve interconnected data. However, testing graph database-backed applications has distinctive challenges. Due to the sheer dimension of the graph schema state space, testing applications using naive random graph instances is unlikely to cover a large portion of an application program. We present PGFuzz, a graph transformation-based greybox fuzzer for testing graph database-backed applications, that is, to the best of our knowledge, the first fuzzer to specifically target graph database applications. PGFuzz builds on top of state-of-the-art graph generators and utilizes graph transformations guided by code coverage to produce application test inputs. PGFuzz's graph transformations are schema-aware and support recently introduced graph schema, key, and cardinality constraints. We evaluate PGFuzz on graph database applications that we curate from open-source repositories and show that PGFuzz substantially improves the test coverage of graph database-backed applications compared to the state-of-the-art.
We present a machine-checkable sufficient condition for relative termination of double-pushout graph rewriting systems with injective rules on edge-labeled multigraphs. Our method defines a graph's weight as the sum of weights of occurrences of a set of graphs within it. By ensuring (1) every rewriting step using rules in a set A strictly decreases the host graph's weight, and (2) every rewriting step using rules in a set B never increases it, we guarantee that rules in the set A can be applied only finitely many times in any rewriting sequence with rules in the union of A and B. Our method resolves termination cases that prior interpretation-based methods cannot. We also propose an implementation of our technique.
In many application areas, it is necessary to specify and check properties of graphs. Such properties may be complex, placing structural requirements on graph regions of unbounded size. In this paper, we show that alternating graph automata can check such graph properties, e.g., whether a given input graph is a tree, or whether it contains a Hamiltonian cycle or not. In fact, we show that these automata can accept PSPACE-complete graph languages, and that their uniform membership problem is contained in PSPACE when only automata without permutation cycles are considered.
Graph transformations can be used to specify and analyse software systems by modelling operations as rules and generating the labelled transition system (LTS) as a representation of system behaviour. Model-based testing (MBT) often uses model checking over LTS to discover paths that satisfy certain test requirements. Significant challenges include the size of the state space and the complexity of model checking. Meta-heuristic search-based approaches try to cope with this problem by exploring only a small portion of the LTS to produce paths that cover maximal test objectives. Despite acceptable results in small case studies, these approaches also do not scale well. MBT approaches using graph transformation face the same limitations as LTS-based MBT in general, exacerbated by the more complex nature of graph-based LTS. However, apart from the behavioural information of the LTS, here we are able to use the graph structure of states and rules to define and evaluate test objectives. This enables a new method based on deep reinforcement learning to generate test suites for systems specified through graph transformations. We use the reward/penalty mechanism of reinforcement learning to optimise the selection of moves within the state space, enabling the generation of test cases based on prior decisions. Our goal is to achieve greater coverage of test objectives while minimising the size of the test cases. The method has been implemented in GROOVE, an open-source toolset for designing and model checking graph transformation systems. Experimental results in well-known case studies demonstrate that our approach generates test cases with improved coverage scores while reducing the cost of testing compared to existing works.
This paper addresses the following verification task: Given a graph transformation system and a class of initial graphs, can we guarantee (non-)reachability of a given other class of graphs that characterizes bad or erroneous states? Both initial and bad states are characterized by nested conditions (having first-order expressive power). Such systems typically have an infinite state space, causing the problem to be undecidable. We use abstract interpretation to obtain a finite approximation of that state space, and employ counter-example guided abstraction refinement to iteratively obtain suitable predicates for automated verification. Although our primary application is the analysis of graph transformation systems, we state our result in the general setting of reactive systems.
Distributed Cyber-Physical Systems (DCPSs) are omnipresent and their analysis against provided specifications is a central challenge. Hereby, distribution results in communication delays among agents that have to be adequately taken into account by software models to avoid race conditions. However, engineering DCPSs at a higher level of detail by incorporating communication delays explicitly inflates model size and impedes analysis. In this paper, we employ Timed Graph Transformation Systems (TGTSs) to model DCPSs and distinguish between local immediate and remote δ -delayed observations, requiring up to δ time units. We then (a) demonstrate potential absence of δ -delay robustness for TGTS models, (b) provide a procedure widening safe behavioral options of a verified 0-delay system model to derive a δ -delay robust TGTS model, and (c) analyze the restrictiveness of the widening and the resulting TGTS model for new unsafe behavior. As a running example, we consider a DCPS in which multiple distributed autonomous shuttles locally coordinate their movement on a track topology to avoid collisions.
Bigraphs are an expressive graphical modelling formalism to represent systems with a mix of both spatial and non-local connectivity. Currently it is possible to write nonsensical models, e.g. with a Room nested inside a Person rather than Person nested inside a Room, or to create a hyperedge from what should be a binary link. A sorting scheme can be used to filter badly-formed bigraphs from those that are well formed. While the theory of bigraph sorts is well developed, none of the existing methods leads to a practical implementation. Instead they are based on tables of descriptions or semi-mathematical notations. We look at sorting bigraphs through a practical lens: developing a new sorting language, and show how an extension to the existing theory of bigraphs, in the form of well-sorted interfaces, paves the way for an implementation of well-sorted bigraphs. We discuss the trade-offs of this approach, and show how it allows sorts to be specified for existing bigraph models found in the literature.
Graph APIs are capable of flexibly retrieving or manipulating graph-structured data over the web. This rather novel type of APIs presents new challenges when it comes to properly securing the APIs against the usual web application security risks, e.g., broken access control. A prominent security testing approach is taint analysis, which traces tainted, i.e., security-relevant, data from sources (where tainted data is inserted) to sinks (where the use of tainted data may lead to a security risk), over the information flow in an application. We present a first systematic approach to static and dynamic taint analysis for Graph APIs focusing on broken access control. The approach comprises the following. We taint nodes in the Graph API if they represent data requiring specific privileges in order to be retrieved or manipulated, and identify API calls which are related to sources and sinks. Then, we statically analyze whether tainted information flow between API source and sink calls occurs. To this end, we model the API calls using graph transformation rules. We subsequently use critical pair analysis to automatically analyze potential dependencies between rules representing source calls and rules representing sink calls. We distinguish direct from indirect tainted information flow and argue under which conditions the CPA is able to detect not only direct, but also indirect tainted flow. The static taint analysis (i) identifies flows that need to be further reviewed, since tainted nodes may be created by an API call and used or manipulated by another API call later without having the necessary privileges, and (ii) can be used to systematically design dynamic security tests for broken access control. The dynamic taint analysis checks if potential broken access control risks detected during the static taint analysis really occur. We apply the approach to a part of the GitHub GraphQL API.
Achieving the complexity of graph algorithms in conventional languages with programs based on graph transformation rules is challenging because of the cost of graph matching. Previous work demonstrated that with so-called rooted rules, certain algorithms can be executed in linear time using the graph programming language GP 2. However, for non-destructive algorithms which retain the structure of input graphs, achieving a linear runtime required that input graphs have a bounded node degree. In this paper, we show how to overcome this restriction by enhancing the graph data structure generated by the GP 2 compiler and exploiting the new structure in programs. As a case study, we present a 2-colouring program that runs in linear time on connected input graphs with arbitrary node degrees. We prove the linear time complexity and also provide empirical evidence in the form of timings for various classes of input graphs.
Bond graphs represent the structure and functionality of mechatronic systems from a power flow perspective. Unfortunately, presentations of bond graphs are replete with ambiguity, significantly impeding understanding. We extend the formalisation in preceding work to address the phenomenon of ‘causality’, intended to help formulate solution strategies for bond graphs, but usually presented in such vague terms that the claims made are easily shown to be false. We show that ‘causality’ only works as advertised in the simplest cases, where it mimics the mathematical definition of bond graph semantics. Counterexamples severely limit the applicability of the notion.
We refine the weighted type graph technique for proving termination of double pushout (DPO) graph transformation systems. We increase the power of the approach for graphs, we generalize the technique to other categories, and we allow for variations of DPO that occur in the literature.
On the one side, the formalism of Global Transformations comes with the claim of capturing any transformation of space that is local, synchronous and deterministic. The claim has been proven for different classes of models such as mesh refinements from computer graphics, Lindenmayer systems from morphogenesis modeling and cellular automata from biological, physical and parallel computation modeling. The Global Transformation formalism achieves this by using category theory for its genericity, and more precisely the notion of Kan extension to determine the global behaviors based on the local ones. On the other side, Causal Graph Dynamics describe the transformation of port graphs in a synchronous and deterministic way and has not yet being tackled. In this paper, we show the precise sense in which the claim of Global Transformations holds for them as well. This is done by showing different ways in which they can be expressed as Kan extensions, each of them highlighting different features of Causal Graph Dynamics. Along the way, this work uncovers the interesting class of Monotonic Causal Graph Dynamics and their universality among General Causal Graph Dynamics.
In this demonstration, we present an engine leveraging graph transformations for the automated reformulation of constraint specifications of combinatorial search problems. These arise in many settings, such as planning, scheduling, routing and design. The engine is situated in the Constraint Modelling Pipeline that, starting from an initial high-level specification, can apply type-specific refinements while targeting solvers from multiple paradigms: SAT, SMT, Mixed Integer Programming, and Constraint Programming. The problem specification is crucial in producing an effective input for the target solver, motivating our work to explore the space of reformulations of an initial specification. Our system transforms a constraint specification in the Essence language into an Abstract Syntax Tree (AST). These ASTs, considered as directed labelled graphs, serve as inputs to the graph transformation language GP2 (Graph Programs 2) for subsequent reformulation. Our engine currently employs a curated set of handcrafted rewrite rules applied sequentially to the ASTs by the GP2 framework. It is designed to learn the efficacy of various rewrites, prioritising those that yield superior performance outcomes. At this stage, our primary emphasis is ensuring the rewritten specifications’ soundness and semantic invariance. Central to our methodology is constructing a search graph, where nodes represent model specifications and solutions, while edges represent graph transformations and solver performance. Through this search graph our system enables the exploration of constraint specification variants and the evaluation of their effects on lower-level refinement strategies and solvers. Finally, we present a visualisation tool that allows the interactive inspection of the search graph and its content.
Context: The growing size of graph-based modeling artifacts in model-driven engineering calls for techniques that enable efficient execution of graph queries. Incremental approaches based on the RETE algorithm provide an adequate solution in many scenarios, but are generally designed to search for query results over the entire graph. However, in certain situations, a user may only be interested in query results for a subgraph, for instance when a developer is working on a large model of which only a part is loaded into their workspace. In this case, the global execution semantics can result in significant computational overhead. Contribution: To mitigate the outlined shortcoming, in this paper we propose an extension of the RETE approach that enables local, yet fully incremental execution of graph queries, while still guaranteeing completeness of results with respect to the relevant subgraph. Results: We empirically evaluate the presented approach via experiments inspired by a scenario from software development and an independent social network benchmark. The experimental results indicate that the proposed technique can significantly improve performance regarding memory consumption and execution time in favorable cases, but may incur a noticeable linear overhead in unfavorable cases.
