Document

**Published in:** LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)

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.

Filippo Bonchi, Alessandro Di Giorgio, and Davide Trotta. When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.MFCS.2024.30, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Trotta, Davide}, title = {{When Lawvere Meets Peirce: An Equational Presentation of Boolean Hyperdoctrines}}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, pages = {30:1--30:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-335-5}, ISSN = {1868-8969}, year = {2024}, volume = {306}, editor = {Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.30}, URN = {urn:nbn:de:0030-drops-205867}, doi = {10.4230/LIPIcs.MFCS.2024.30}, annote = {Keywords: relational algebra, hyperdoctrines, cartesian bicategories, string diagrams} }

Document

**Published in:** LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

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.

Filippo Bonchi, Alessandro Di Giorgio, and Paweł Sobociński. Diagrammatic Polyhedral Algebra. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.FSTTCS.2021.40, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Soboci\'{n}ski, Pawe{\l}}, title = {{Diagrammatic Polyhedral Algebra}}, booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)}, pages = {40:1--40:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-215-0}, ISSN = {1868-8969}, year = {2021}, volume = {213}, editor = {Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.40}, URN = {urn:nbn:de:0030-drops-155511}, doi = {10.4230/LIPIcs.FSTTCS.2021.40}, annote = {Keywords: String diagrams, Polyhedral cones, Polyhedra} }

Document

(Co)algebraic pearls

**Published in:** LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

Farkas' lemma is a celebrated result on the solutions of systems of linear inequalities, which finds application pervasively in mathematics and computer science. In this work we show how to formulate and prove Farkas' lemma in diagrammatic polyhedral algebra, a sound and complete graphical calculus for polyhedra. Furthermore, we show how linear programs can be modeled within the calculus and how some famous duality results can be proved.

Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi. From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.9, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Zanasi, Fabio}, title = {{From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9}, URN = {urn:nbn:de:0030-drops-153643}, doi = {10.4230/LIPIcs.CALCO.2021.9}, annote = {Keywords: String diagrams, Farkas Lemma, Duality, Linear Programming} }

Document

**Published in:** LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

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.

Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10, author = {Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}}, title = {{On Doctrines and Cartesian Bicategories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {10:1--10:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10}, URN = {urn:nbn:de:0030-drops-153656}, doi = {10.4230/LIPIcs.CALCO.2021.10}, annote = {Keywords: Cartesian bicategories, elementary existential doctrines, string diagram} }

Document

(Co)algebraic pearls

**Published in:** LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions.

Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11, author = {Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria}, title = {{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11}, URN = {urn:nbn:de:0030-drops-153666}, doi = {10.4230/LIPIcs.CALCO.2021.11}, annote = {Keywords: Convex sets of distributions monad, Convex semilattices, Unique base} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

LIPIcs, Volume 202, MFCS 2021, Complete Volume

46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 1-1560, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Proceedings{bonchi_et_al:LIPIcs.MFCS.2021, title = {{LIPIcs, Volume 202, MFCS 2021, Complete Volume}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {1--1560}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021}, URN = {urn:nbn:de:0030-drops-144396}, doi = {10.4230/LIPIcs.MFCS.2021}, annote = {Keywords: LIPIcs, Volume 202, MFCS 2021, Complete Volume} }

Document

Front Matter

**Published in:** LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Front Matter, Table of Contents, Preface, Conference Organization

46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.MFCS.2021.0, author = {Bonchi, Filippo and Puglisi, Simon J.}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)}, pages = {0:i--0:xvi}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-201-3}, ISSN = {1868-8969}, year = {2021}, volume = {202}, editor = {Bonchi, Filippo and Puglisi, Simon J.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.0}, URN = {urn:nbn:de:0030-drops-144409}, doi = {10.4230/LIPIcs.MFCS.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }

Document

**Published in:** LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

We argue that cartesian bicategories, often used as a general categorical algebra of relations, are also a natural setting for the study of the axiom of choice (AC). In this setting, AC manifests itself as an inequation asserting that every total relation contains a map. The generality of cartesian bicategories allows us to separate this formulation from other set-theoretically equivalent properties, for instance that epimorphisms split. Moreover, via a classification result, we show that cartesian bicategories satisfying choice tend to be those that arise from bicategories of spans.

