一句话：证明 Max-Plus 自动机的 Big-O（仿射支配）问题可判定，且复杂度为 PSPACE-完全。
本文研究 Max-Plus 自动机的 Big-O 问题，也称仿射支配问题：给定两个 Max-Plus 自动机计算的函数 f 与 g，判定是否存在常数 c 使得 f < cg + c。该问题是不可判定的包含问题 f < g 的一种松弛。作者证明该问题可判定，并精确确定其复杂度为 PSPACE-完全。证明技术基于 Simon 的森林因子分解定理，核心是在一个对稳定化（stabilisation）与扁平化（flattening）两种特殊运算封闭的有限半群中检测特定元素，称为见证（witnesses）。该结果给出了 Max-Plus 自动机支配关系判定问题的可判定性与精确复杂度刻画。
We show that the big-O problem for max-plus automata 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.
@article{paperbot3399,
title = {The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)},
author = {Laure Daviaud and David Purser and Marie Tcheng},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:3)2025}
}