Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #3 to TR14-134 | 24th March 2015 16:15

Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies

RSS-Feed




Revision #3
Authors: Martin Lück, Arne Meier, Irina Schindler
Accepted on: 24th March 2015 16:15
Downloads: 524
Keywords: 


Abstract:

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.



Changes to previous version:

Corrected the W[1]-hardness reductions.


Revision #2 to TR14-134 | 23rd November 2014 16:40

Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies





Revision #2
Authors: Martin Lück, Arne Meier, Irina Schindler
Accepted on: 23rd November 2014 16:40
Downloads: 902
Keywords: 


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.



Changes to previous version:

More detailed proofs, explanations, and visualizations added.


Revision #1 to TR14-134 | 24th October 2014 11:16

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





Revision #1
Authors: Martin Lück, Arne Meier, Irina Schindler
Accepted on: 24th October 2014 11:16
Downloads: 589
Keywords: 


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 temporal depth and pathwidth. The classification shows a dichotomy between W[1]-hard and fixed-parameter tractable fragments. The only real operator fragments which is 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 cases.


Paper:

TR14-134 | 10th October 2014 10:09

Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies





TR14-134
Authors: Martin Lück, Arne Meier, Irina Schindler
Publication: 24th October 2014 11:00
Downloads: 707
Keywords: 


Abstract:

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.



ISSN 1433-8092 | Imprint