Volume
LIPIcs, Volume 72
7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO)
Event
CALCO 2017, June 12-16, 2017, Ljubljana, SloveniaEditors
Publication Details
- published at: 2017-11-17
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-033-0
- DBLP: db/conf/calco/calco2017
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 72, CALCO'17, Complete Volume
Abstract
LIPIcs, Volume 72, CALCO'17, Complete Volume
Cite as
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
Front Matter, Table of Contents, Preface, List of Authors
Abstract
Front Matter, Table of Contents, Preface, List of Authors
Cite as
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
Probability Sheaves and the Giry Monad
Abstract
I introduce the notion of probability sheaf, which is a mathematical structure capturing the relationship between probabilistic concepts (such as random variable) and sample spaces. Various probability-theoretic notions can be (re)formulated in terms of category-theoretic structure on the category of probability sheaves.
As a main example, I consider the Giry monad, which, in its original formulation, constructs spaces of probability measures. I show that the Giry monad generalises to the category of probability sheaves, where it turns out to have a simple, purely category-theoretic definition.
Cite as
Alex Simpson. Probability Sheaves and the Giry Monad. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 1:1-1:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{simpson:LIPIcs.CALCO.2017.1,
author = {Simpson, Alex},
title = {{Probability Sheaves and the Giry Monad}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {1:1--1:6},
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.1},
URN = {urn:nbn:de:0030-drops-80517},
doi = {10.4230/LIPIcs.CALCO.2017.1},
annote = {Keywords: Random variable, conditional independence, category theory, sheaves, Giry monad}
}
Document
Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks
Abstract
Span(Graph) was introduced by Katis, Sabadini and Walters as a categorical algebra of automata with interfaces, with main operation being communicating-parallel composition. Additional operations provide also a calculus of connectors or wires among components.
A system so described has two aspects: an informal network geometry arising from the algebraic expression, and a space of states and transition given by its evaluation in Span(Graph). So, Span(Graph) yields purely compositional, hierarchical descriptions of networks with a fixed topology .
The dual algebra Cospan(Graph) allows to describe also the sequential behaviour of systems. Both algebras, of spans and of cospans, are symmetrical monoidal categories with commutative separable algebra structures on the objects.
Hence, the combined algebra CospanSpan(Graph) can be interpreted as a general algebra for reconfigurable/hierarchical networks, generalizing the usual Kleene's algebra for classical automata. We present some examples of systems described in this setting.
Cite as
Alessandro Gianola, Stefano Kasangian, and Nicoletta Sabadini. Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gianola_et_al:LIPIcs.CALCO.2017.2,
author = {Gianola, Alessandro and Kasangian, Stefano and Sabadini, Nicoletta},
title = {{Cospan/Span(Graph): an Algebra for Open, Reconfigurable Automata Networks}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {2:1--2:17},
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.2},
URN = {urn:nbn:de:0030-drops-80535},
doi = {10.4230/LIPIcs.CALCO.2017.2},
annote = {Keywords: Categories, Automata, Composition, Networks}
}
Document
On Corecursive Algebras for Functors Preserving Coproducts
Abstract
For an endofunctor H on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on Y as the coproduct of the terminal coalgebra for H and the free H-algebra on Y. As a consequence, we derive that H is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors H(-) + Y are then cia functors. For finitary set functors we prove that, conversely, if H is a cia functor, then it has the form H = W \times (-) + Y for some sets W and Y.
Cite as
Jiri Adámek and Stefan Milius. On Corecursive Algebras for Functors Preserving Coproducts. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 3:1-3:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{adamek_et_al:LIPIcs.CALCO.2017.3,
author = {Ad\'{a}mek, Jiri and Milius, Stefan},
title = {{On Corecursive Algebras for Functors Preserving Coproducts}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {3:1--3:15},
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.3},
URN = {urn:nbn:de:0030-drops-80298},
doi = {10.4230/LIPIcs.CALCO.2017.3},
annote = {Keywords: terminal coalgebra, free algebra, corecursive algebra, hyper-extensive category}
}
Document
Bisimulation for Weakly Expressive Coalgebraic Modal Logics
Abstract
Research on the expressiveness of coalgebraic modal logics with respect to semantic equivalence notions has so far focused mainly on finding logics that are able to distinguish states that are not behaviourally equivalent (such logics are said to be expressive). In other words, the notion of behavioural equivalence is taken as the starting point, and the expressiveness of the logic is evaluated against it.
However, for some applications, modal logics that are not expressive are of independent interest. Such an example is given by contingency logic.
We can now turn the question of expressiveness around and ask, given a modal logic, what is a suitable notion of semantic equivalence? In this paper, we propose a notion of \Lambda-bisimulation which is parametric in a collection
\Lambda of predicate liftings. We study the basic properties of \Lambda-bisimilarity, and prove as our main result a Hennessy-Milner style theorem, which shows that (for finitary functors) \Lambda-bisimilarity exactly matches the expressiveness of the coalgebraic modal logic arising from \Lambda.
Cite as
Zeinab Bakhtiari and Helle Hvid Hansen. Bisimulation for Weakly Expressive Coalgebraic Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{bakhtiari_et_al:LIPIcs.CALCO.2017.4,
author = {Bakhtiari, Zeinab and Hvid Hansen, Helle},
title = {{Bisimulation for Weakly Expressive Coalgebraic Modal Logics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {4:1--4:16},
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.4},
URN = {urn:nbn:de:0030-drops-80500},
doi = {10.4230/LIPIcs.CALCO.2017.4},
annote = {Keywords: Coalgebraic modal logic, bisimulation, expressiveness, Hennessy-Milner theorem}
}
Document
Monoidal Company for Accessible Functors
Abstract
Distributive laws between functors are a fundamental tool in the theory of coalgebras. In the context of coinduction in complete lattices, they correspond to the so-called compatible functions, which enable enhancements of the coinductive proof technique. Amongst these, the greatest compatible function, called the companion, has recently been shown to satisfy many good properties.
Categorically, the companion of a functor corresponds to the final object in a category of distributive laws. We show that every accessible functor on a locally presentable category has a companion. Central to this and other constructions in the paper is the presentation of distributive laws as coalgebras for a certain functor. This functor itself has again, what we call, a second-order companion. We show how this companion interacts with the various monoidal structures on functor categories. In particular, both the first- and second-order companion give rise to monads. We use these results to obtain an abstract GSOS-like extension result for specifications involving the second-order companion.
Cite as
Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{basold_et_al:LIPIcs.CALCO.2017.5,
author = {Basold, Henning and Pous, Damien and Rot, Jurriaan},
title = {{Monoidal Company for Accessible Functors}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {5:1--5:16},
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.5},
URN = {urn:nbn:de:0030-drops-80379},
doi = {10.4230/LIPIcs.CALCO.2017.5},
annote = {Keywords: coalgebras, distributive laws, accessible functors, monoidal categories}
}
Document
On Path-Based Coalgebras and Weak Notions of Bisimulation
Abstract
It is well known that the theory of coalgebras provides an abstract definition of behavioural equivalence that coincides with strong bisimulation across a wide variety of state-based systems. Unfortunately, the theory in the presence of so-called silent actions is not yet fully developed. In this paper, we give a coalgebraic characterisation of branching (delay) bisimulation in the context of labelled transition systems (fully probabilistic systems). It is shown that recording executions (up to a notion of stuttering), rather than the set of successor states, from a state is sufficient to characterise the respected bisimulation relations in both cases.
Cite as
Harsh Beohar and Sebastian Küpper. On Path-Based Coalgebras and Weak Notions of Bisimulation. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{beohar_et_al:LIPIcs.CALCO.2017.6,
author = {Beohar, Harsh and K\"{u}pper, Sebastian},
title = {{On Path-Based Coalgebras and Weak Notions of Bisimulation}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {6:1--6:17},
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.6},
URN = {urn:nbn:de:0030-drops-80362},
doi = {10.4230/LIPIcs.CALCO.2017.6},
annote = {Keywords: Paths, Executions, Branching bisimulation, Coalgebras}
}
Document
Parity Automata for Quantitative Linear Time Logics
Abstract
We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.
Cite as
Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cirstea_et_al:LIPIcs.CALCO.2017.7,
author = {Cirstea, Corina and Shimizu, Shunsuke and Hasuo, Ichiro},
title = {{Parity Automata for Quantitative Linear Time Logics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {7:1--7:18},
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.7},
URN = {urn:nbn:de:0030-drops-80468},
doi = {10.4230/LIPIcs.CALCO.2017.7},
annote = {Keywords: coalgebra, quantitative logic, linear time logic, parity automaton}
}
Document
Automata Minimization: a Functorial Approach
Abstract
In this paper we regard languages and their acceptors - such as deterministic or weighted automata, transducers, or monoids - as
functors from input categories that specify the type of the
languages and of the machines to categories that specify the type of
outputs.
Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be applied to several phenomena in automata theory, starting with determinization and
minimization (previously studied from a coalgebraic and duality theoretic perspective). We apply in particular these techniques to
Choffrut's minimization algorithm for subsequential transducers and revisit Brzozowski's minimization algorithm.
Cite as
Thomas Colcombet and Daniela Petrisan. Automata Minimization: a Functorial Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.CALCO.2017.8,
author = {Colcombet, Thomas and Petrisan, Daniela},
title = {{Automata Minimization: a Functorial Approach}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {8:1--8:16},
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.8},
URN = {urn:nbn:de:0030-drops-80484},
doi = {10.4230/LIPIcs.CALCO.2017.8},
annote = {Keywords: functor automata, minimization, Choffrut's minimization algorithm, subsequential transducers, Brzozowski's minimization algorithm}
}
Document
The Positivication of Coalgebraic Logics
Abstract
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case of several modal logics. We show how the semantics of a boolean coalgebraic logic can be canonically lifted to define a semantics for its positive fragment, and that weak completeness transfers from the boolean case to the positive case.
Cite as
Fredrik Dahlqvist and Alexander Kurz. The Positivication of Coalgebraic Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2017.9,
author = {Dahlqvist, Fredrik and Kurz, Alexander},
title = {{The Positivication of Coalgebraic Logics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {9:1--9:15},
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.9},
URN = {urn:nbn:de:0030-drops-80425},
doi = {10.4230/LIPIcs.CALCO.2017.9},
annote = {Keywords: Coalgebraic logic, coalgebras, enriched category theory, boolean algebra, distributive lattice, positive modal logic, monotone modal logic}
}
Document
Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics
Abstract
Recent developments of game semantics have given rise to new models of concurrent languages. On the one hand, an approach based on string diagrams has given models of CCS and the pi-calculus, and on the other hand, Tsukada and Ong have designed a games model for a non-deterministic lambda-calculus. There is an obvious, shallow relationship between the two approaches, as they both define innocent strategies as sheaves for a Grothendieck topology embedding
"views" into "plays". However, the notions of views and plays differ greatly between the approaches: Tsukada and Ong use notions from standard game semantics, while the authors of this paper use string diagrams. We here aim to bridge this gap by showing that even though the notions of plays, views, and innocent strategies differ, it is mostly a matter of presentation.
Cite as
Clovis Eberhart and Tom Hirschowitz. Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{eberhart_et_al:LIPIcs.CALCO.2017.10,
author = {Eberhart, Clovis and Hirschowitz, Tom},
title = {{Justified Sequences in String Diagrams: a Comparison Between Two Approaches to Concurrent Game Semantics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {10:1--10:16},
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.10},
URN = {urn:nbn:de:0030-drops-80407},
doi = {10.4230/LIPIcs.CALCO.2017.10},
annote = {Keywords: Concurrency, Sheaves, Presheaf models, Game Semantics}
}
Document
Disjunctive Bases: Normal Forms for Modal Logics
Abstract
We present the concept of a disjunctive basis as a generic framework for normal forms in modal logic based on coalgebra. Disjunctive bases were defined in previous work on completeness for modal fixpoint logics, where they played a central role in the proof of a generic completeness theorem for coalgebraic mu-calculi. Believing the concept has a much wider significance, here
we investigate it more thoroughly in its own right. We show that the presence of a disjunctive basis at the "one-step" level entails a number of good properties for a coalgebraic mu-calculus, in particular, a simulation theorem showing that every alternating automaton can be transformed into an equivalent nondeterministic one. Based on this, we prove a Lyndon theorem for the full
fixpoint logic, its fixpoint-free fragment and its one-step fragment, and a Uniform Interpolation result, for both the full mu-calculus and its fixpoint-free fragment. We also raise the questions, when a disjunctive basis exists, and how disjunctive bases are related to Moss' coalgebraic "nabla" modalities. Nabla formulas provide disjunctive bases for many coalgebraic modal logics, but there are cases where disjunctive bases give useful normal forms even when nabla formulas fail to do so, our prime example being graded modal logic. Finally, we consider the problem of giving a category-theoretic formulation of disjunctive
bases, and provide a partial solution.
Cite as
Sebastian Enqvist and Yde Venema. Disjunctive Bases: Normal Forms for Modal Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{enqvist_et_al:LIPIcs.CALCO.2017.11,
author = {Enqvist, Sebastian and Venema, Yde},
title = {{Disjunctive Bases: Normal Forms for Modal Logics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {11:1--11:16},
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.11},
URN = {urn:nbn:de:0030-drops-80357},
doi = {10.4230/LIPIcs.CALCO.2017.11},
annote = {Keywords: Modal logic, fixpoint logic, automata, coalgebra, graded modal logic, Lyndon theorem, uniform interpolation}
}
Document
A Universal Construction for (Co)Relations
Abstract
Calculi of string diagrams are increasingly used to present the syntax and algebraic structure of various families of circuits, including signal flow graphs, electrical circuits and quantum processes. In many such approaches, the semantic interpretation for diagrams is given in terms of relations or corelations (generalised equivalence relations) of some kind. In this paper we show how semantic categories of both relations and corelations can be characterised as colimits of simpler categories. This modular perspective is important as it simplifies the task of giving a complete axiomatisation for semantic equivalence of string diagrams. Moreover, our general result unifies various theorems that are independently found in literature and are relevant for program semantics, quantum computation and control theory.
Cite as
Brendan Fong and Fabio Zanasi. A Universal Construction for (Co)Relations. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{fong_et_al:LIPIcs.CALCO.2017.12,
author = {Fong, Brendan and Zanasi, Fabio},
title = {{A Universal Construction for (Co)Relations}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {12:1--12:16},
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.12},
URN = {urn:nbn:de:0030-drops-80334},
doi = {10.4230/LIPIcs.CALCO.2017.12},
annote = {Keywords: corelation, prop, string diagram}
}
Document
Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics
Abstract
The non-commutative sequoid operator (/) on games was introduced to capture algebraically the presence of state in history-sensitive strategies in game semantics, by imposing a causality relation on the tensor product of games. Coalgebras for the functor A (/) _ - i.e., morphisms from S to A (/) S --- may be viewed as state transformers: if A (/) _ has a final coalgebra, !A, then the anamorphism of such a state transformer encapsulates its explicit state, so that it is shared only between successive invocations.
We study the conditions under which a final coalgebra !A for A (/) _ is the carrier of a cofree commutative comonoid on A. That is, it is a model of the exponential of linear logic in which we can construct imperative objects such as reference cells coalgebraically, in a game semantics setting. We show that if the tensor decomposes into the sequoid, the final coalgebra !A may be endowed with the structure of the cofree commutative comonoid if there is a natural isomorphism from !(A × B)to !A (x) !B. This condition is always satisfied if !A is the bifree algebra for A (/) _, but in general it is necessary to impose it, as we establish by giving an example of a sequoidally decomposable category of games in which plays will be allowed to have transfinite length. In this category, the final coalgebra for the functor A (/)_ is not the cofree commutative comonoid over A: we illustrate this by explicitly contrasting the final sequence for the functor A (/) _ with the chain of symmetric tensor powers used in the construction of the cofree commutative comonoid as a limit by Melliès, Tabareau and Tasson.
Cite as
William John Gowers and James Laird. Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{gowers_et_al:LIPIcs.CALCO.2017.13,
author = {Gowers, William John and Laird, James},
title = {{Sequoidal Categories and Transfinite Games: A Coalgebraic Approach to Stateful Objects in Game Semantics}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {13:1--13:17},
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.13},
URN = {urn:nbn:de:0030-drops-80454},
doi = {10.4230/LIPIcs.CALCO.2017.13},
annote = {Keywords: Game Semantics, Stateful Languages, Transfinite Games, Sequoid Operator}
}
Document
Free Constructions and Coproducts of d-Frames
Abstract
A general theory of presentations for d-frames does not yet exist. We review the difficulties and give sufficient conditions for when they can be overcome. As an application we prove that the category of d-frames is closed under coproducts.
Cite as
Tomás Jakl and Achim Jung. Free Constructions and Coproducts of d-Frames. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{jakl_et_al:LIPIcs.CALCO.2017.14,
author = {Jakl, Tom\'{a}s and Jung, Achim},
title = {{Free Constructions and Coproducts of d-Frames}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {14:1--14:15},
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.14},
URN = {urn:nbn:de:0030-drops-80304},
doi = {10.4230/LIPIcs.CALCO.2017.14},
annote = {Keywords: Free construction, d-frame, coproduct, C-ideals}
}
Document
UML Interactions Meet State Machines - An Institutional Approach
Abstract
UML allows the multi-viewpoint modelling of systems. One important question is whether an interaction as specified by a sequence diagram can be actually realised in the system. Here, the latter is specified as a combination of several state machines (one for each lifeline in the interaction) by a composite structure diagram. In order to tackle this question, we formalise the involved UML diagram types as institutions, and their relations as institution (co)morphisms.
Cite as
Alexander Knapp and Till Mossakowski. UML Interactions Meet State Machines - An Institutional Approach. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{knapp_et_al:LIPIcs.CALCO.2017.15,
author = {Knapp, Alexander and Mossakowski, Till},
title = {{UML Interactions Meet State Machines - An Institutional Approach}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {15:1--15:15},
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.15},
URN = {urn:nbn:de:0030-drops-80346},
doi = {10.4230/LIPIcs.CALCO.2017.15},
annote = {Keywords: UML, state machines, interactions, composite structure diagrams, institutions, multi-view consistency}
}
Document
Being Van Kampen in Presheaf Topoi is a Uniqueness Property
Abstract
Fibred semantics is the foundation of the model-instance pattern of software engineering. Software models can often be formalized as objects of presheaf topoi, e.g. the category of directed graphs. Multimodeling requires to construct colimits of diagrams of single models and their instances, while decomposition of instances of the multimodel is given by pullback. Compositionality requires an exact interplay of these operations, i.e., the diagrams must enjoy the Van Kampen property. However, checking the validity of the Van Kampen property algorithmically based on its definition is often impossible.
In this paper we state a necessary and sufficient yet easily checkable condition for the Van Kampen property to hold for diagrams in presheaf topoi. It is based on a uniqueness property of path-like structures within the defining congruence classes that make up the colimiting cocone of the models. We thus add to the statement "Being Van Kampen is a Universal Property" by Heindel and Sobocinski presented at CALCO 2009 the fact that the Van Kampen property reveals a set-based structural uniqueness feature.
Cite as
Harald König and Uwe Wolter. Being Van Kampen in Presheaf Topoi is a Uniqueness Property. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{konig_et_al:LIPIcs.CALCO.2017.16,
author = {K\"{o}nig, Harald and Wolter, Uwe},
title = {{Being Van Kampen in Presheaf Topoi is a Uniqueness Property}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {16:1--16:15},
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.16},
URN = {urn:nbn:de:0030-drops-80320},
doi = {10.4230/LIPIcs.CALCO.2017.16},
annote = {Keywords: Van Kampen Cocone, Presheaf Topos, Fibred Semantics, Mapping Path}
}
Document
Custom Hypergraph Categories via Generalized Relations
Abstract
Process theories combine a graphical language for compositional reasoning with an underlying categorical semantics. They have been successfully applied to fields such as quantum computation, natural language processing, linear dynamical systems and network theory. When investigating a new application, the question arises of how to identify a suitable process theoretic model.
We present a conceptually motivated parameterized framework for the construction of models for process theories. Our framework generalizes the notion of binary relation along four axes of variation, the truth values, a choice of algebraic structure, the ambient mathematical universe and the choice of proof relevance or provability. The resulting categories are preorder-enriched and provide analogues of relational converse and taking graphs of maps. Our constructions are functorial in the parameter choices, establishing mathematical connections between different application domains. We illustrate our techniques by constructing many existing models from the literature, and new models that open up ground for further development.
Cite as
Dan Marsden and Fabrizio Genovese. Custom Hypergraph Categories via Generalized Relations. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{marsden_et_al:LIPIcs.CALCO.2017.17,
author = {Marsden, Dan and Genovese, Fabrizio},
title = {{Custom Hypergraph Categories via Generalized Relations}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {17:1--17:16},
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.17},
URN = {urn:nbn:de:0030-drops-80494},
doi = {10.4230/LIPIcs.CALCO.2017.17},
annote = {Keywords: Process Theory, Categorical Compositional Semantics, Generalized Relations, Hypergraph Category, Compact Closed Category}
}
Document
Proper Functors and their Rational Fixed Point
Abstract
The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g. for weighted automata.
Cite as
Stefan Milius. Proper Functors and their Rational Fixed Point. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{milius:LIPIcs.CALCO.2017.18,
author = {Milius, Stefan},
title = {{Proper Functors and their Rational Fixed Point}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {18:1--18:16},
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.18},
URN = {urn:nbn:de:0030-drops-80314},
doi = {10.4230/LIPIcs.CALCO.2017.18},
annote = {Keywords: proper functor, proper semiring, coalgebra, rational fixed point}
}
Document
A Classical Groupoid Model for Quantum Networks
Abstract
We give a mathematical analysis of a new type of classical computer network architecture, intended as a model of a new technology that has recently been proposed in industry. Our approach is based on groubits, generalizations of classical bits based on groupoids. This network architecture allows the direct execution of a number of protocols that are usually associated with quantum networks, including teleportation, dense coding and secure key distribution.
Cite as
David Reutter and Jamie Vicary. A Classical Groupoid Model for Quantum Networks. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.19,
author = {Reutter, David and Vicary, Jamie},
title = {{A Classical Groupoid Model for Quantum Networks}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {19:1--19:18},
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.19},
URN = {urn:nbn:de:0030-drops-80391},
doi = {10.4230/LIPIcs.CALCO.2017.19},
annote = {Keywords: groupoids, networks, quantum, semantics, key distribution}
}
Document
A 2-Categorical Approach to Composing Quantum Structures
Abstract
We present an infinite number of construction schemes for quantum structures, including unitary error bases, Hadamard matrices, quantum Latin squares and controlled families, many of which have not previously been described. Our results rely on the type structure of biunitary connections, 2-categorical structures which play a central role in the theory of planar algebras. They have an attractive graphical calculus which allows simple correctness proofs for the constructions we present. We apply these techniques to construct a unitary error basis that cannot be built using any previously known method.
Cite as
David Reutter and Jamie Vicary. A 2-Categorical Approach to Composing Quantum Structures. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.20,
author = {Reutter, David and Vicary, Jamie},
title = {{A 2-Categorical Approach to Composing Quantum Structures}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {20:1--20:20},
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.20},
URN = {urn:nbn:de:0030-drops-80389},
doi = {10.4230/LIPIcs.CALCO.2017.20},
annote = {Keywords: quantum constructions, 2-category, graphical calculus, planar algebra}
}
Document
Uniform Interpolation in Coalgebraic Modal Logic
Abstract
A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
Cite as
Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform Interpolation in Coalgebraic Modal Logic. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{seifan_et_al:LIPIcs.CALCO.2017.21,
author = {Seifan, Fatemeh and Schr\"{o}der, Lutz and Pattinson, Dirk},
title = {{Uniform Interpolation in Coalgebraic Modal Logic}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {21:1--21:16},
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.21},
URN = {urn:nbn:de:0030-drops-80415},
doi = {10.4230/LIPIcs.CALCO.2017.21},
annote = {Keywords: modal logic, coalgebraic logic, uniform interpolation, preservation of weak pullbacks}
}
Document
Termination in Convex Sets of Distributions
Abstract
Convex algebras, also called (semi)convex sets, are at the heart of modelling probabilistic systems including probabilistic automata. Abstractly, they are the Eilenberg-Moore algebras of the
finitely supported distribution monad. Concretely, they have been studied for decades within algebra and convex geometry.
In this paper we study the problem of extending a convex algebra by a single point. Such extensions enable the modelling of termination in probabilistic systems. We provide a full description of all possible extensions for a particular class of convex algebras: For a fixed convex subset D of a vector space satisfying additional technical condition, we consider the algebra of convex subsets of D. This class contains the convex algebras of convex subsets of distributions, modelling (nondeterministic) probabilistic automata. We also provide a full description of all possible extensions for the class of free convex algebras, modelling fully probabilistic systems.
Finally, we show that there is a unique functorial extension, the so-called black-hole extension.
Cite as
Ana Sokolova and Harald Woracek. Termination in Convex Sets of Distributions. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{sokolova_et_al:LIPIcs.CALCO.2017.22,
author = {Sokolova, Ana and Woracek, Harald},
title = {{Termination in Convex Sets of Distributions}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {22:1--22:16},
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.22},
URN = {urn:nbn:de:0030-drops-80434},
doi = {10.4230/LIPIcs.CALCO.2017.22},
annote = {Keywords: convex algebra, one-point extensions, convex powerset monad}
}
Document
Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence
Abstract
We present a new proof system for equality of terms which present elements of the final coalgebra of a finitary set functor. This is most important when the functor is finitary, and we improve on logical systems which have already been proposed in several papers. Our contributions here are (1) a new logical rule which makes for proofs which are somewhat easier to find, and (2) a soundness/completeness theorem which works for all finitary functors, in particular removing a weak pullback preservation requirement that had been used previously. Our work is based on properties of precongruence relations and also on a new parametrized coinduction principle.
Cite as
David Sprunger and Lawrence S. Moss. Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{sprunger_et_al:LIPIcs.CALCO.2017.23,
author = {Sprunger, David and Moss, Lawrence S.},
title = {{Precongruences and Parametrized Coinduction for Logics for Behavioral Equivalence}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {23:1--23:15},
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.23},
URN = {urn:nbn:de:0030-drops-80474},
doi = {10.4230/LIPIcs.CALCO.2017.23},
annote = {Keywords: precongruence, kernel bisimulation, finitary functor, coalgebra, behavioural equivalence}
}
Document
Finite Behaviours and Finitary Corecursion
Abstract
In the coalgebraic approach to state-based systems, semantics is captured up to behavioural equivalence by special coalgebras such as the final coalgebra, the final locally finitely presentable coalgebra (Adámek, Milius, and Velebil), or the final locally finitely generated coalgebra (Milius, Pattinson, and Wißmann). The choice of the proper semantic domain is determined by finiteness restrictions imposed on the systems of interest. We propose a unifying perspective by introducing the concept of a final locally (I,M)-presentable coalgebra, where the two parameters I and M determine what a "finite" system is. Under suitable conditions on the categories and type functors, we show that the final locally (I,M)-presentable coalgebra exists and coincides with the initial (I,M)-iterative algebra, thereby putting a common roof over several results on iterative, fg-iterative and completely iterative algebras that were given a separate treatment before.
Cite as
Henning Urbat. Finite Behaviours and Finitary Corecursion. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{urbat:LIPIcs.CALCO.2017.24,
author = {Urbat, Henning},
title = {{Finite Behaviours and Finitary Corecursion}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {24:1--24:16},
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.24},
URN = {urn:nbn:de:0030-drops-80444},
doi = {10.4230/LIPIcs.CALCO.2017.24},
annote = {Keywords: Iterative algebra, completely iterative algebra, fg-iterative algebra, rational fixpoint, terminal coalgebra, iterative monad}
}
Document
The EfProb Library for Probabilistic Calculations
Abstract
EfProb is an abbreviation of Effectus Probability. It is the name of
a library for probability calculations in Python. EfProb offers a
uniform language for discrete, continuous and quantum probability.
For each of these three cases, the basic ingredients of the language
are states, predicates, and channels. Probabilities are typically
calculated as validities of predicates in states. States can be
updated (conditioned) with predicates. Channels can be used for state
transformation and for predicate transformation. This short paper
gives an overview of the use of EfProb.
Cite as
Kenta Cho and Bart Jacobs. The EfProb Library for Probabilistic Calculations. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 25:1-25:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
Copy BibTex To Clipboard
@InProceedings{cho_et_al:LIPIcs.CALCO.2017.25,
author = {Cho, Kenta and Jacobs, Bart},
title = {{The EfProb Library for Probabilistic Calculations}},
booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
pages = {25:1--25:8},
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.25},
URN = {urn:nbn:de:0030-drops-80529},
doi = {10.4230/LIPIcs.CALCO.2017.25},
annote = {Keywords: probability, embedded language, effectus theory}
}