Details
| Original language | English |
|---|---|
| Article number | 1 |
| Journal | ACM Transactions on Computational Logic |
| Volume | 18 |
| Issue number | 1 |
| Publication status | Published - Jan 2017 |
Abstract
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.
Keywords
- Computation tree logic, Linear temporal logic, Parametrised complexity, Pathwidth, Post's lattice, Temporal depth, Temporal logic, Treewidth
ASJC Scopus subject areas
- Mathematics(all)
- Theoretical Computer Science
- Computer Science(all)
- Mathematics(all)
- Logic
- Mathematics(all)
- Computational Mathematics
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
In: ACM Transactions on Computational Logic, Vol. 18, No. 1, 1, 01.2017.
Research output: Contribution to journal › Article › Research › peer review
}
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 -