The study of categories that abstract the structural properties of relations has been extensively developed over the years, resulting in a rich and diverse body of work. This paper strives to provide a modern presentation of these ``categories for relations'', including their enriched version, further showing how they arise as Kleisli categories of symmetric monoidal monads. The resulting taxonomy aims at bringing clarity and organisation to the many related concepts and frameworks occurring in the literature.

Many well-known logical identities are naturally written as equivalences between contextual formulas. A simple example is the Boole-Shannon expansion $c[p] \equiv (p \wedge c[\mathrm{true}] ) \vee (\neg\, p \wedge c[\mathrm{false}] )$, where $c$ denotes an arbitrary formula with possibly multiple occurrences of a "hole", called a context, and $c[\varphi]$ denotes the result of "filling" all holes of $c$ with the formula $\varphi$. Another example is the unfolding rule $\mu X. c[X] \equiv c[\mu X. c[X]]$ of the modal $\mu$-calculus. We consider the modal $\mu$-calculus as overarching temporal logic and, as usual, reduce the problem whether $\varphi_1 \equiv \varphi_2$ holds for contextual formulas $\varphi_1, \varphi_2$ to the problem whether $\varphi_1 \leftrightarrow \varphi_2$ is valid . We show that the problem whether a contextual formula of the $\mu$-calculus is valid for all contexts can be reduced to validity of ordinary formulas. Our first result constructs a canonical context such that a formula is valid for all contexts if{}f it is valid for this particular one. However, the ordinary formula is exponential in the nesting-depth of the context variables. In a second result we solve this problem, thus proving that validity of contextual formulas is EXP-complete, as for ordinary equivalences. We also prove that both results hold for CTL and LTL as well. We conclude the paper with some experimental results. In particular, we use our implementation to automatically prove the correctness of a set of six contextual equivalences of LTL recently introduced by Esparza et al. for the normalization of LTL formulas. While Esparza et al. need several pages of manual proof, our tool only needs milliseconds to do the job and to compute counterexamples for incorrect variants of the equivalences.

Full formal descriptions of algorithms making use of quantum principles must take into account both quantum and classical computing components and assemble them so that they communicate and cooperate. Moreover, to model concurrent and distributed quantum computations, as well as quantum communication protocols, quantum to quantum communications which move qubits physically from one place to another must also be taken into account. Inspired by classical process algebras, which provide a framework for modeling cooperating computations, a process algebraic notation is defined, named QPAlg for Quantum Process Algebra, which provides a homogeneous style to formal descriptions of concurrent and distributed computations comprising both quantum and classical parts. On the quantum side, QPAlg provides quantum variables, operations on quantum variables (unitary operators and measurement observables), as well as new forms of communications involving the quantum world. The operational semantics makes sure that these quantum objects, operations and communications operate according to the postulates of quantum mechanics.

Past years have seen the development of a few proposals for quantum extensions of process calculi. The rationale is clear: with the development of quantum communication protocols, there is a need to abstract and focus on the basic features of quantum concurrent systems, like CCS and CSP have done for their classical counterparts. So far, though, no accepted standard has emerged, neither for the syntax nor for the behavioural semantics. Indeed, the various proposals do not agree on what should be the observational properties of quantum values, and as a matter of fact, the soundness of such properties has never been validated against the prescriptions of quantum theory. To this aim, we introduce a new calculus, Linear Quantum CCS (lqCCS), and investigate the features of behavioural equivalences based on barbs and contexts. Our calculus can be thought of as an asynchronous, linear version of qCCS, which is in turn based on value-passing CCS. The combination of linearity and asynchronous communication fits well with the properties of quantum systems (e.g. the no-cloning theorem), since it ensures that each qubit is sent exactly once, precisely specifying which qubits of a process interact with the context. We exploit contexts to examine how bisimilarities relate to quantum theory. We show that the observational power of general contexts is incompatible with quantum theory: roughly, they can perform non-deterministic moves depending on quantum values without measuring (hence perturbing) them. Therefore, we refine the operational semantics in order to prevent contexts from performing unfeasible non-deterministic choices. This induces a coarser bisimilarity that better fits the quantum setting: ( i ) it lifts the indistinguishability of quantum states to the distributions of processes and, despite the additional constraints, ( i i ) it preserves the expressiveness of non-deterministic choices based on classical information. To the best of our knowledge, our semantics is the first one that satisfies the two properties above.

Introduced in the 1990s in the context of the algebraic approach to graph rewriting, gs-monoidal categories are symmetric monoidal categories where each object is equipped with the structure of a commutative comonoid. They arise for example as Kleisli categories of commutative monads on cartesian categories, and as such they provide a general framework for effectful computation. Recently proposed in the context of categorical probability, Markov categories are gs-monoidal categories where the monoidal unit is also terminal, and they arise for example as Kleisli categories of commutative affine monads, where affine means that the monad preserves the monoidal unit. The aim of this paper is to study a new condition on the gs-monoidal structure, resulting in the concept of weakly Markov categories, which is intermediate between gs-monoidal categories and Markov ones. In a weakly Markov category, the morphisms to the monoidal unit are not necessarily unique, but form a group. As we show, these categories exhibit a rich theory of conditional independence for morphisms, generalising the known theory for Markov categories. We also introduce the corresponding notion for commutative monads, which we call weakly affine, and for which we give two equivalent characterisations. The paper argues that these monads are relevant to the study of categorical probability. A case at hand is the monad of finite non-zero measures, which is weakly affine but not affine. Such structures allow to investigate probability without normalisation within an elegant categorical framework.

