paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A coalgebraic take on regular and $\omega$-regular behaviours

正则与 ω-正则行为的余代数视角
LMCS vol.Volume 17, Issue 42021匹配度 2/10 · 该论文是纯余代数/自动机理论研究，虽与形式化验证的基础理论有间接联系，但未涉及用户核心关注的 LLM/Agent 交叉、静态分析应用、浮点程序分析或贝叶斯程序分析。引用 0 inbox
Tomasz Brengos
形式语义逻辑与自动机
crossref: 2026-09-10

AI 速览

一句话：在 monad 余代数框架下统一刻画有限与 ω-正则行为，并给出对应 Kleene 定理及多类自动机实例。

本文提出一个统一的余代数框架，用于定义类型为 monad 的系统的有限行为与带 Büchi 接受条件的无限行为。作者首先构造了一个适合建模有限与无限行为的 monad，随后给出余代数自动机及其（ω-）行为的概念。论文最后证明针对（ω-）正则输入的余代数 Kleene 型定理，并将该框架实例化于非确定（Büchi）自动机、树自动机和概率自动机。该工作以范畴论与余代数方法统一了经典自动机理论中正则与 ω-正则行为的语义，并为不同计算模型提供了可复用的理论模板。

问题
如何为不同类型的系统（非确定、树、概率等）的有限与无限 ω-正则行为提供统一的余代数语义框架。
方法
在类型为 monad 的余代数系统中定义自动机及其（ω-）行为，构造适合建模有限/无限行为的 monad，并证明针对（ω-）正则输入的 Kleene 型定理。
评估
评估以理论实例化为主：将框架应用于非确定（Büchi）自动机、树自动机和概率自动机，说明其覆盖范围。
原文摘要（Abstract）

We present a general coalgebraic setting in which we define finite and infinite behaviour with B\"uchi acceptance condition for systems whose type is a monad. The first part of the paper is devoted to presenting a construction of a monad suitable for modelling (in)finite behaviour. The second part of the paper focuses on presenting the concepts of a (coalgebraic) automaton and its ($\omega$-) behaviour. We end the paper with coalgebraic Kleene-type theorems for ($\omega$-) regular input. The framework is instantiated on non-deterministic (B\"uchi) automata, tree automata and probabilistic automata.

链接与引用

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

BibTeX 
@article{paperbot1252,
  title = {A coalgebraic take on regular and $\omega$-regular behaviours},
  author = {Tomasz Brengos},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 4},
  year = {2021},
  doi = {10.46298/lmcs-17(4:24)2021}
}