Backdoors for Linear Temporal Logic

Abu-Khzam, F.N.: A kernelization algorithm for d-hitting set. J. Comput. Syst. Sci. 76(7), 524–531 (2010)

Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: The complexity of clausal fragments of LTL. In: Proc. 19th LPAR, LNCS, vol. 8312 (2013)

Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The complexity of generalized satisfiability for linear temporal logic. LMCS 5(1), 1–21 (2009)

Chen, C.C., Lin, I.P.: The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic. IPL 45(3), 131–136 (1993)

Chen, J., Chor, B., Fellows, M., Huang, X., Juedes, D., Kanji, I., Xia, G.: Tight lower bounds for certain parameterized NP-hard problems. Inf. Comput. 201(2), 216–231 (2005)

Chen, J., Kanj, I.A., Xia, G.: Improved upper bounds for vertex cover. Theor. Comput. Sci. 411(40–42), 3736–3756 (2010)

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. Logic of Programs. LNCS, vol. 131, pp. 52–71. Springer, Berlin (1981)

Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84–103 (2002)

Dilkina, B.N., Gomes, C.P., Sabharwal, A.: Tradeoffs in the complexity of backdoor detection. In: Proc. 13th CP, Lecture Notes in Computer Science, vol. 4741, pp. 256–270. Springer (2007)

Dilkina, B.N., Gomes, C.P., Sabharwal, A.: Backdoors in the context of learning. In: Proc. 12th SAT, Lecture Notes in Computer Science, vol. 5584, pp. 73–79. Springer, Berlin (2009)

Dixon, C., Fisher, M., Konev, B.: Tractable temporal reasoning. In: Proc. of IJCAI, pp. 318–323 (2007)

Downey, R.G., Fellows, M.R.: Fundamentals of Parameterized Complexity. Springer, London (2013)

Dvorák, W., Ordyniak, S., Szeider, S.: Augmenting tractable fragments of abstract argumentation. Artif. Intell. 186, 157–173 (2012)

Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30(1), 1–24 (1985)

Fisher, M.: A normal form for temporal logic and its application in theorem-proving and execution. J. Logic Comput. 7, 429–456 (1997)

Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Trans. Comput. Logic 2(1), 12–56 (2001)

Gabbay, D.M., Hodkinsion, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press, Inc., New York (1994)

Gaspers, S., Szeider, S.: Backdoors to satisfaction. In: The Multivariate Algorithmic Revolution and Beyond - Essays Dedicated to Michael R. Fellows on the Occasion of His 60th Birthday, LNCS, vol. 7370, pp. 287–317. Springer, Berlin (2012)

Gaspers, S., Szeider, S.: Strong backdoors to bounded treewidth SAT. In: Proc. 54th FOCS, pp. 489–498. IEEE Computer Society (2013)

Kottler, S., Kaufmann, M., Sinz, C.: A new bound for an NP-hard subclass of 3-SAT using backdoors. In: Proc. 11th SAT, Lecture Notes in Computer Science, pp. 161–167. Springer, Berlin (2008)

Kripke, S.: Semantical considerations on modal logic. Acta philosophica Fennica 16, 84–94 (1963)

Kronegger, M., Ordyniak, S., Pfandler, A.: Backdoors to planning. In: Proc. 28th AAAI, pp. 2300–2307. AAAI Press (2014)

Kronegger, M., Ordyniak, S., Pfandler, A.: Variable-deletion backdoors to planning. In: Proc. 29th AAAI, pp. 2300–2307. AAAI Press (2014)

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001). https://doi.org/10.1023/A:1011254632723

LeBras, R., Bernstein, R., Gomes, C.P., Selman, B., van Dover, R.B.: Crowdsourcing backdoor identification for combinatorial optimization. In: Proc. 23rd IJCAI. AAAI (2013)

Lück, M., Meier, A.: LTL Fragments are hard for standard parameterizations. In: Proc. of TIME, pp. 59–68 (2015). https://doi.org/10.1109/TIME.2015.9

Markey, N.: Past is for free: on the complexity of verifying linear temporal properties with past. Acta Informatica 40(6–7), 431–458 (2004)

Meier, A., Ordyniak, S., Sridharan, R., Schindler, I.: Backdoors for linear temporal logic. In: J. Guo, D. Hermelin (eds.) 11th International Symposium on Parameterized and Exact Computation (IPEC 2016), vol. 63, pp. 23:1–23:17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2017)

Ono, H., Nakamura, A.: On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica 39, 325–333 (1980)

Ordyniak, S., Paulusma, D., Szeider, S.: Satisfiability of acyclic and almost acyclic CNF formulas. Theor. Comput. Sci. 481, 85–99 (2013)

Pfandler, A., Rümmele, S., Szeider, S.: Backdoors to abduction. In: Proc. 23rd IJCAI (2013)

Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS, pp. 46–57. IEEE Comp. Soc. Press (1977)

Ruan, Y., Kautz, H.A., Horvitz, E.: The backdoor key: A path to understanding problem hardness. In: Proc. 19th IAAI, pp. 124–130. AAAI Press (2004)

Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77–97 (2009)

Samer, M., Szeider, S.: Fixed-parameter tractability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap 13, pp. 425–454. IOS Press, Amsterdam (2009)

Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. In: Proc. of STOC, pp. 159–168. ACM (1982)

Szeider, S.: On fixed-parameter tractable parameterizations of SAT. In: Proc. of SAT, pp. 188–202 (2003)

Williams, R., Gomes, C., Selman, B.: Backdoors to typical case complexity. In: Proc. 18th IJCAI, pp. 1173–1178. Morgan Kaufmann (2003)