paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)

Max-Plus 自动机的 Big-O 问题是可判定的（PSPACE-完全）
LICS 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2023匹配度 1/10 · 该论文属于自动机与形式语言理论，研究 max-plus 自动机的 big-O 可判定性，与用户关注的 PL/AI 交叉、静态分析、浮点程序分析、贝叶斯程序分析以及 LLM/Agent 等方向没有直接关联。引用 4 inbox
Laure Daviaud, David Purser
逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：证明 max-plus 自动机的 big-O（仿射支配）问题可判定，且为 PSPACE-完全。

本文研究 max-plus 自动机（即定义在 (ℕ∪{-∞}, max, +) 半环上的加权自动机）的 big-O 问题，也称仿射支配问题：给定分别计算函数 f 和 g 的两个 max-plus 自动机，判定是否存在常数 c 使得 f ≤ cg + c。该问题是不可判定的包含问题 f ≤ g 的一种松弛。作者证明该问题可判定，并精确刻画其复杂度为 PSPACE-完全。证明工具是 Simon 森林因子分解定理，核心在于在有限半群中检测称为 witness 的特定元素；该半群对 stabilisation 和 flattening 两种操作封闭。

问题
研究 max-plus 自动机的 big-O/仿射支配问题：给定计算 f 和 g 的两个自动机，判定是否存在常数 c 使 f ≤ cg + c。它是不可判定包含问题 f ≤ g 的松弛。
方法
利用 Simon 森林因子分解定理，通过检测有限半群中的 witness 元素来给出判定过程；该半群对 stabilisation 与 flattening 封闭。
评估
以可判定性证明和复杂度分析评估，证明该问题可判定并属于 PSPACE，同时给出 PSPACE-完全性。
原文摘要（Abstract）

We show that the big-O problem for max-plus automata, i.e. weighted automata over the semiring (ℕ ∪ {–∞}, max, +), is decidable and PSPACE-complete. The big-O (or affine domination) problem asks whether, given two max-plus automata computing functions f and g, there exists a constant c such that f ≤ cg + c. This is a relaxation of the containment problem asking whether f ≤ g, which is undecidable. Our decidability result uses Simon’s forest factorisation theorem, and relies on detecting specific elements, that we call witnesses, in a finite semigroup closed under two special operations: stabilisation and flattening.

链接与引用

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

BibTeX 
@inproceedings{abs-2304-05229,
  title = {The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)},
  author = {Laure Daviaud and David Purser},
  booktitle = {LICS},
  year = {2023},
  doi = {10.1109/lics56636.2023.10175798}
}