-
Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions
Authors:
Lara Stoltenow,
Barbara König,
Sven Schneider,
Andrea Corradini,
Leen Lambers,
Fernando Orejas
Abstract:
We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a…
▽ More
We study nested conditions, a generalization of first-order logic to a categorical setting, and provide a tableau-based (semi-decision) procedure for checking (un)satisfiability and finite model generation. This generalizes earlier results on graph conditions. Furthermore we introduce a notion of witnesses, allowing the detection of infinite models in some cases. To ensure completeness, paths in a tableau must be fair, where fairness requires that all parts of a condition are processed eventually. Since the correctness arguments are non-trivial, we rely on coinductive proof methods and up-to techniques that structure the arguments. We distinguish between two types of categories: categories where all sections are isomorphisms, allowing for a simpler tableau calculus that includes finite model generation; in categories where this requirement does not hold, model generation does not work, but we still obtain a sound and complete calculus.
△ Less
Submitted 9 July, 2024;
originally announced July 2024.
-
Left-Linear Rewriting in Adhesive Categories
Authors:
Paolo Baldan,
Davide Castelnovo,
Andrea Corradini,
Fabio Gadducci
Abstract:
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of man…
▽ More
When can two sequential steps performed by a computing device be considered (causally) independent? This is a relevant question for concurrent and distributed systems, since independence means that they could be executed in any order, and potentially in parallel. Equivalences identifying rewriting sequences which differ only for independent steps are at the core of the theory of concurrency of many formalisms. We investigate the issue in the context of the double pushout approach to rewriting in the general setting of adhesive categories. While a consolidated theory exists for linear rules,which can consume, preserve and generate entities, this paper focuses on left-linear rules which may also "merge" parts of the state. This is an apparently minimal, yet technically hard enhancement,since a standard characterisation of independence that - in the linear case - allows one to derive a number of properties, essential in the development of a theory of concurrency, no longer holds. The paper performs an in-depth study of the notion of independence for left-linear rules: it introduces a novel characterisation of independence, identifies well-behaved classes of left-linear rewriting systems,and provides some fundamental results including a Church-Rosser property and the existence of canonical equivalence proofs for concurrent computations. These results properly extends the class of formalisms that can be modelled in the adhesive framework
△ Less
Submitted 8 July, 2024;
originally announced July 2024.
-
Equivariant localisation in the theory of $Z$-stability for Kähler manifolds
Authors:
Alexia Corradini
Abstract:
We apply equivariant localisation to the theory of $Z$-stability and $Z$-critical metrics on a Kähler manifold $(X,α)$, where $α$ is a Kähler class. We show that the invariants used to determine $Z$-stability of the manifold, which are integrals over test configurations, can be written as a product of equivariant classes, hence equivariant localisation can be applied. We also study the existence o…
▽ More
We apply equivariant localisation to the theory of $Z$-stability and $Z$-critical metrics on a Kähler manifold $(X,α)$, where $α$ is a Kähler class. We show that the invariants used to determine $Z$-stability of the manifold, which are integrals over test configurations, can be written as a product of equivariant classes, hence equivariant localisation can be applied. We also study the existence of $Z$-critical Kähler metrics in $α$, whose existence is conjectured to be equivalent to $Z$-stability of $(X,α)$. In particular, we study a class of invariants that give an obstruction to the existence of such metrics. Then we show that these invariants can also be written as a product of equivariant classes. From this we give a new, more direct proof of an existing result: the former invariants determining $Z$-stability on a test configuration are equal to the latter invariants related to the existence of $Z$-critical metrics on the central fibre of the test configuration. This provides a new approach from which to derive the $Z$-critical equation.
△ Less
Submitted 13 September, 2022;
originally announced September 2022.
-
From Gs-monoidal to Oplax Cartesian Categories: Constructions and Functorial Completeness
Authors:
Tobias Fritz,
Fabio Gadducci,
Davide Trotta,
Andrea Corradini
Abstract:
Originally introduced in the context of the algebraic approach to term graph rewriting, the notion of gs-monoidal category has surfaced a few times under different monikers in the last decades. They can be thought of as symmetric monoidal categories whose arrows are generalised relations, with enough structure to talk about domains and partial functions, but less structure than cartesian bicategor…
▽ More
Originally introduced in the context of the algebraic approach to term graph rewriting, the notion of gs-monoidal category has surfaced a few times under different monikers in the last decades. They can be thought of as symmetric monoidal categories whose arrows are generalised relations, with enough structure to talk about domains and partial functions, but less structure than cartesian bicategories. The aim of this paper is threefold. The first goal is to extend the original definition of gs-monoidality by enriching it with a preorder on arrows, giving rise to what we call oplax cartesian categories. Second, we show that (preorder-enriched) gs-monoidal categories naturally arise both as Kleisli categories and as span categories, and the relation between the resulting formalisms is explored. Finally, we present two theorems concerning Yoneda embeddings on the one hand and functorial completeness on the other, the latter inducing a completeness result also for lax functors from oplax cartesian categories to $\mathbf{Rel}$.
△ Less
Submitted 29 September, 2023; v1 submitted 13 May, 2022;
originally announced May 2022.
-
Encoding Incremental NACs in Safe Graph Grammars using Complementation
Authors:
Andrea Corradini,
Maryam Ghaffari Saadat,
Reiko Heckel
Abstract:
In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique.…
▽ More
In modelling complex systems with graph grammars (GGs), it is convenient to restrict the application of rules using attribute constraints and negative application conditions (NACs). However, having both attributes and NACs in GGs renders the behavioural analysis (e.g. unfolding) of such systems more complicated. We address this issue by an approach to encode NACs using a complementation technique. We consider the correctness of our encoding under the assumption that the grammar is safe and NACs are incremental, and outline how this result can be extended to unsafe, attributed grammars.
△ Less
Submitted 2 December, 2020;
originally announced December 2020.
-
Rewriting Abstract Structures: Materialization Explained Categorically
Authors:
Andrea Corradini,
Tobias Heindel,
Barbara König,
Dennis Nolte,
Arend Rensink
Abstract:
The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in p…
▽ More
The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effectively computable under certain assumptions.
△ Less
Submitted 13 February, 2019;
originally announced February 2019.
-
Event Structures for Petri nets with Persistence
Authors:
Paolo Baldan,
Roberto Bruni,
Andrea Corradini,
Fabio Gadducci,
Hernan Melgratti,
Ugo Montanari
Abstract:
Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a u…
▽ More
Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a uniquely determined set of causes. Prime event structures, in turn, can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections.
Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new subclass of general event structures, called locally connected, by means of a chain of coreflections relying on an unfolding construction.
△ Less
Submitted 27 September, 2018; v1 submitted 11 February, 2018;
originally announced February 2018.
-
Specifying Graph Languages with Type Graphs
Authors:
Andrea Corradini,
Barbara König,
Dennis Nolte
Abstract:
We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basi…
▽ More
We investigate three formalisms to specify graph languages, i.e. sets of graphs, based on type graphs. First, we are interested in (pure) type graphs, where the corresponding language consists of all graphs that can be mapped homomorphically to a given type graph. In this context, we also study languages specified by restriction graphs and their relation to type graphs. Second, we extend this basic approach to a type graph logic and, third, to type graphs with annotations. We present decidability results and closure properties for each of the formalisms.
△ Less
Submitted 21 April, 2017; v1 submitted 18 April, 2017;
originally announced April 2017.
-
Domains and Event Structures for Fusions
Authors:
Paolo Baldan,
Andrea Corradini,
Fabio Gadducci
Abstract:
Stable event structures, and their duality with prime algebraic domains arising as partial orders of configurations, are a landmark of concurrency theory, providing a clear characterisation of causality in computations. They have been used for defining a concurrent semantics of several formalisms, from Petri nets to (linear) graph rewriting systems, which in turn lay at the basis of many visual mo…
▽ More
Stable event structures, and their duality with prime algebraic domains arising as partial orders of configurations, are a landmark of concurrency theory, providing a clear characterisation of causality in computations. They have been used for defining a concurrent semantics of several formalisms, from Petri nets to (linear) graph rewriting systems, which in turn lay at the basis of many visual modelling frameworks. Stability however is restrictive when dealing with formalisms with "fusion", i.e., where a computational step can not only consume and produce but also merge parts of the state. This happens, e.g., for graph rewriting systems with non-linear rules, which are needed to cover some relevant applications (such as the graphical encoding of calculi with name passing). Guided by the need of capturing the semantics of formalisms with fusion we leave aside stability and we characterise, as a natural generalisation of prime algebraic domains, a class of domains, referred to as weak prime domains. We then identify a corresponding class of event structures, that we call connected event structures, via a duality result formalised as an equivalence of categories. We show that connected event structures are exactly the class of event structures that arise as the semantics of non-linear graph rewriting systems. Interestingly, the category of general unstable event structures coreflects into our category of weak prime domains, so that our result provides a characterisation of the partial orders of configurations of such event structures.
△ Less
Submitted 18 November, 2020; v1 submitted 9 January, 2017;
originally announced January 2017.
-
Proceedings 9th International Workshop on Computing with Terms and Graphs
Authors:
Andrea Corradini,
Hans Zantema
Abstract:
This volume contains the proceedings of TERMGRAPH 2016, the Ninth International Workshop on Computing with Terms and Graphs which was held on April 8, 2016 in Eindhoven, The Netherlands, as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016).
This volume contains the proceedings of TERMGRAPH 2016, the Ninth International Workshop on Computing with Terms and Graphs which was held on April 8, 2016 in Eindhoven, The Netherlands, as a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016).
△ Less
Submitted 10 September, 2016;
originally announced September 2016.
-
AGREE -- Algebraic Graph Rewriting with Controlled Embedding (Long Version)
Authors:
Anadrea Corradini,
Dominique Duval,
Rachid Echahed,
Frédéric Prost,
Leila Ribeiro
Abstract:
The several algebraic approaches to graph transformation proposed in the literature all ensure that if an item is preserved by a rule, so are its connections with the context graph where it is embedded. But there are applications in which it is desirable, for example when cloning an item, to specify different embeddings for the original and for the copy. Therefore we propose a conservative extensi…
▽ More
The several algebraic approaches to graph transformation proposed in the literature all ensure that if an item is preserved by a rule, so are its connections with the context graph where it is embedded. But there are applications in which it is desirable, for example when cloning an item, to specify different embeddings for the original and for the copy. Therefore we propose a conservative extension of these approaches where a rule can specify how the embedding of a preserved item should be changed, typically by removing certain connections.
△ Less
Submitted 8 June, 2015; v1 submitted 14 November, 2014;
originally announced November 2014.
-
Term Graph Rewriting and Parallel Term Rewriting
Authors:
Andrea Corradini,
Frank Drewes
Abstract:
The relationship between Term Graph Rewriting and Term Rewriting is well understood: a single term graph reduction may correspond to several term reductions, due to sharing. It is also known that if term graphs are allowed to contain cycles, then one term graph reduction may correspond to infinitely many term reductions. We stress that this fact can be interpreted in two ways. According to the "s…
▽ More
The relationship between Term Graph Rewriting and Term Rewriting is well understood: a single term graph reduction may correspond to several term reductions, due to sharing. It is also known that if term graphs are allowed to contain cycles, then one term graph reduction may correspond to infinitely many term reductions. We stress that this fact can be interpreted in two ways. According to the "sequential interpretation", a term graph reduction corresponds to an infinite sequence of term reductions, as formalized by Kennaway et.al. using strongly converging derivations over the complete metric space of infinite terms. Instead according to the "parallel interpretation" a term graph reduction corresponds to the parallel reduction of an infinite set of redexes in a rational term. We formalize the latter notion by exploiting the complete partial order of infinite and possibly partial terms, and we stress that this interpretation allows to explain the result of reducing circular redexes in several approaches to term graph rewriting.
△ Less
Submitted 13 February, 2011;
originally announced February 2011.
-
Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
Authors:
Paolo Baldan,
Andrea Corradini,
Hartmut Ehrig,
Reiko Heckel,
Barbara König
Abstract:
We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary Place/Transition nets suited to model open systems which might interact with the surrounding environment and endowed with a colimit-based composition operation. We show that natural notions of bisimilarity…
▽ More
We propose a framework for the specification of behaviour-preserving reconfigurations of systems modelled as Petri nets. The framework is based on open nets, a mild generalisation of ordinary Place/Transition nets suited to model open systems which might interact with the surrounding environment and endowed with a colimit-based composition operation. We show that natural notions of bisimilarity over open nets are congruences with respect to the composition operation. The considered behavioural equivalences differ for the choice of the observations, which can be single firings or parallel steps. Additionally, we consider weak forms of such equivalences, arising in the presence of unobservable actions. We also provide an up-to technique for facilitating bisimilarity proofs. The theory is used to identify suitable classes of reconfiguration rules (in the double-pushout approach to rewriting) whose application preserves the observational semantics of the net.
△ Less
Submitted 21 October, 2008; v1 submitted 24 September, 2008;
originally announced September 2008.
