On the Complexity of Computing Minimal Unsatisfiable LTL formulas

TL;DR

This paper proves that finding minimal unsatisfiable formulas in LTL and related problems are FPSPACE-complete, highlighting the high computational complexity involved in these logical decision problems.

Contribution

It establishes the FPSPACE-completeness of minimal unsatisfiable LTL formulas and related search problems, extending known hardness results and resolving an open question.

Findings

Minimal Unsatisfiable LTL formulas are FPSPACE-complete.

The decision problem for minimal false QCNF is FPSPACE-hard.

Inherent Vacuity Checking is FPSPACE-hard.

Abstract

We show that (1) the Minimal False QCNF search-problem (MF-search) and the Minimal Unsatisfiable LTL formula search problem (MU-search) are FPSPACE complete because of the very expressive power of QBF/LTL, (2) we extend the PSPACE-hardness of the MF decision problem to the MU decision problem. As a consequence, we deduce a positive answer to the open question of PSPACE hardness of the inherent Vacuity Checking problem. We even show that the Inherent Non Vacuous formula search problem is also FPSPACE-complete.