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.

翻译：概率自动分析(PA)也被称为概率非决定性的过渡系统,将概率和非确定性标签的过渡系统结合起来。它们可以被赋予不同的语义学,比如强烈的双异性、二次相异性或(最近)两异性分布。后者以PA作为概率分布变异器的观点为基础,也称为信仰状态,并促进向一流公民的分布。我们给出了两个相异性分布的焦格模型,并解释了信仰-状态变异器由PA产生的起源。为了做到这一点,我们明确了PA中存在的共振代数结构,并将信仰-状态变异器确定为带有矩形变异体空间的转型系统。作为我们抽象方法的结果,我们可以提供一种我们称之为振动至锥形体的精确验证技术。