AI 中文总结
本文从细粒度复杂度理论角度，基于3k-团等假设证明下推模型检测现有算法的时间下界，提出2NPDA(k)假设并通过线性归约网络佐证，解释该问题长期无更优算法的原因。
AI 中文摘要
递归程序验证中的许多问题都可归约为下推模型检测问题。该问题的输入为栈字母表大小为常数的下推自动机（PDA），以及由若干非确定有限自动机（NFA）的交集所描述的不良行为集合，问题是判定PDA是否存在属于该不良行为集合的行为。众所周知，该问题存在一种运行时间为$O(n^{2k} |Σ| + n^{3k})$的算法，其中$n$是PDA和各NFA的最大状态数，$Σ$是公共输入字母表，$k-1$是NFA的数量。尽管该问题十分重要，但目前尚未发现更优的算法。\n 本文通过细粒度复杂度理论的视角，解释了这一进展停滞的原因。我们证明：若3k-团假设（对应地，组合3k-团假设）成立，则对任意$ε> 0$，不存在运行时间为$O((n^{(ω-1)k} |Σ| + n^{ωk})^{1-ε})$的算法（对应地，组合算法），其中$ω$是矩阵乘法指数。此外，基于组合假设，我们还证明：对于输入字母表大小为常数的下推模型检测，对任意$ε> 0$，都无法在快于$O(n^{3(k-1)-ε})$的时间内求解。\n 最后，我们探究了该问题是否存在$O(N^{3k-ε})$时间算法的可能性，其中$N$是输入的总比特数。我们提出了一个新假设——2NPDA$(k)$假设，用于解释为何该问题缺乏$O(N^{3k-ε})$时间算法。为支撑该假设，我们展示了2NPDA$(k)$假设、下推模型检测以及形式语言与自动机理论中其他问题之间的一组线性时间归约网络。
英文摘要
Many problems in the verification of recursive programs can be reduced to pushdown model checking. In this problem, we are given as input a pushdown automaton (PDA) over a constant-sized stack alphabet, and a description of undesirable behaviors given by an intersection of NFAs, and the problem is to decide if there is a behavior of the PDA that belongs to the set of undesirable behaviors. It is well-known that there is an algorithm for this problem that runs in time $O(n^{2k} |Σ| + n^{3k})$, where $n$ is the maximum number of states of the PDA and the NFAs, $Σ$ is the common input alphabet, and $k-1$ is the number of NFAs. Despite the importance of this problem, no better algorithm is known for it. In this paper, we provide an explanation for this lack of progress using the lens of fine-grained complexity theory. We prove that if the $3k$-Clique hypothesis (resp. combinatorial $3k$-Clique hypothesis) is true, then for any $ε> 0$, there is no algorithm (resp. combinatorial algorithm) that solves this problem in time $O((n^{(ω-1)k} |Σ| + n^{ωk})^{1-ε})$ (resp. $O((n^{2k} |Σ| + n^{3k})^{1-ε})$) where $ω$ is the matrix multiplication exponent. Furthermore, using the combinatorial hypothesis, we also show that pushdown model checking over constant-sized input alphabets cannot be solved in time faster than $O(n^{3(k-1)-ε})$ for any $ε> 0$. Finally, we investigate the possibility of an $O(N^{3k-ε})$ time algorithm for this problem where $N$ is the total bit size of the input. We formulate a new hypothesis, the 2NPDA$(k)$ hypothesis, that helps explain the lack of $O(N^{3k-ε})$ time algorithms for this problem. To corroborate this hypothesis, we show a web of linear-time reductions between the 2NPDA$(k)$ hypothesis, pushdown model checking, and other problems in formal language and automata theory.
CommentsFull version of the LICS 2025 paper "Pushdown Model Checking above the Cubic Bottleneck". Abstract shortened to fit arXiv requirements
