paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Distribution Bisimilarity via the Power of Convex Algebras

借助凸代数幂的分布双相似性
LMCS vol.Volume 17, Issue 32021匹配度 2/10 · 论文研究概率自动机的分布双相似性,属于纯形式语义/余代数理论,与用户关注的静态分析、LLM/Agent 与形式化验证交叉、浮点程序分析及贝叶斯程序分析均无直接关联。引用 5 inbox
Filippo Bonchi, Alexandra Silva, Ana Sokolova
crossref: 2026-09-10

AI 速览

一句话:用余代数与凸代数统一刻画概率自动机的分布双相似性,并给出直到凸包的互模拟证明技术。

概率自动机(PA)同时包含概率与非确定性,可赋予强双相似性、凸双相似性以及较新的分布双相似性等语义。分布双相似性将 PA 视为概率分布(信念状态)的变换器,使分布成为一等公民。本文给出分布双相似性的余代数刻画,阐明信念状态变换器如何从 PA 产生;通过显式暴露 PA 中已有的凸代数结构,将信念状态变换器识别为状态空间承载凸代数的迁移系统。作为该抽象方法的结果,作者提出一种称为“直到凸包的双模拟”的可靠证明技术。

问题
如何从余代数视角统一理解概率自动机的分布双相似性,并解释信念状态变换器的来源。
方法
显式刻画 PA 的凸代数结构,将信念状态变换器建模为状态空间带凸代数的迁移系统,并给出余代数式定义。
评估
理论推导为主:由抽象框架导出“直到凸包的双模拟”这一可靠证明技术,用于证明分布双相似性。
原文摘要(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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}