Bounded variable logic, parameterized logarithmic space, and Savitch's theorem

• Yijia Chen

• Shanghai Jiao Tong University

It is well known that model-checking first-order logic (MC(FO)) is complete for PSPACE. But if we restrict the number of variables appearing in the formulas, then the problem becomes solvable in polynomial time by an algorithm due to M. Vardi. However, Vardi's algorithm requires polynomial space. We show that the question whether this can be done in so-called parameterized logarithmic space is ultimately linked to a question concerning Savitch's theorem. In 1969, W. Savitch proved that the directed reachability problem can be solved in 𝑂(log₂ n) space. It has been open even since whether this can be improved to 𝑂(log₂ n). We show that it is indeed the case if model-checking first-order logic with only two variables is in parameterized logarithmic space. Our proof is via a parameterized complexity class PATH recently introduced by M. Elberfeld, C. Stockhusen, and T. Tantau.

This is joint work with Moritz Mueller.