Fine-Grained Complexity Lower Bounds for Problems in Computer Aided Verification

This article presents two fine-grained complexity lower bounds with relevance to algorithmic problems in computer aided verification. We have chosen these lower bounds as the proofs are relatively simple, but the techniques can be extended to give lower bounds for many more algorithmic problems. The goal is to present the bounds with minimal notation, making the results accessible to a broad community and stimulating further research in the area. Specifically, we first describe a lower bound on the symbolic complexity of computing strongly connected components, which can be extended to show lower bounds for fundamental model-checking questions in graphs, published in [CDHL16b]. Second we present a conditional lower bound for disjunctive safety problems on graphs from [CDHL18] in the RAM model of computation. This bound can be modified to give conditional lower bounds for disjunctive objectives for reachability, Büchi, coBüchi and Rabin objectives in MDPs. We also present various open questions.