Details
| Originalsprache | Englisch |
|---|---|
| Seiten (von - bis) | 476-496 |
| Seitenumfang | 21 |
| Fachzeitschrift | ALGORITHMICA |
| Jahrgang | 81 |
| Ausgabenummer | 2 |
| Frühes Online-Datum | 18 Sept. 2018 |
| Publikationsstatus | Veröffentlicht - 15 Feb. 2019 |
Abstract
In the present paper, we introduce the backdoor set approach into the field of temporal logic for the global fragment of linear temporal logic. We study the parameterized complexity of the satisfiability problem parameterized 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/future/always, and the combination of them. Detection is shown to be fixed-parameter tractable whereas the complexity of evaluation behaves differently. 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.
ASJC Scopus Sachgebiete
- Informatik (insg.)
- Allgemeine Computerwissenschaft
- Informatik (insg.)
- Angewandte Informatik
- Mathematik (insg.)
- Angewandte Mathematik
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
in: ALGORITHMICA, Jahrgang 81, Nr. 2, 15.02.2019, S. 476-496.
Publikation: Beitrag in Fachzeitschrift › Artikel › Forschung › Peer-Review
}
TY - JOUR
T1 - Backdoors for Linear Temporal Logic
AU - Meier, Arne
AU - Ordyniak, Sebastian
AU - Ramanujan, M. S.
AU - Schindler, Irena
N1 - Funding Information: The first and last author gratefully acknowledge the support by the German Research Foundation DFG for their grant ME 4279/1-1. The second and third author acknowledge support by the Austrian Science Fund (FWF, project P26696). We thank the anonymous referees for their valuable comments.
PY - 2019/2/15
Y1 - 2019/2/15
N2 - In the present paper, we introduce the backdoor set approach into the field of temporal logic for the global fragment of linear temporal logic. We study the parameterized complexity of the satisfiability problem parameterized 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/future/always, and the combination of them. Detection is shown to be fixed-parameter tractable whereas the complexity of evaluation behaves differently. 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.
AB - In the present paper, we introduce the backdoor set approach into the field of temporal logic for the global fragment of linear temporal logic. We study the parameterized complexity of the satisfiability problem parameterized 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/future/always, and the combination of them. Detection is shown to be fixed-parameter tractable whereas the complexity of evaluation behaves differently. 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.
KW - Backdoor sets
KW - Linear temporal logic
KW - Parameterized complexity
UR - http://www.scopus.com/inward/record.url?scp=85053691943&partnerID=8YFLogxK
U2 - 10.1007/s00453-018-0515-5
DO - 10.1007/s00453-018-0515-5
M3 - Article
AN - SCOPUS:85053691943
VL - 81
SP - 476
EP - 496
JO - ALGORITHMICA
JF - ALGORITHMICA
SN - 0178-4617
IS - 2
ER -