Details
| Originalsprache | Englisch |
|---|---|
| Titel des Sammelwerks | 11th International Symposium on Parameterized and Exact Computation, IPEC 2016, August 24-26, 2016, Aarhus, Denmark |
| Herausgeber/-innen | Jiong Guo, Danny Hermelin |
| Seiten | 23:1-23:17 |
| Band | 63 |
| ISBN (elektronisch) | 9783959770231 |
| Publikationsstatus | Veröffentlicht - 2016 |
Publikationsreihe
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Band | 63 |
| ISSN (Print) | 1868-8969 |
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 (FPT) 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.)
- Software
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
11th International Symposium on Parameterized and Exact Computation, IPEC 2016, August 24-26, 2016, Aarhus, Denmark. Hrsg. / Jiong Guo; Danny Hermelin. Band 63 2016. S. 23:1-23:17 23 (Leibniz International Proceedings in Informatics, LIPIcs; Band 63).
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
T1 - Backdoors for Linear Temporal Logic
AU - Meier, Arne
AU - Ordyniak, Sebastian
AU - Sridharan, Ramanujan
AU - Schindler, Irena
PY - 2016
Y1 - 2016
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 (FPT) 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 (FPT) 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=85014611663&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.IPEC.2016.23
DO - 10.4230/LIPIcs.IPEC.2016.23
M3 - Conference contribution
VL - 63
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 23:1-23:17
BT - 11th International Symposium on Parameterized and Exact Computation, IPEC 2016, August 24-26, 2016, Aarhus, Denmark
A2 - Guo, Jiong
A2 - Hermelin, Danny
ER -