ECCC-Report TR14-134https://eccc.weizmann.ac.il/report/2014/134Comments and Revisions published for TR14-134en-usTue, 24 Mar 2015 16:15:26 +0200
Revision 3
| Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies |
Martin Lück,
Arne Meier,
Irina Schindler
https://eccc.weizmann.ac.il/report/2014/134#revision3We 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.Tue, 24 Mar 2015 16:15:26 +0200https://eccc.weizmann.ac.il/report/2014/134#revision3
Revision 2
| Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies |
Martin Lück,
Arne Meier,
Irina Schindler
https://eccc.weizmann.ac.il/report/2014/134#revision2We 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.Sun, 23 Nov 2014 16:40:35 +0200https://eccc.weizmann.ac.il/report/2014/134#revision2
Revision 1
| Parameterized Complexity of CTL: A Generalization of Courcelle's Theorem |
Martin Lück,
Arne Meier,
Irina Schindler
https://eccc.weizmann.ac.il/report/2014/134#revision1We 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.Fri, 24 Oct 2014 11:16:52 +0300https://eccc.weizmann.ac.il/report/2014/134#revision1
Paper TR14-134
| Parameterized Complexity of CTL: Courcelle's Theorem For Infinite Vocabularies |
Martin Lück,
Arne Meier,
Irina Schindler
https://eccc.weizmann.ac.il/report/2014/134We 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.Fri, 24 Oct 2014 11:00:08 +0300https://eccc.weizmann.ac.il/report/2014/134