Model Checking CTL is Almost Always Inherently Sequential

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 most applications, approaching CTL model checking by parallelism will not result in the desired speed up. We also completely determine the complexity of the model checking problem for all fragments of the extensions ECTL, CTL+, and ECTL+.

Authors

• Olaf Beyersdorff
• Arne Meier
• Michael Thomas 0001
• Heribert Vollmer
• Martin Mundhenk
• Thomas Schneider 0002

Keywords

• Logic
• Computer science
• Parallel processing
• Gold
• Computational complexity
• Polynomials
• Visualization
• Model Checking
• Computation Tree Logic
• Temporal Operators
• Lower Bound
• Upper Bound
• Hardness
• Set Of Operations
• Output Gate
• Temporal Logic
• Linear Logic
• complexity