DROPS

Document

DOI: 10.4230/LIPIcs.IPEC.2016.23

Backdoors for Linear Temporal Logic

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

Published in: LIPIcs, Volume 63, 11th International Symposium on Parameterized and Exact Computation (IPEC 2016)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{meier_et_al:LIPIcs.IPEC.2016.23,
  author =	{Meier, Arne and Ordyniak, Sebastian and Sridharan, Ramanujan and Schindler, Irena},
  title =	{{Backdoors for Linear Temporal Logic}},
  booktitle =	{11th International Symposium on Parameterized and Exact Computation (IPEC 2016)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-023-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{63},
  editor =	{Guo, Jiong and Hermelin, Danny},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2016.23},
  URN =		{urn:nbn:de:0030-drops-69462},
  doi =		{10.4230/LIPIcs.IPEC.2016.23},
  annote =	{Keywords: Linear Temporal Logic, Parameterized Complexity, Backdoor Sets}
}

Search Results

Documents authored by Schindler, Irena

Backdoors for Linear Temporal Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message