TY - JOUR

T1 - Parametrised complexity of satisfiability in temporal logic

AU - Luck, Martin

AU - Meier, Arne

AU - Schindler, Irena

N1 - Funding information: This work was supported by DFG grant ME 4279/1-1. Part of this work has been published in a preliminary form in: M. Luck, A. Meier, and I. Schindler, Parameterized Complexity of CTL, Proc. LATA 2015, pp. 549-560, vol. 8977 LNCS. Luck et al. [2015].

PY - 2017/1

Y1 - 2017/1

N2 - We apply the concept of formula treewidth and pathwidth to computation tree logic, linear temporal logic, and the full branching time logic. Several representations of formulas as graphlike structures are discussed, and corresponding notions of treewidth and pathwidth are introduced. As an application for such structures, we present a classification in terms of parametrised complexity of the satisfiability problem, where we make use of Courcelle's famous theorem for recognition of certain classes of structures. Our classification shows a dichotomy between W[1]-hard and fixed-parameter tractable operator fragments almost independently of the chosen graph representation. The only fragments that are proven to be fixed-parameter tractable (FPT) are those that are restricted to the X operator. By investigating Boolean operator fragments in the sense of Post's lattice, we achieve the same complexity as in the unrestricted case if the set of available Boolean functions can express the function "negation of the implication." Conversely, we show containment in FPT for almost all other clones.

AB - We apply the concept of formula treewidth and pathwidth to computation tree logic, linear temporal logic, and the full branching time logic. Several representations of formulas as graphlike structures are discussed, and corresponding notions of treewidth and pathwidth are introduced. As an application for such structures, we present a classification in terms of parametrised complexity of the satisfiability problem, where we make use of Courcelle's famous theorem for recognition of certain classes of structures. Our classification shows a dichotomy between W[1]-hard and fixed-parameter tractable operator fragments almost independently of the chosen graph representation. The only fragments that are proven to be fixed-parameter tractable (FPT) are those that are restricted to the X operator. By investigating Boolean operator fragments in the sense of Post's lattice, we achieve the same complexity as in the unrestricted case if the set of available Boolean functions can express the function "negation of the implication." Conversely, we show containment in FPT for almost all other clones.

KW - Computation tree logic

KW - Linear temporal logic

KW - Parametrised complexity

KW - Pathwidth

KW - Post's lattice

KW - Temporal depth

KW - Temporal logic

KW - Treewidth

UR - http://www.scopus.com/inward/record.url?scp=85010806818&partnerID=8YFLogxK

U2 - 10.1145/3001835

DO - 10.1145/3001835

M3 - Article

AN - SCOPUS:85010806818

VL - 18

JO - ACM Transactions on Computational Logic

JF - ACM Transactions on Computational Logic

SN - 1529-3785

IS - 1

M1 - 1

ER -