一句话:用余代数与凸代数统一刻画概率自动机的分布双相似性,并给出直到凸包的互模拟证明技术。
概率自动机(PA)同时包含概率与非确定性,可赋予强双相似性、凸双相似性以及较新的分布双相似性等语义。分布双相似性将 PA 视为概率分布(信念状态)的变换器,使分布成为一等公民。本文给出分布双相似性的余代数刻画,阐明信念状态变换器如何从 PA 产生;通过显式暴露 PA 中已有的凸代数结构,将信念状态变换器识别为状态空间承载凸代数的迁移系统。作为该抽象方法的结果,作者提出一种称为“直到凸包的双模拟”的可靠证明技术。
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.
@article{paperbot1294,
title = {Distribution Bisimilarity via the Power of Convex Algebras},
author = {Filippo Bonchi and Alexandra Silva and Ana Sokolova},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:10)2021}
}