Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies.
Martin Lück, Arne Meier, Irina Schindler · Electronic colloquium on computational complexity · 2014
We present a complete classification of the parameterized complexity of all operator fragments of the satisfiability problem in computation tree logic CTL. The investigated parameterization is temporal depth and pathwidth. Our results show a dichotomy between W[1]-hard and fixed-parameter tractable fragments. The two real operator fragments which are in FPT are the fragments containing solely AF, or AX. Also we prove a generalization of Courcelle’s theorem to infinite vocabularies which will be used to proof the FPT-membership cases.