Pushdown Model Checking above the Cubic Bottleneck
A. R. Balasubramanian, Dmitry V. Chistikov, Rupak Majumdar · 2025
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.