paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Coalgebraic trace semantics via forgetful logics

基于遗忘逻辑的余代数迹语义
LMCS vol.Volume 12, Issue 42017匹配度 2/10 · 该论文属于余代数、模态逻辑与自动机迹语义的形式语义研究，与用户画像核心关注的静态分析、LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析均无直接关系，仅在“PL 形式语义/形式化验证”大方向上有较远邻近性。引用 43 inbox
Bartek Klin, Jurriaan Rot
形式语义逻辑与自动机
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：提出用遗忘模态逻辑统一刻画余代数迹语义，并给出其与确定化构造一致及典范确定化存在的条件。

本文以模态逻辑为统一框架研究余代数的迹语义，特别是通过遗忘逻辑（forgetful logics）将逻辑语义与行为语义联系起来。作者以加权自动机、交替自动机、树自动机的语言语义以及生成式概率系统的迹语义等为例，展示该方法的表达力和灵活性。文中给出一个充分条件，保证由逻辑语义定义的迹与经由给定确定化构造得到的迹语义一致；进一步提出一个条件，确保存在相对于给定逻辑语义正确的典范确定化过程，并指出该过程与 Brzozowski 最小化算法密切相关。

问题
如何在统一的范畴与逻辑框架下刻画余代数系统的迹语义，并使其与具体自动机及概率系统的语言或迹语义相对应。
方法
采用模态逻辑，尤其是遗忘逻辑，作为余代数迹语义的框架，给出逻辑语义与确定化所得迹语义一致的条件，并刻画相对于逻辑语义正确的典范确定化过程。
评估
通过加权自动机、交替自动机、树自动机以及生成式概率系统等具体实例展示方法的适用性，并将其典范确定化过程与 Brzozowski 最小化算法建立联系。
原文摘要（Abstract）

We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is closely related to Brzozowski's minimization algorithm.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{KlinR15,
  title = {Coalgebraic trace semantics via forgetful logics},
  author = {Bartek Klin and Jurriaan Rot},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 12, Issue 4},
  year = {2017},
  doi = {10.2168/lmcs-12(4:10)2016}
}