July 23, 2009 to July 25, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2009.12
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+.
Model checking, temporal logic, complexity
Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer, Martin Mundhenk, Thomas Schneider, "Model Checking CTL is Almost Always Inherently Sequential", TIME, 2009, Temporal Representation and Reasoning, International Syposium on, Temporal Representation and Reasoning, International Syposium on 2009, pp. 21-28, doi:10.1109/TIME.2009.12