On the Complexity of Computing Minimal Unsatisfiable LTL formulas

Details On the Complexity of Computing Minimal Unsatisfiable LTL formulas On the Complexity of Computing Minimal Unsatisfiable LTL formulas

2012-03-16

arxiv.org/abs/1203.3706v2

Computer Science

Logic in Computer Science

Minimal unsatisfiable cores For LTL causes inherent vacuity checking redundancy coverage

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

On the Complexity of Computing Minimal Unsatisfiable LTL formulas does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On the Complexity of Computing Minimal Unsatisfiable LTL formulas, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the Complexity of Computing Minimal Unsatisfiable LTL formulas will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-351904