Document Open Access Logo

Backdoors for Linear Temporal Logic

Authors Arne Meier, Sebastian Ordyniak, Ramanujan Sridharan, Irena Schindler

PDF
Thumbnail PDF

File

LIPIcs.IPEC.2016.23.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Author Details

Arne Meier
Sebastian Ordyniak
Ramanujan Sridharan
Irena Schindler

Cite As Get BibTex

Arne Meier, Sebastian Ordyniak, Ramanujan Sridharan, and Irena Schindler. Backdoors for Linear Temporal Logic. In 11th International Symposium on Parameterized and Exact Computation (IPEC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 63, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) 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.

Subject Classification

Keywords
  • Linear Temporal Logic
  • Parameterized Complexity
  • Backdoor Sets

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. F. N. Abu-Khzam. A kernelization algorithm for d-hitting set. Journal of Computer and System Sciences, 76(7):524-531, 2010. Google Scholar
  2. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. The complexity of clausal fragments of LTL. In Proc. 19th LPAR, volume 8312 of LNCS, 2013. Google Scholar
  3. M. Bauland, T. Schneider, H. Schnoor, I. Schnoor, and H. Vollmer. The complexity of generalized satisfiability for linear temporal logic. LMCS, 5(1), 2009. Google Scholar
  4. C.-C. Chen and I.-P. Lin. The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic. IPL, 45(3):131-136, 1993. Google Scholar
  5. J. Chen, B. Chor, M. Fellows, X. Huang, D. Juedes, I. Kanji, and G. Xia. Tight Lower Bounds for Certain Parameterized NP-Hard Problems. Information and Computation, 201(2):216-231, 2005. Google Scholar
  6. J. Chen, I. A. Kanj, and G. Xia. Improved upper bounds for vertex cover. Theoretical Computer Science, 411(40-42):3736-3756, 2010. Google Scholar
  7. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronisation skeletons using branching time temporal logic. In Logic of Programs, volume 131 of LNCS, pages 52-71. Springer Verlag, 1981. Google Scholar
  8. S. Demri and P. Schnoebelen. The complexity of propositional linear temporal logics in simple cases. Information and Computation, 174(1):84-103, 2002. Google Scholar
  9. B. N. Dilkina, C. P. Gomes, and A. Sabharwal. Tradeoffs in the complexity of backdoor detection. In Proc. 13th CP, volume 4741 of Lecture Notes in Computer Science, pages 256-270. Springer Verlag, 2007. Google Scholar
  10. B. N. Dilkina, C. P. Gomes, and A. Sabharwal. Backdoors in the context of learning. In Proc. 12th SAT, volume 5584 of Lecture Notes in Computer Science, pages 73-79. Springer Verlag, 2009. Google Scholar
  11. C. Dixon, M. Fisher, and B. Konev. Tractable temporal reasoning. In Proc. of IJCAI, pages 318-323, 2007. Google Scholar
  12. R. G. Downey and M. R. Fellows. Fundamentals of Parameterized Complexity. Springer, 2013. Google Scholar
  13. W. Dvorák, S. Ordyniak, and S. Szeider. Augmenting tractable fragments of abstract argumentation. Artificial Intelligence, 186:157-173, 2012. Google Scholar
  14. E. Allen Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30(1):1-24, 1985. Google Scholar
  15. M. Fisher, C. Dixon, and M. Peim. Clausal temporal resolution. ACM Transactions on Computational Logic, 2(1):12-56, 2001. Google Scholar
  16. Michael Fisher. A normal form for temporal logic and its application in theorem-proving and execution. Journal of Logic and Computation, 7:429-456, 1997. Google Scholar
  17. D. M. Gabbay, I. Hodkinsion, and M. Reynolds. Temporal logic: mathematical foundations and computational aspects, volume 1. Oxford University Press, Inc. New York, USA, 1994. Google Scholar
  18. S. Gaspers and S. Szeider. Backdoors to satisfaction. In The Multivariate Algorithmic Revolution and Beyond - Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday, volume 7370 of LNCS, pages 287-317. Springer, 2012. Google Scholar
  19. S. Gaspers and S. Szeider. Strong backdoors to bounded treewidth SAT. In Proc. 54th FOCS, pages 489-498. IEEE Computer Society, 2013. Google Scholar
  20. S. Kottler, M. Kaufmann, and C. Sinz. A new bound for an NP-hard subclass of 3-SAT using backdoors. In Proc. 11th SAT, Lecture Notes in Computer Science, pages 161-167. Springer Verlag, 2008. Google Scholar
  21. S. Kripke. Semantical considerations on modal logic. In Acta philosophica Fennica, volume 16, pages 84-94, 1963. Google Scholar
  22. M. Kronegger, S. Ordyniak, and A. Pfandler. Backdoors to planning. In Proc. 28th AAAI, pages 2300-2307. AAAI Press, 2014. Google Scholar
  23. M. Kronegger, S. Ordyniak, and A. Pfandler. Variable-deletion backdoors to planning. In Proc. 29th AAAI, pages 2300-2307. AAAI Press, 2014. Google Scholar
  24. R. LeBras, R. Bernstein, C. P. Gomes, B. Selman, and R. Bruce van Dover. Crowdsourcing backdoor identification for combinatorial optimization. In Proc. 23rd IJCAI. AAAI, 2013. Google Scholar
  25. M. Lück and A. Meier. LTL Fragments are Hard for Standard Parameterisations. In Proc. of TIME, pages 59-68, 2015. URL: http://dx.doi.org/10.1109/TIME.2015.9.
  26. N. Markey. Past is for free: On the complexity of verifying linear temporal properties with past. Acta Informatica, 40(6-7):431-458, 2004. Google Scholar
  27. H. Ono and A. Nakamura. On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica, 39(325-333), 1980. Google Scholar
  28. S. Ordyniak, D. Paulusma, and S. Szeider. Satisfiability of acyclic and almost acyclic CNF formulas. Theoretical Computer Science, 481:85-99, 2013. Google Scholar
  29. A. Pfandler, S. Rümmele, and S. Szeider. Backdoors to abduction. In Proc. 23rd IJCAI, 2013. Google Scholar
  30. A. Pnueli. The temporal logic of programs. In Proc. of FOCS, pages 46-57. IEEE Comp. Soc. Press, 1977. Google Scholar
  31. Y. Ruan, H. A. Kautz, and E. Horvitz. The backdoor key: A path to understanding problem hardness. In Proc. 19th IAAI, pages 124-130. AAAI Press, 2004. Google Scholar
  32. M. Samer and S. Szeider. Backdoor sets of quantified Boolean formulas. Journal of Automated Reasoning, 42(1):77-97, 2009. Google Scholar
  33. M. Samer and S. Szeider. Fixed-parameter tractability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, chapter 13, pages 425-454. IOS Press, 2009. Google Scholar
  34. A. Sistla and E. Clarke. The complexity of propositional linear temporal logics. In Proc. of STOC, pages 159-168. ACM, 1982. Google Scholar
  35. S. Szeider. On fixed-parameter tractable parameterizations of SAT. In Proc. of SAT, pages 188-202, 2003. URL: http://dx.doi.org/10.1007/978-3-540-24605-3_15.
  36. R. Williams, C. Gomes, and B. Selman. Backdoors to typical case complexity. In Proc. 18th IJCAI, pages 1173-1178. Morgan Kaufmann, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact