paperbot · PL 论文追踪

全部论文 待读 收藏

P2 One Theorem to Rule Them All

一个定理统御一切
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 论文研究LTL到确定性Rabin、极限确定Büchi和非确定Büchi自动机的统一翻译，属于逻辑与自动机理论、形式化验证基础，但与用户核心方向（LLM/Agent与静态分析/形式化验证交叉、浮点程序分析、贝叶斯程序分析）没有直接关联，也未涉及LLM/Agent或工程落地。引用 27 inbox
Javier Esparza, Jan Křetínský, Salomon Sickert
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：提出一个统一主定理，将 LTL 公式翻译为确定性 Rabin、极限确定 Büchi 和非确定 Büchi 自动机，均达渐近最优规模。

本文研究线性时序逻辑（LTL）到不同 ω-自动机的翻译。传统构造分别使用 Safra、ranking、breakpoint 等复杂技术，且缺乏统一框架。作者提出一个纯逻辑的 Master Theorem，将 LTL 公式的语言分解为若干可用基本手段翻译成 ω-自动机的语言的正布尔组合。基于该定理，他们统一导出三种翻译：确定性 Rabin 自动机、极限确定 Büchi 自动机和非确定 Büchi 自动机。所得自动机具有渐近最优规模：确定性 Rabin 为双指数，极限确定 Büchi 与非确定 Büchi 为单指数。该工作表明无需 Safra、ranking 或 breakpoint 构造即可完成这些翻译，为 LTL 自动机构造提供了统一且简洁的理论基础。

问题
LTL 到确定性 Rabin、极限确定 Büchi 和非确定 Büchi 自动机的翻译通常各自依赖 Safra、ranking、breakpoint 等复杂专用构造，缺乏统一且简洁的框架。
方法
提出一个纯逻辑的主定理，将公式语言分解为可基本翻译成 ω-自动机的语言的正布尔组合，并由该定理统一导出三种自动机翻译。
评估
通过理论证明与渐近规模分析表明翻译正确且自动机规模最优，不依赖 Safra、ranking 或 breakpoint 构造。
原文摘要（Abstract）

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into ω-automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.

链接与引用

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

BibTeX 
@inproceedings{paperbot4314,
  title = {One Theorem to Rule Them All},
  author = {Javier Esparza and Jan Křetínský and Salomon Sickert},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209161}
}