Abstract Adhesive categoriesprovide an abstract framework for the algebraic approach to rewriting theory, where many general results can be recast and uniformly proved. However, checking that a model satisfies the adhesivity properties is sometimes far from immediate. In this paper we present a new criterion giving a sufficient condition for $$\mathcal {M},\mathcal {N}$$ M,N -adhesivity, a generalisation of the original notion of adhesivity. We apply it to several existing categories, and in particular tohierarchical graphs, a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting and for which various alternative definitions float around.

String diagrams are a powerful and intuitive graphical syntax, originating in theoretical physics and later formalised in the context of symmetric monoidal categories. In recent years, they have found application in the modelling of various computational structures, in fields as diverse as Computer Science, Physics, Control Theory, Linguistics, and Biology. In several of these proposals, transformations of systems are modelled as rewrite rules of diagrams. These developments require a mathematical foundation for string diagram rewriting: whereas rewrite theory for terms is well-understood, the two-dimensional nature of string diagrams poses quite a few additional challenges. This work systematises and expands a series of recent conference papers, laying down such a foundation. As a first step, we focus on the case of rewrite systems for string diagrammatic theories that feature a Frobenius algebra. This common structure provides a more permissive notion of composition than the usual one available in monoidal categories, and has found many applications in areas such as concurrency, quantum theory, and electrical circuits. Notably, this structure provides an exact correspondence between the syntactic notion of string diagrams modulo Frobenius structure and the combinatorial structure of hypergraphs. Our work introduces a combinatorial interpretation of string diagram rewriting modulo Frobenius structures in terms of double-pushout hypergraph rewriting. We prove this interpretation to be sound and complete and we also show that the approach can be generalised to rewriting modulo multiple Frobenius structures. As a proof of concept, we show how to derive from these results a termination strategy for Interacting Bialgebras, an important rewrite theory in the study of quantum circuits and signal flow graphs.

Abstract Symmetric monoidal theories (SMTs) generalise algebraic theories in a way that make them suitable to express resource-sensitive systems, in which variables cannot be copied or discarded at will. In SMTs, traditional tree-like terms are replaced by string diagrams, topological entities that can be intuitively thought of as diagrams of wires and boxes. Recently, string diagrams have become increasingly popular as a graphical syntax to reason about computational models across diverse fields, including programming language semantics, circuit theory, quantum mechanics, linguistics, and control theory. In applications, it is often convenient to implement the equations appearing in SMTs as rewriting rules. This poses the challenge of extending the traditional theory of term rewriting, which has been developed for algebraic theories, to string diagrams. In this paper, we develop a mathematical theory of string diagram rewriting for SMTs. Our approach exploits the correspondence between string diagram rewriting and double pushout (DPO) rewriting of certain graphs, introduced in the first paper of this series. Such a correspondence is only sound when the SMT includes a Frobenius algebra structure. In the present work, we show how an analogous correspondence may be established for arbitrary SMTs, once an appropriate notion of DPO rewriting (which we call convex) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras.

Abstract In this paper, we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorially as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For standard DPO rewriting without interfaces, confluence for terminating rewriting systems is, in general, undecidable. Nevertheless, we show here that confluence for DPOI, and hence string diagram rewriting, is decidable. We apply this result to give effective procedures for deciding local confluence of symmetric monoidal theories with and without Frobenius structure by critical pair analysis. For the latter, we introduce the new notion of path joinability for critical pairs, which enables finitely many joins of a critical pair to be lifted to an arbitrary context in spite of the strong non-local constraints placed on rewriting in a generic symmetric monoidal theory.

Replicated Data Types (RDTs) have been introduced as a suitable abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, RDTs are commonly specified in terms of two relations: visibility, which accounts for the different views that a store may have, and arbitration, which states the logical order imposed on the operations executed over the store. Different flavours, e.g., operational, axiomatic and functional, have recently been proposed for the specification of RDTs. In this work, we propose an algebraic characterisation of RDT specifications. We define categories of visibility relations and arbitrations, show the existence of relevant limits and colimits, and characterize RDT specifications as functors between such categories that preserve these additional structures.

Symmetric monoidal categories have become ubiquitous as a formal environment for the analysis of compound systems in a compositional, resource-sensitive manner using the graphical syntax of string diagrams. Recently, reasoning with string diagrams has been implemented concretely via double-pushout (DPO) hypergraph rewriting. The hypergraph representation has the twin advantages of being convenient for mechanisation and of completely absorbing the structural laws of symmetric monoidal categories, leaving just the domain-specific equations explicit in the rewriting system.

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.

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 frameworks. Stability however is restrictive for dealing with formalisms where a computational step can merge parts of the state, like 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). We characterise, as a natural generalisation of prime algebraic domains, a class of domains that is well-suited to model the semantics of formalisms with fusions. 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 nonlinear graph rewriting systems. Interestingly, the category of general unstable event structures coreflects into our category of domains, so that our result provides a characterisation of the partial orders of configurations of such event structures.

