Distribution Bisimilarity via the Power of Convex Algebras

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

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2021-01, Vol.17, Issue 3
Main Authors: Bonchi, Filippo, Silva, Alexandra, Sokolova, Ana
Format: Article
Language:English
Subjects:
computer science - logic in computer science
d.2.4
f.1.2
f.3
g.3
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1860-5974
1860-5974
DOI:10.46298/lmcs-17(3:10)2021