LTL Fragments are Hard for Standard Parameterisations

2015/04/23 by Martin Lück, Lück, Martin, Arne Meier +1
Computer Science · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1504.06187

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.

Citations

• The complexity of propositional linear temporal logics

Related

• The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments
• Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem
• Complexity of Safety and coSafety Fragments of Linear Temporal Logic
• The Complexity of Fragments of Second-Order HyperLTL
• Fairness and promptness in Muller formulas