On the Complexity of Computing Minimal Unsatisfiable LTL formulas
Logic in Computer Science
2012-03-26 v2
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.
Cite
@article{arxiv.1203.3706,
title = {On the Complexity of Computing Minimal Unsatisfiable LTL formulas},
author = {Francois Hantry and Lakhdar Saïs and Mohand-Saïd Hacid},
journal= {arXiv preprint arXiv:1203.3706},
year = {2012}
}
Comments
Minimal unsatisfiable cores For LTL causes inherent vacuity checking redundancy coverage