一句话：证明下推模型检测的 O(n^{2k}|Σ|+n^{3k}) 上界在 3k-clique 假设下已接近最优。
论文研究递归程序验证中的核心问题——下推模型检测：给定常量栈字母表的下推自动机（PDA）和若干 NFA 的交表示不良行为，判定 PDA 是否产生不良行为。自 1960 年代以来，已知 O(n^{2k}|Σ|+n^{3k}) 时间算法，但长期无改进。作者用细粒度复杂度理论解释该瓶颈，证明若 3k-clique 假设成立，则不存在 (n^{2k}|Σ|+n^{3k})^{1−ε} 时间算法；该下界对确定性机器乃至确定性单计数器机仍成立，常量字母表下也需 Ω(n^{3(k−1)−ε})。针对按输入比特大小 N 的 O(N^{3k−ε}) 算法，作者提出 2NPDA(k) 假设，并给出其与下推模型检测及语言/自动机问题之间的线性时间归约网络。
It is well known that various problems in program analysis and 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, representing the program, 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(n2k|Σ| + n3k), where n is the maximum number of states of the PDA and the NFAs, Σ is the common alphabet of these machines, and k − 1 is the number of NFAs used to specify the violations. Despite the importance of this problem, no better algorithm is known for it since the 1960s.In this paper, we provide an explanation for this lack of progress using the lens of fine-grained complexity theory. More precisely, we prove that if the (combinatorial) 3k-clique hypothesis is true, then there is no algorithm that solves pushdown model checking in time O((n2k|Σ| + n3k))1−εfor any ε > 0. Hence, our result implies that any better algorithm for pushdown model checking than the existing ones would lead to a breakthrough for the 3k-clique problem. Our lower bound applies even in the case when all the machines are deterministic, and even when the PDA is simply a deterministic one-counter machine. Furthermore, using the same hypothesis, we also show that pushdown model checking over constant-sized input alphabets cannot be solved in time faster than O(n3(k−1)−ε) for ε > 0.Finally, we also investigate the possibility of an O(N3k−ε) time algorithm for pushdown model checking where N is the total bit size of the given input. We formulate a new hypothesis, the 2NPDA(k) hypothesis, that helps explain the lack of O(N3k−ε) time algorithms for pushdown model checking. To corroborate this hypothesis, we show a web of linear-time reductions between the 2NPDA(k) hypothesis, pushdown model checking, and other problems in language theory and automata theory.