Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem

TL;DR

This paper classifies the parameterized complexity of all operator fragments of CTL satisfiability based on temporal depth and pathwidth, revealing a dichotomy between W[1]-hard and fixed-parameter tractable cases.

Contribution

It provides a near-complete classification of CTL operator fragments' complexity and generalizes Courcelle's theorem to infinite signatures for FPT proofs.

Findings

Only the AX fragment is fixed-parameter tractable.

Most fragments are W[1]-hard.

A generalized Courcelle's theorem is established.

Abstract

We present an almost complete classification of the parameterized complexity of all operator fragments of the satisfiability problem in computation tree logic CTL. The investigated parameterization is the sum of temporal depth and structural pathwidth. The classification shows a dichotomy between W[1]-hard and fixed-parameter tractable fragments. The only real operator fragment which is confirmed to be in FPT is the fragment containing solely AX. Also we prove a generalization of Courcelle's theorem to infinite signatures which will be used to proof the FPT-membership case.