Filippo Bonchi, Jens Seeber, and Paweł Sobociński. The Axiom of Choice in Cartesian Bicategories. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2019.15, author = {Bonchi, Filippo and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}}, title = {{The Axiom of Choice in Cartesian Bicategories}}, booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-120-7}, ISSN = {1868-8969}, year = {2019}, volume = {139}, editor = {Roggenbach, Markus and Sokolova, Ana}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.15}, URN = {urn:nbn:de:0030-drops-114439}, doi = {10.4230/LIPIcs.CALCO.2019.15}, annote = {Keywords: Cartesian bicategories, Axiom of choice, string diagrams} }

Document

**Published in:** LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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 for 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, à la Hoare and à la Milner.

Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Bialgebraic Semantics for String Diagrams. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2019.37, author = {Bonchi, Filippo and Piedeleu, Robin and Sobocinski, Pawel and Zanasi, Fabio}, title = {{Bialgebraic Semantics for String Diagrams}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {37:1--37:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.37}, URN = {urn:nbn:de:0030-drops-109398}, doi = {10.4230/LIPIcs.CONCUR.2019.37}, annote = {Keywords: String Diagram, Structural Operational Semantics, Bialgebraic semantics} }

Document

**Published in:** LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

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

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2018.17, author = {Bonchi, Filippo and K\"{o}nig, Barbara and Petrisan, Daniela}, title = {{Up-To Techniques for Behavioural Metrics via Fibrations}}, booktitle = {29th International Conference on Concurrency Theory (CONCUR 2018)}, pages = {17:1--17:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-087-3}, ISSN = {1868-8969}, year = {2018}, volume = {118}, editor = {Schewe, Sven and Zhang, Lijun}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.17}, URN = {urn:nbn:de:0030-drops-95552}, doi = {10.4230/LIPIcs.CONCUR.2018.17}, annote = {Keywords: behavioural metrics, bisimilarity, up-to techniques, coalgebras, fibrations} }

Document

**Published in:** LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

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.

Filippo Bonchi, Jens Seeber, and Pawel Sobocinski. Graphical Conjunctive Queries. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 13:1-13:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2018.13, author = {Bonchi, Filippo and Seeber, Jens and Sobocinski, Pawel}, title = {{Graphical Conjunctive Queries}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {13:1--13:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.13}, URN = {urn:nbn:de:0030-drops-96805}, doi = {10.4230/LIPIcs.CSL.2018.13}, annote = {Keywords: conjunctive query inclusion, string diagrams, cartesian bicategories} }

Document

Complete Volume

**Published in:** LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

LIPIcs, Volume 72, CALCO'17, Complete Volume

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Proceedings{bonchi_et_al:LIPIcs.CALCO.2017, title = {{LIPIcs, Volume 72, CALCO'17, Complete Volume}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017}, URN = {urn:nbn:de:0030-drops-82059}, doi = {10.4230/LIPIcs.CALCO.2017}, annote = {Keywords: Theory of Computation, Models of computation, Logics and Meanings of Programs, Semantics of Programming Languages – Algebraic Approach} }

Document

Front Matter

**Published in:** LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Front Matter, Table of Contents, Preface, List of Authors

7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CALCO.2017.0, author = {Bonchi, Filippo and K\"{o}nig, Barbara}, title = {{Front Matter, Table of Contents, Preface, List of Authors}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.0}, URN = {urn:nbn:de:0030-drops-80284}, doi = {10.4230/LIPIcs.CALCO.2017.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, List of Authors} }

Document

**Published in:** LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Probabilistic automata (PA) 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 the latter semantics, 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.

Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.23, author = {Bonchi, Filippo and Silva, Alexandra and Sokolova, Ana}, title = {{The Power of Convex Algebras}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {23:1--23:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.23}, URN = {urn:nbn:de:0030-drops-77966}, doi = {10.4230/LIPIcs.CONCUR.2017.23}, annote = {Keywords: belief-state transformers, bisimulation up-to, coalgebra, convex algebra, convex powerset monad, probabilistic automata} }

Document

**Published in:** LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

The symmetric monoidal theory of Interacting Hopf Algebras provides a sound and complete axiomatisation for linear relations over a given field. As is the case for ordinary relations, linear relations have a natural order that coincides with inclusion. In this paper, we give a presentation for this ordering by extending the theory of Interacting Hopf Algebras with a single additional inequation. We show that the extended theory gives rise to an abelian bicategory—a concept due to Carboni and Walters—and highlight similarities with the algebra of relations. Most importantly, the ordering leads to a well-behaved notion of refinement for signal flow graphs.

Filippo Bonchi, Joshua Holland, Dusko Pavlovic, and Pawel Sobocinski. Refinement for Signal Flow Graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2017.24, author = {Bonchi, Filippo and Holland, Joshua and Pavlovic, Dusko and Sobocinski, Pawel}, title = {{Refinement for Signal Flow Graphs}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {24:1--24:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.24}, URN = {urn:nbn:de:0030-drops-77758}, doi = {10.4230/LIPIcs.CONCUR.2017.24}, annote = {Keywords: Signal flow graphs, refinement, operational semantics, string diagrams, symmetric monoidal inequality theory} }

Document

**Published in:** LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

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, by identifying conditions under which 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 in 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.

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards Trace Metrics via Functor Lifting. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 35-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.CALCO.2015.35, author = {Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara}, title = {{Towards Trace Metrics via Functor Lifting}}, booktitle = {6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)}, pages = {35--49}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-84-2}, ISSN = {1868-8969}, year = {2015}, volume = {35}, editor = {Moss, Lawrence S. and Sobocinski, Pawel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.35}, URN = {urn:nbn:de:0030-drops-55254}, doi = {10.4230/LIPIcs.CALCO.2015.35}, annote = {Keywords: trace metric, monad lifting, pseudometric, coalgebra} }

Document

**Published in:** LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Up-to techniques are useful tools for optimising proofs of behavioural equivalence of processes. Bisimulations up-to context can be safely used in any language specified by GSOS rules. We showed this result in a previous paper by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras. In this paper, we prove the soundness of up-to contextual closure for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend our previously developed categorical framework to an ordered setting.

Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 240-253, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CONCUR.2015.240, author = {Bonchi, Filippo and Petrisan, Daniela and Pous, Damien and Rot, Jurriaan}, title = {{Lax Bialgebras and Up-To Techniques for Weak Bisimulations}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {240--253}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Aceto, Luca and de Frutos Escrig, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.240}, URN = {urn:nbn:de:0030-drops-53709}, doi = {10.4230/LIPIcs.CONCUR.2015.240}, annote = {Keywords: Up-to techniques, weak bisimulation, (lax) bialgebras} }

Document

**Published in:** LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

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 /F 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 /F-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.

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 403-415, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{baldan_et_al:LIPIcs.FSTTCS.2014.403, author = {Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K\"{o}nig, Barbara}, title = {{Behavioral Metrics via Functor Lifting}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {403--415}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-77-4}, ISSN = {1868-8969}, year = {2014}, volume = {29}, editor = {Raman, Venkatesh and Suresh, S. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.403}, URN = {urn:nbn:de:0030-drops-48599}, doi = {10.4230/LIPIcs.FSTTCS.2014.403}, annote = {Keywords: behavioral metric, functor lifting, pseudometric, coalgebra} }

Document

**Published in:** LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

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 behavioral
equivalence ($\sim_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. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.

Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing the powerset construction, coalgebraically. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 272-283, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.FSTTCS.2010.272, author = {Silva, Alexandra and Bonchi, Filippo and Bonsangue, Marcello M. and Rutten, Jan J. M. M.}, title = {{Generalizing the powerset construction, coalgebraically}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)}, pages = {272--283}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-23-1}, ISSN = {1868-8969}, year = {2010}, volume = {8}, editor = {Lodaya, Kamal and Mahajan, Meena}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.272}, URN = {urn:nbn:de:0030-drops-28706}, doi = {10.4230/LIPIcs.FSTTCS.2010.272}, annote = {Keywords: coalgebra, language equivalence, bisimilarity, powerset construction} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail