Search

Fo-bicategories are a categorification of Peirce's calculus of relations. Notably, their laws provide a proof system for first-order logic that is both purely equational and complete. This paper illustrates a correspondence between fo-bicategories and Lawvere's hyperdoctrines. To streamline our proof, we introduce peircean bicategories, which offer a more succinct characterization of fo-bicategories.

We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley's property directed reachability algorithm. For finding safe invariants or counterexamples, the first algorithm exploits over-approximations of both forward and backward transition relations, expressed abstractly by the notion of adjoints. In the absence of adjoints, one can use the second algorithm, which exploits lower sets and their principals. As a notable example of application, we consider quantitative reachability problems for Markov Decision Processes., Comment: 44 pages, 11 figures, the full version of the paper accepted by CAV 2023

Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this work we present tape diagrams, a sound and complete diagrammatic language for these categories, that can be intuitively thought as string diagrams of string diagrams. We test the effectiveness of our approach against the positive fragment of Tarski's calculus of relations.

In this paper we address the problem of proving confluence for string diagram rewriting, which was previously shown to be characterised combinatorically as double-pushout rewriting with interfaces (DPOI) on (labelled) hypergraphs. For standard DPO rewriting without interfaces, confluence for terminating rewrite 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.

We study the canonical weak distributive law $\delta$ of the powerset monad over the semimodule monad for a certain class of semirings containing, in particular, positive semifields. For this subclass we characterise $\delta$ as a convex closure in the free semimodule of a set. Using the abstract theory of weak distributive laws, we compose the powerset and the semimodule monads via $\delta$, obtaining the monad of convex subsets of the free semimodule., Comment: arXiv admin note: substantial text overlap with arXiv:2012.14778

We study the relationship between cartesian bicategories and a specialisation of Lawvere's hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines.

We extend the theory of Interacting Hopf algebras with an order primitive, and give a sound and complete axiomatisation of the prop of polyhedral cones. Next, we axiomatise an affine extension and prove soundness and completeness for the prop of polyhedra.

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

We describe the canonical weak distributive law $\delta \colon \mathcal S \mathcal P \to \mathcal P \mathcal S$ of the powerset monad $\mathcal P$ over the $S$-left-semimodule monad $\mathcal S$, for a class of semirings $S$. We show that the composition of $\mathcal P$ with $\mathcal S$ by means of such $\delta$ yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs's monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of $\mathcal P$ to $\mathbb{EM}(\mathcal S)$ as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad $\mathcal P_f$.

String diagrams are a powerful and intuitive graphical syntax, originated in the study of symmetric monoidal categories. In the last few 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 many such proposals, the transformations of the described systems are modelled as rewrite rules of diagrams. These developments demand a mathematical foundation for string diagram rewriting: whereas rewrite theory for terms is well-understood, the two-dimensional nature of string diagrams poses additional challenges. This work systematises and expands a series of recent conference papers laying down such foundation. As first step, we focus on the case of rewrite systems for string diagrammatic theories which feature a Frobenius algebra. This situation ubiquitously appear in various approaches: for instance, in the algebraic semantics of linear dynamical systems, Frobenius structures model the wiring of circuits; in categorical quantum mechanics, they model interacting quantum observables. Our work introduces a combinatorial interpretation of string diagram rewriting modulo Frobenius structures, in terms of double-pushout hypergraph rewriting. Furthermore, we prove this interpretation to be sound and complete. In the last part, we also see that the approach can be generalised to model 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.

We prove that every finitely generated convex set of finitely supported probability distributions has a unique base, and use this result to show that the monad of convex sets of probability distributions is presented by the algebraic theory of convex semilattices.

Relational structures are emerging as ubiquitous mathematical machinery in the semantics of open systems of various kinds. Cartesian bicategories are a well-known categorical algebra of relations that has proved especially useful in recent applications. The passage between a category and its bicategory of relations is an important question that has been widely studied for decades. We study an alternative construction that yields a cartesian bicategory of relations. Its behaviour is closely related to the axiom of choice, which itself can be expressed in the language of cartesian bicategories.

We extend the signal flow calculus---a compositional account of the classical signal flow graph model of computation---to encompass affine behaviour, and furnish it with a novel operational semantics. The increased expressive power allows us to define a canonical notion of contextual equivalence, which we show to coincide with denotational equality. Finally, we characterise the realisable fragment of the calculus: those terms that express the computations of (affine) signal flow graphs., Comment: Accepted for publication in the proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020)

Turi and Plotkin's bialgebraic semantics is an abstract approach to specifying the operational semantics of a system, by means of a distributive law between its syntax (encoded as a monad) and its dynamics (an endofunctor). This setup is instrumental in showing that a semantic specification (a coalgebra) satisfies desirable properties: in particular, that it is compositional. In this work, we use the bialgebraic approach to derive well-behaved structural operational semantics of string diagrams, a graphical syntax that is increasingly used in the study of interacting systems across different disciplines. Our analysis relies on representing the two-dimensional operations underlying string diagrams in various categories as a monad, and their bialgebraic semantics in terms of a distributive law over that monad. As a proof of concept, we provide bialgebraic compositional semantics for a versatile string diagrammatic language which has been used to model both signal flow graphs (control theory) and Petri nets (concurrency theory). Moreover, our approach reveals a correspondence between two different interpretations of the Frobenius equations on string diagrams and two synchronisation mechanisms for processes, \`a la Hoare and \`a la Milner., Comment: Accepted for publications in the proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019)

