Title :
LTL Fragments are Hard for Standard Parameterisations
Author_Institution :
Inst. fur Theor. Inf., Leibniz Univ. Hannover, Hannover, Germany
Abstract :
We classify the complexity of the LTL satisfiability and model checking problems for several standard parameterisations. The investigated parameters are temporal depth, number of propositional variables and formula treewidth, resp., pathwidth. We show that all operator fragments of LTL under the investigated parameterisations are intractable in the sense of parameterised complexity.
Keywords :
"Complexity theory","Model checking","Runtime","Turing machines","Standards","Context","Semantics"
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2015 22nd International Symposium on
DOI :
10.1109/TIME.2015.9