LTL Fragments are Hard for Standard Parameterisations

TL;DR

This paper analyzes the computational complexity of LTL satisfiability and model checking across various standard parameters, demonstrating that all operator fragments remain intractable within these parameterized frameworks.

Contribution

It provides a comprehensive classification showing that all LTL operator fragments are computationally hard under common parameterizations.

Findings

All operator fragments of LTL are intractable under the studied parameters.

Complexity results hold for parameters like temporal depth, propositional variables, and formula treewidth.

The results establish fundamental limits for efficient model checking and satisfiability algorithms.

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.