Model Checking CTL is Almost Always Inherently Sequential

TL;DR

This paper investigates the complexity of model checking for various fragments of CTL, revealing that most are inherently sequential (P-complete), limiting the benefits of parallelization in practical scenarios.

Contribution

It systematically classifies the complexity of model checking for all CTL fragments and extensions, showing most are P-complete and thus inherently sequential.

Findings

Most CTL fragments are P-complete, indicating inherent sequentiality.

Parallelization offers limited speedup for CTL model checking.

Complete complexity classification for all fragments of ECTL, CTL+, and ECTL+.

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+.