paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Bisimulation Finiteness of Pushdown Systems Is Elementary

下推系统的互模拟有限性是初等的
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10 · 该论文属于下推系统互模拟可判定性与复杂度的纯自动机/形式语义理论结果，虽与形式化验证领域相邻，但既不涉及 LLM/Agent 与静态分析的交叉，也与浮点程序分析和贝叶斯程序分析无关；同时是纯理论证明，缺少用户偏好的工程实现、工业落地或 benchmark 驱动的成分。引用 1 inbox
Stefan Göller, Paweł Parys
形式语义逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明若下推系统互模拟等价于有限系统，则存在规模初等有界的有限等价系统，从而该判定问题是初等可判定的。

论文研究下推系统的互模拟有限性问题：给定下推系统，判定它是否与某个有限系统互模拟等价。此前该问题已知可判定，但最好上界为 Ackermann 级。作者证明了一个更强的定量结果：若下推系统与有限系统互模拟等价，则已存在一个与其互模拟等价的有限系统，其规模在原下推系统描述规模上是初等有界的。作为推论，互模拟有限性判定问题是初等可判定的，从而将此前最优的 Ackermann 上界显著改进为初等上界。

问题
判定给定下推系统是否与某个有限系统互模拟等价（互模拟有限性），并降低该判定问题的复杂度上界。
方法
通过证明若存在有限互模拟等价系统，则存在规模在原下推系统描述规模上初等有界的有限等价系统。
评估
理论证明；由此得到互模拟有限性判定问题是初等可判定的，并将已知 Ackermann 上界改进为初等上界。
原文摘要（Abstract）

We show that in case a pushdown system is bisimulation equivalent to a finite system, there is already a bisimulation equivalent finite system whose size is elementarily bounded in the description size of the pushdown system. As a consequence we obtain that it is elementarily decidable if a given pushdown system is bisimulation equivalent to some finite system. This improves a previously best-known ACKERMANN upper bound for this problem.

链接与引用

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

BibTeX 
@inproceedings{paperbot5511,
  title = {Bisimulation Finiteness of Pushdown Systems Is Elementary},
  author = {Stefan Göller and Paweł Parys},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394827}
}