paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Initial Algebra Correspondence under Reachability Conditions

可达性条件下的初始代数对应
LICS 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2025匹配度 3/10 · 该论文属于范畴论/形式语义方向,讨论转移系统不动点语义与可达性条件,与画像核心关注的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析交叉较少。仅与形式化验证/程序语义有间接关联,未涉及工程实现、工业落地或 LLM 工具。引用 0 inbox
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot
crossref: 2026-09-12

AI 速览

一句话:提出统一范畴框架,用伴随刻画可达性条件,使转移系统的两种不动点/初始代数语义一致,并实例化到马尔可夫链与自动机。

许多转移系统存在两种不同的不动点语义,例如马尔可夫链上的全期望奖励与部分期望奖励语义;在适当条件下二者恰好一致,如几乎必然可达时。本文提出一个统一的范畴框架来刻画这类可达性条件,保证两种语义之间的对应。该框架通过适当的伴随自然导出抽象可达性条件,从而证明不动点乃至更一般的初始代数之间的重合。作者给出若干实例以展示其一般性,包括马尔可夫链的几乎必然可达条件和自动机的无歧义条件;并进一步利用逐点 Kan 扩张研究马尔可夫决策过程实例的规范构造。

问题
如何用统一的条件解释不同转移系统(如马尔可夫链、马尔可夫决策过程、自动机)中两种不动点或初始代数语义何时一致?
方法
在范畴论中通过适当伴随导出抽象可达性条件,并借助逐点 Kan 扩张给出马尔可夫决策过程实例的规范构造。
评估
通过实例化展示框架的一般性,包括马尔可夫链的几乎必然可达条件与自动机的无歧义条件,并研究马尔可夫决策过程实例的构造。
原文摘要(Abstract)

Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost sure reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions.

链接与引用

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

BibTeX
@inproceedings{paperbot8652,
  title = {Initial Algebra Correspondence under Reachability Conditions},
  author = {Mayuko Kori and Kazuki Watanabe and Jurriaan Rot},
  booktitle = {LICS},
  year = {2025},
  doi = {10.1109/lics65433.2025.00013}
}