Pushdown Model Checking Above the Cubic Bottleneck
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} |\Sigma| + n^{3k})$, where $n$ is the maximum number of states of the PDA and the NFAs, $\Sigma$ 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 $\epsilon > 0$, there is no algorithm (resp. combinatorial algorithm) that solves this problem in time $O((n^{(\omega-1)k} |\Sigma| + n^{\omega k})^{1-\epsilon})$ (resp. $O((n^{2k} |\Sigma| + n^{3k})^{1-\epsilon})$) where $\omega$ 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)-\epsilon})$ for any $\epsilon > 0$. Finally, we investigate the possibility of an $O(N^{3k-\epsilon})$ 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-\epsilon})$ 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.