TR12-069 Authors: Lakhdar Saïs, Mohand-Saïd Hacid, francois hantry

Publication: 26th May 2012 12:22

Downloads: 2637

Keywords:

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.