String diagrams are a powerful and intuitive graphical syntax for terms of symmetric monoidal categories (SMCs). They find many applications in computer science and are becoming increasingly relevant in other fields such as physics and control theory.

The paper is devoted to an analysis of the concurrent features of asynchronous systems. A preliminary step is represented by the introduction of a non-interleaving extension of barbed equivalence. This notion is then exploited in order to prove thatconcurrency cannot be observedthrough asynchronous interactions, i.e., that the interleaving and concurrent versions of a suitable asynchronous weak equivalence actually coincide. The theory is validated on some case studies, related to nominal calculi (π-calculus) and visual specification formalisms (Petri nets). Additionally, we prove that a class of systems which is deemed (output-buffered) asynchronous, according to a characterization that was previously proposed in the literature, falls into our theory.

In this paper we focus on the synthesis of labelled transition systems (LTSs) for process calculi using Mobile Ambients (MAs) as a testbed. Our proposal is based on a graphical encoding: a process is mapped into a graph equipped with interfaces such that the denotation is fully abstract with respect to the standard structural congruence. Graphs with interfaces are amenable to the synthesis mechanism based on borrowed contexts (BCs), which is an instance of relative pushouts (RPOs). The BC mechanism allows the effective construction of an LTS that has graphs with interfaces as states and labels, and such that the associated bisimilarity is a congruence. We focus here on the analysis of an LTS over processes as graphs with interfaces: we use the LTS on graphs to recover an LTS directly defined over the structure of MA processes and define a set of SOS inference rules capturing the same operational semantics.

Barbed bisimilarity is a widely used behavioral equivalence for interactive systems: given a set of predicates (denoted “barbs” and representing basic observations on states) and a set of contexts (representing the possible execution environments), two systems are deemed to be equivalent if they verify the same barbs whenever inserted inside any of the chosen contexts. Despite its flexibility and expressiveness, this definition of equivalence is unsatisfactory because often the quantification is over an infinite set of contexts, thus making barbed bisimilarity very hard to be verified. Should a labeled operational semantics be available, more efficient observational equivalences might be adopted. To this end, a series of techniques has been proposed to derive labeled transition systems (LTSs) from unlabeled ones, the main example being Leifer and Milner’s theory of reactive systems. The underlying intuition is that labels should be the “minimal” contexts that allow for a reduction step to be performed. However, minimality is difficult to asses, whereas the set of “intuitively” correct labels is often easily devised by the ingenuity of the researcher. This article introduces a framework that characterizes (weak) barbed bisimilarity via LTSs whose labels are (not necessarily minimal) contexts. Differently from previous proposals, our theory does not depend on the way the labeled transitions are built but instead relies on a simple set-theoretical presentation for identifying those properties such an LTS should verify to (1) capture the barbed bisimilarities of the underlying system and (2) ensure that such bisimilarities are congruences. Furthermore, we adopt suitable proof techniques to make feasible the verification of such properties. To provide a test-bed for our formalism, we instantiate it by addressing the semantics of the Mobile Ambients calculus, recasting its barbed bisimilarities via label-based behavioral equivalences.

Quantified μ-calculi combine the fix-point and modal operators of temporal logics with (existential and universal) quantifiers, and they allow for reasoning about the possible behaviour of individual components within a software system. In this paper

Web services represent a promising technology for the development of distributed heterogeneous software systems. In this setting, a major issue is to establish whether two services can be used interchangeably in any context. To this aim, our paper first briefly reviews the results contained in a recent article by the same authors, where a suitable notion of behavioural equivalence for Web services was introduced. Our work then extends those results, in order to account for ontologybased service specifications. Next, a concrete example scenario – a car rental system – is presented, and it is then used to illustrate how the equivalence between services can be fruitfully employed for correctly addressing two prominent, modularity-related problems: the publication of correct service specifications and the replaceability of (sub)services.

We propose a graphical implementation for (possibly recursive) processes of the π-calculus, encoding each process into a graph. Our implementation is sound and complete with respect to the structural congruence for the calculus: two processes are equivalent if and only if they are mapped into graphs with the same normal form. Most importantly, the encoding allows the use of standard graph rewriting mechanisms for modelling the reduction semantics of the calculus.

Introduces a new paradigm for concurrency, called behaviours-as-types. In this paradigm, types are used to convey information about the behaviour of processes: while terms correspond to processes, types correspond to behaviours. We apply this paradigm to Winskel's (1994) process algebra. Its types are similar to Kozen's (1983) modal /spl mu/-calculus; hence, they are called modal /spl mu/-types. We prove that two terms having the same type denote two processes which behave in the some way, that is, they are bisimilar. We give a sound and complete compositional typing system for this language. Such a system naturally also recovers the notion of bisimulation on open terms, allowing us to deal with processes with undefined parts in a compositional manner.