Parametrised complexity of satisfiability in temporal logic

Show simple item record

dc.identifier.uri http://dx.doi.org/10.15488/1212
dc.identifier.uri http://www.repo.uni-hannover.de/handle/123456789/1236
dc.contributor.author Lück, Martin
dc.contributor.author Meier, Arne
dc.contributor.author Schindler, Irena
dc.date.accessioned 2017-03-20T13:19:20Z
dc.date.available 2017-03-20T13:19:20Z
dc.date.issued 2017
dc.identifier.citation Luck, M.; Meier, A.; Schindler, I.: Parametrised complexity of satisfiability in temporal logic. In: ACM Transactions on Computational Logic 18 (2017), Nr. 1, 1. DOI: https://doi.org/10.1145/3001835
dc.description.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. © ACM 2017. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in ACM Transactions on Computational Logic 18 (2017), Nr. 1, 1. DOI: https://doi.org/10.1145/3001835. eng
dc.description.sponsorship DFG/ME 4279/1-1
dc.language.iso eng
dc.publisher Association for Computing Machinery
dc.relation.ispartofseries ACM Transactions on Computational Logic 18 (2017), Nr. 1
dc.rights Es gilt deutsches Urheberrecht. Das Dokument darf zum eigenen Gebrauch kostenfrei genutzt, aber nicht im Internet bereitgestellt oder an Außenstehende weitergegeben werden.
dc.subject Computation tree logic eng
dc.subject Linear temporal logic eng
dc.subject Parametrised complexity eng
dc.subject Pathwidth eng
dc.subject Post's lattice eng
dc.subject Temporal depth eng
dc.subject Temporal logic eng
dc.subject Treewidth eng
dc.subject Boolean functions eng
dc.subject Formal logic eng
dc.subject Temporal logic eng
dc.subject Computation tree logic eng
dc.subject Linear temporal logic eng
dc.subject Parametrised complexity eng
dc.subject Pathwidth eng
dc.subject Post's lattice eng
dc.subject Temporal depth eng
dc.subject Tree-width eng
dc.subject Computer circuits eng
dc.subject.ddc 510 | Mathematik ger
dc.title Parametrised complexity of satisfiability in temporal logic
dc.type Text
dc.type article
dc.relation.issn 1529-3785
dc.relation.doi https://doi.org/10.1145/3001835
dc.bibliographicCitation.issue 1
dc.bibliographicCitation.volume 18
dc.bibliographicCitation.firstPage 1
dc.description.version acceptedVersion
tib.accessRights frei zug�nglich


Files in this item

This item appears in the following Collection(s):

Show simple item record

 

Search the repository


Browse

My Account

Usage Statistics