Stream GSOS is a specification format for operations and calculi on infinite sequences. The notion of bisimilarity provides a canonical proof technique for equivalence of closed terms in such specifications. In this paper, we focus on open terms, which may contain variables, and which are equivalent whenever they denote the same stream for every possible instantiation of the variables. Our main contribution is to capture equivalence of open terms as bisimilarity on certain Mealy machines, providing a concrete proof technique. Moreover, we introduce an enhancement of this technique, called bisimulation up-to substitutions, and show how to combine it with other up-to techniques to obtain a powerful method for proving equivalence of open terms.

This paper studies trace-based equivalences for systems combining nondeterministic and probabilistic choices. We show how trace semantics for such processes can be recovered by instantiating a coalgebraic construction known as the generalised powerset construction. We characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their oundness in a compositional way. In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages., Comment: long version of our CONCUR 2018 paper

Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points. While abstract interpretation is always sound by definition, the soundness of up-to techniques needs some ingenuity to be proven. For completeness, the setting is switched: up-to techniques are always complete, while abstract domains are not. In this work we show that, under reasonable assumptions, there is an evident connection between sound up-to techniques and complete abstract domains., Comment: 12 pages, accepted to 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'18)

The Calculus of Conjunctive Queries (CCQ) has foundational status in database theory. A celebrated theorem of Chandra and Merlin states that CCQ query inclusion is decidable. Its proof transforms logical formulas to graphs: each query has a natural model - a kind of graph - and query inclusion reduces to the existence of a graph homomorphism between natural models. We introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as CCQ. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters' notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin's insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.

We study different behavioral metrics, such as those arising from both branching and linear-time semantics, in a coalgebraic setting. Given a coalgebra $\alpha\colon X \to HX$ for a functor $H \colon \mathrm{Set}\to \mathrm{Set}$, we define a framework for deriving pseudometrics on $X$ which measure the behavioral distance of states. A crucial step is the lifting of the functor $H$ on $\mathrm{Set}$ to a functor $\overline{H}$ on the category $\mathrm{PMet}$ of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. If $H$ has a final coalgebra, every lifting $\overline{H}$ yields in a canonical way a behavioral distance which is usually branching-time, i.e., it generalizes bisimilarity. In order to model linear-time metrics (generalizing trace equivalences), we show sufficient conditions for lifting distributive laws and monads. These results enable us to employ the generalized powerset construction.

We introduce the concept of Frobenius theory as a generalisation of Lawvere's functorial semantics approach to categorical universal algebra. Whereas the universe for models of Lawvere theories is the category of sets and functions, or more generally cartesian categories, Frobenius theories take their models in the category of sets and relations, or more generally in cartesian bicategories.

Probabilistic automata (PA), also known as probabilistic nondeterministic labelled transition systems, combine probability and nondeterminism. They can be given different semantics, like strong bisimilarity, convex bisimilarity, or (more recently) distribution bisimilarity. The latter is based on the view of PA as transformers of probability distributions, also called belief states, and promotes distributions to first-class citizens. We give a coalgebraic account of distribution bisimilarity, and explain the genesis of the belief-state transformer from a PA. To do so, we make explicit the convex algebraic structure present in PA and identify belief-state transformers as transition systems with state space that carries a convex algebra. As a consequence of our abstract approach, we can give a sound proof technique which we call bisimulation up-to convex hull., Comment: Full (extended) version of a CONCUR 2017 paper, minor revision of the LMCS submission

We show how up-to techniques for (bi-)similarity can be used in the setting of weighted systems. The problems we consider are language equivalence, language inclusion and the threshold problem (also known as universality problem) for weighted automata. We build a bisimulation relation on the fly and work up-to congruence and up-to similarity. This requires to determine whether a pair of vectors (over a semiring) is in the congruence closure of a given relation of vectors. This problem is considered for rings and l-monoids, for the latter we provide a rewriting algorithm and show its confluence and termination. We then explain how to apply these up-to techniques to weighted automata and provide runtime results.

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. An important role in many such approaches is played by equational theories of diagrams, typically oriented and applied as rewrite rules. This paper lays a comprehensive foundation of this form of rewriting. We interpret diagrams combinatorially as typed hypergraphs and establish the precise correspondence between diagram rewriting modulo the laws of SMCs on the one hand and double pushout (DPO) rewriting of hypergraphs, subject to a soundness condition called convexity, on the other. This result rests on a more general characterisation theorem in which we show that typed hypergraph DPO rewriting amounts to diagram rewriting modulo the laws of SMCs with a chosen special Frobenius structure. We illustrate our approach with a proof of termination for the theory of non-commutative bimonoids., Comment: preprint. 32 pages

We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, showing under which conditions also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra on Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.

Bialgebrae provide an abstract framework encompassing the semantics of different kinds of computational models. In this paper we propose a bialgebraic approach to the semantics of logic programming. Our methodology is to study logic programs as reactive systems and exploit abstract techniques developed in that setting. First we use saturation to model the operational semantics of logic programs as coalgebrae on presheaves. Then, we make explicit the underlying algebraic structure by using bialgebrae on presheaves. The resulting semantics turns out to be compositional with respect to conjunction and term substitution. Also, it encodes a parallel model of computation, whose soundness is guaranteed by a built-in notion of synchronisation between different threads.

We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha: X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha: X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent., Comment: to be published in: Proceedings of FSTTCS 2014

We introduce the theory IH of interacting Hopf algebras, parametrised over a principal ideal domain R. The axioms of IH are derived using Lack's approach to composing PROPs: they feature two Hopf algebra and two Frobenius algebra structures on four different monoid-comonoid pairs. This construction is instrumental in showing that IH is isomorphic to the PROP of linear relations (i.e. subspaces) over the field of fractions of R.

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $\epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $\dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems.

Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.

The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence (~_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics., Comment: 23 pages

Concurrent constraint programming (ccp) is a well-established model for concurrency that singles out the fundamental aspects of asynchronous systems whose agents (or processes) evolve by posting and querying (partial) information in a global medium. Bisimilarity is a standard behavioural equivalence in concurrency theory. However, only recently a well-behaved notion of bisimilarity for ccp, and a ccp partition refinement algorithm for deciding the strong version of this equivalence have been proposed. Weak bisimiliarity is a central behavioural equivalence in process calculi and it is obtained from the strong case by taking into account only the actions that are observable in the system. Typically, the standard partition refinement can also be used for deciding weak bisimilarity simply by using Milner's reduction from weak to strong bisimilarity; a technique referred to as saturation. In this paper we demonstrate that, because of its involved labeled transitions, the above-mentioned saturation technique does not work for ccp. We give an alternative reduction from weak ccp bisimilarity to the strong one that allows us to use the ccp partition refinement algorithm for deciding this equivalence., Comment: In Proceedings ICE 2012, arXiv:1212.3458. arXiv admin note: text overlap with arXiv:1212.1548

Saraswat's concurrent constraint programming (ccp) is a mature formalism for modeling processes (or programs) that interact by telling and asking constraints in a global medium, called the store. Bisimilarity is a standard behavioural equivalence in concurrency theory, but a well-behaved notion of bisimilarity for ccp has been proposed only recently. When the state space of a system is finite, the ordinary notion of bisimilarity can be computed via the well-known partition refinement algorithm, but unfortunately, this algorithm does not work for ccp bisimilarity. In this paper, we propose a variation of the partition refinement algorithm for verifying ccp bisimilarity. To the best of our knowledge this is the first work providing for the automatic verification of program equivalence for ccp, Comment: 27th ACM Symposium On Applied Computing, Trento : Italy (2012)

The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics (that is defined in terms of bisimilarity) is characterized by the final morphism in some category of coalgebras. Since the behaviour of interactive systems is for many reasons infinite, symbolic semantics were introduced as a mean to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, symbolic bisimilarity has a different shape with respect to ordinary bisimilarity, and thus the standard coalgebraic characterization does not work. In this paper, we introduce its coalgebraic models. We will use as motivating examples two asynchronous formalisms: open Petri nets and asynchronous pi-calculus. Indeed, as we have shown in a previous paper, asynchronous bisimilarity can be seen as an instance of symbolic bisimilarity., Comment: 53 pages, 13 Figures, 2 Tables. Journal version of the work published in the proceedings of CALCO 2009

Reactive systems (RSs) represent a meta-framework aimed at deriving behavioral congruences for those computational formalisms whose operational semantics is provided by reduction rules. RSs proved a flexible specification device, yet so far most of the efforts dealing with their behavioural semantics focused on idem pushouts (IPOs) and saturated (also known as dynamic) bisimulations. In this paper we introduce a novel, intermediate behavioural equivalence: L-bisimilarity, which is able to recast both its IPO and saturated counterparts. The equivalence is parametric with respect to a set L of RSs labels, and it is shown that under mild conditions on L it is indeed a congruence. Furthermore, L-bisimilarity can also recast the notion of barbed semantics for RSs, proposed by the same authors in a previous paper. In order to provide a suitable test-bed, we instantiate our proposal by addressing the semantics of (asynchronous) CCS and of the calculus of mobile ambients.

This volume contains the proceedings of the 2nd Workshop on Interaction and Concurrency Experience (ICE'09). The workshop was held in Bologna, Italy on 31th of August 2009, as a satellite workshop of CONCUR'09. The previous edition of ICE has been organized in Reykjavik (2008). The ICE workshop is intended as a series of international scientific meetings oriented to researchers in various fields of theoretical computer science and, each year, the workshop focuses on a specific topic: ICE 2009 focused on structured interactions meant as the class of synchronisations that go beyond the "simple" point-to-point synchronisations (e.g., multicast or broadcast synchronisations, even-notification based interactions, time dependent interactions, distributed transactions,...).