arXiv subjects

Filippo Bonchi

Publications and source records attributed to Filippo Bonchi.

49 records · Page 3Linked to original sources

arXiv2016

Rewriting modulo symmetric monoidal structure

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.

math.CT↗

arXiv2015

Interacting Hopf Algebras

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.

cs.LO↗

arXiv2015

Towards Trace Metrics via Functor Lifting

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.

cs.LO↗

arXiv2015

Bialgebraic Semantics for Logic Programming

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.

cs.LO↗

arXiv2014

Behavioral Metrics via Functor Lifting

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.

cs.LO↗

arXiv2014

Coinduction up to in a fibrational setting

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.

cs.LO↗

arXiv2014

How to Kill Epsilons with a Dagger -- A Coalgebraic Take on Systems with Algebraic Label Structure

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $ε$-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.

cs.LO↗

arXiv2013

Generalizing determinization from automata to coalgebras

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.

cs.LO↗

arXiv2012

Reducing Weak to Strong Bisimilarity in CCP

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.

cs.PL↗

arXiv2012

Partition Refinement for Bisimilarity in CCP

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

cs.LO↗

arXiv2011

Symbolic and Asynchronous Semantics via Normalized Coalgebras

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.

cs.LO↗

arXiv2010

On Barbs and Labels in Reactive Systems

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.

cs.LO↗

arXiv2009

Proceedings 2nd Interaction and Concurrency Experience: Structured Interactions

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

cs.LO↗