Strong Backdoors for Linear Temporal Logic

TL;DR

This paper introduces the concept of strong backdoors in linear temporal logic, analyzing their detection and evaluation complexity for different formula fragments and operator combinations.

Contribution

It defines strong backdoors for temporal logic and classifies the parameterized complexity of their detection and evaluation for various formula fragments.

Findings

Detection of backdoors is fixed-parameter tractable.

Evaluation complexity varies: paraNP-complete for Krom formulas.

Evaluation for Horn formulas is either fixed-parameter tractable or paraNP-complete.

Abstract

In the present paper we introduce the notion of strong backdoors into the field of temporal logic for the CNF-fragment of linear temporal logic introduced by Fisher. We study the parameterised complexity of the satisfiability problem parameterised by the size of the backdoor. We distinguish between backdoor detection and evaluation of backdoors into the fragments of horn and krom formulas. Here we classify the operator fragments of globally-operators for past or future, and the combination of both. Detection is shown to be in FPT whereas the complexity of evaluation behaves different. We show that for krom formulas the problem is paraNP-complete. For horn formulas the complexity is shown to be either fixed parameter tractable or paraNP-complete depending on the considered operator fragment.