Model Checking CTL is Almost Always Inherently Sequential

Authors:
  • OBOlaf Beyersdorff
    Olaf Beyersdorff
  • AMArne Meier
    Arne Meier
  • MMMartin Mundhenk
    Martin Mundhenk
  • TSThomas Schneider
    Thomas Schneider
  • MTMichael Thomas
    Michael Thomas
  • HVHeribert Vollmer
    Heribert Vollmer
Preprint
Publisher website
Google Scholar
Abstract
The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) and Markey (2004). For all these fragments, except for the trivial case without any temporal operator, we systematically prove model checking to be either inherently sequential (P-complete) or very efficiently parallelizable (LOGCFL-complete). For most fragments, however, model checking for CTL is already P-complete. Hence our results indicate that, in cases where the combined complexity is of relevance, approaching CTL model checking by parallelism cannot be expected to result in any significant speedup. We also completely determine the complexity of the model checking problem for all fragments of the extensions ECTL, CTL+, and ECTL+.

This publication has 14 references indexed in Scilit: