Meier, A.; Ordyniak, S.; Sridharan, R.; Schindler, I.: Backdoors for linear temporal logic. In: Leibniz International Proceedings in Informatics, LIPIcs 63 (2017), 23. DOI: https://doi.org/10.4230/LIPIcs.IPEC.2016.23
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. | |
License of this version: | CC BY 3.0 Unported |
Document Type: | Article |
Publishing status: | publishedVersion |
Issue Date: | 2017 |
Appears in Collections: | Fakultät für Elektrotechnik und Informatik |
pos. | country | downloads | ||
---|---|---|---|---|
total | perc. | |||
1 | ![]() |
Germany | 114 | 50.00% |
2 | ![]() |
United States | 42 | 18.42% |
3 | ![]() |
Greece | 13 | 5.70% |
4 | ![]() |
Sweden | 12 | 5.26% |
5 | ![]() |
China | 6 | 2.63% |
6 | ![]() |
Russian Federation | 5 | 2.19% |
7 | ![]() |
Japan | 4 | 1.75% |
8 | ![]() |
Austria | 4 | 1.75% |
9 | ![]() |
Taiwan | 3 | 1.32% |
10 | ![]() |
Canada | 3 | 1.32% |
other countries | 22 | 9.65% |
Hinweis
Zur Erhebung der Downloadstatistiken kommen entsprechend dem „COUNTER Code of Practice for e-Resources“ international anerkannte Regeln und Normen zur Anwendung. COUNTER ist eine internationale Non-Profit-Organisation, in der Bibliotheksverbände, Datenbankanbieter und Verlage gemeinsam an Standards zur Erhebung, Speicherung und Verarbeitung von Nutzungsdaten elektronischer Ressourcen arbeiten, welche so Objektivität und Vergleichbarkeit gewährleisten sollen. Es werden hierbei ausschließlich Zugriffe auf die entsprechenden Volltexte ausgewertet, keine Aufrufe der Website an sich.