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.
