arXiv subjects

Andrea Corradini

Publications and source records attributed to Andrea Corradini.

13 recordsLinked to original sources

arXiv2026

Structural Morphisms for Nested Conditions - Full Version

Nested conditions are used, among other things, as a graphical way to express first order formulas ruling the applicability of a graph transformation rule to a given match. In this paper, we first introduce several operators on conditions mimicking logical connectives. Next we propose an original notion of structural morphism among nested conditions, and we identify circumstances under which morphisms are consistent with the entailment of the corresponding conditions. Finally we frame the results in a categorical context, proving functoriality and universality properties of the various operations.

cs.LO↗

arXiv2024

On Categories of Nested Conditions

Nested conditions are used, among other things, as a graphical way to express first order formulas ruling the applicability of a graph transformation rule to a given match. In this paper, we propose (for the first time) a notion of structural morphism among nested conditions, consistent with the entailment of the corresponding formulas. This reveals a structural weakness of the existing definition of nested conditions, which we overcome by proposing a new notion of span-based nested conditions, embedding the original ones. We also introduce morphisms for the latter, showing that those form a richer structure by organising the various models in a number of categories suitably related by functors.

cs.LO↗

arXiv2024

Coinductive Techniques for Checking Satisfiability of Generalized Nested Conditions

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.

cs.LO↗

arXiv2024

Left-Linear Rewriting in Adhesive Categories

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

cs.LO↗

arXiv2023

From Gs-monoidal to Oplax Cartesian Categories: Constructions and Functorial Completeness

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}$.

cs.LO↗

arXiv2020

Encoding Incremental NACs in Safe Graph Grammars using Complementation

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.

cs.LO↗

arXiv2020

Domains and Event Structures for Fusions

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.

cs.LO↗

arXiv2019

Rewriting Abstract Structures: Materialization Explained Categorically

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.

cs.LO↗

arXiv2018

Event Structures for Petri nets with Persistence

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.

cs.LO↗

arXiv2017

Specifying Graph Languages with Type Graphs

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.

cs.FL↗

arXiv2016

Proceedings 9th International Workshop on Computing with Terms and Graphs

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).

cs.LO↗

arXiv2011

Term Graph Rewriting and Parallel Term Rewriting

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.

cs.LO↗

arXiv2008

Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets

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.

cs.LO↗