Bonchi, F;
Silva, A;
Sokolova, A;
(2021)
Distribution Bisimilarity via the Power of Convex Algebras.
Logical Methods in Computer Science
, 17
(3)
10:1-10:28.
10.46298/LMCS-17(3:10)2021.
Preview |
Text
1707.02344.pdf - Published Version Download (524kB) | Preview |
Abstract
Probabilistic automata (PA), also known as probabilistic nondeterministic labelled transition systems, combine probability and nondeterminism. They can be given different semantics, like strong bisimilarity, convex bisimilarity, or (more recently) distribution bisimilarity. The latter is based on the view of PA as transformers of probability distributions, also called belief states, and promotes distributions to first-class citizens. We give a coalgebraic account of distribution bisimilarity, and explain the genesis of the belief-state transformer from a PA. To do so, we make explicit the convex algebraic structure present in PA and identify belief-state transformers as transition systems with state space that carries a convex algebra. As a consequence of our abstract approach, we can give a sound proof technique which we call bisimulation up-to convex hull.
| Type: | Article |
|---|---|
| Title: | Distribution Bisimilarity via the Power of Convex Algebras |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.46298/LMCS-17(3:10)2021 |
| Publisher version: | https://doi.org/10.46298/LMCS-17(3:10)2021 |
| Language: | English |
| Additional information: | This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany |
| Keywords: | Science & Technology, Technology, Computer Science, Theory & Methods, Logic, Computer Science, Science & Technology - Other Topics, belief-state transformers, bisimulation up-to, coalgebra, convex algebra, convex powerset monad, distribution bisimilarity, probabilistic automata, BISIMULATION, VERIFICATION, EQUIVALENCE, SEMANTICS, SYSTEMS, PROBABILITY |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10133869 |
Archive Staff Only
 |
View Item |
