paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete

一阶文法的互模拟等价性是 ACKERMANN-完全的
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 2/10 · 该论文属于逻辑与自动机、形式语义领域的纯复杂度理论结果，研究下推自动机/一阶文法的互模拟等价判定复杂度，与用户关注的 PL/AI、Agent、浮点程序分析、贝叶斯程序分析等核心方向没有直接关联。虽然形式验证是相近领域，但本文不涉及 LLM/Agent、静态分析工具或工业落地，匹配度较低。引用 4 inbox
Petr Jancar, Sylvain Schmitz
逻辑与自动机形式语义
crossref: 2026-09-12

AI 速览

一句话：首次给出下推自动机弱互模拟等价判定的 ACKERMANN 复杂度上界，并证明其最优。

本文研究两个带受限静默动作的下推自动机是否弱互模拟等价这一经典判定问题。Sénizergues 曾证明该问题可判定，但其复杂度上界长期未知。作者在一阶文法的等价框架下进行复杂度分析，首次给出 ACKERMANN 上界，并证明该上界与已知下界匹配，从而得到 ACKERMANN-完全性。作为补充，论文还证明当自动机状态数固定时，强互模拟等价性是原始递归的。该结果刻画了互模拟等价判定在自动机与形式语言层面的精确计算复杂度。

问题
判定带受限静默动作的两个下推自动机是否弱互模拟等价，其可判定性已知但复杂度上界未知；等价地，判定一阶文法的互模拟等价性。
方法
在一阶文法框架下开展复杂度分析，给出 ACKERMANN 上界并结合下界完成完全性证明；同时分析固定状态数下的强互模拟情形。
评估
理论复杂度证明：弱互模拟等价为 ACKERMANN-完全，且固定状态数下强互模拟等价为原始递归。
原文摘要（Abstract）

Checking whether two pushdown automata with restricted silent actions are weakly bisimilar was shown decidable by Sénizergues (1998, 2005). We provide the first known complexity upper bound for this famous problem, in the equivalent setting of first-order grammars. This ACKERMANN upper bound is optimal, and we also show that strong bisimilarity is primitive-recursive when the number of states of the automata is fixed.

链接与引用

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

BibTeX 
@inproceedings{paperbot5025,
  title = {Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete},
  author = {Petr Jancar and Sylvain Schmitz},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785848}
}