THE COMPLEXITY OF SATISFIABILITY FOR FRAGMENTS OF CTL AND CTL

The satisfiability problems for CTL and CTL are known to be EXPTIME-complete resp. 2EXPTime-complete (Fischer and Ladner (1979), Vardi and Stockmeyer (1985)). For fragments that use less temporal or propositional operators, the complexity may decrease. This paper undertakes a systematic study of satisfiability for CTL and CTL*-formulae over restricted sets of propositional and temporal operators. We show that restricting the temporal operators yields satisfiability problems complete for 2 EXPTIME, EXPTIME, PSPACE,and NP. Restricting the propositional operators either does not change the complexity (as determined by the temporal operators), or yields very low complexity like NC1, TC0, or NLOGTIME.