Temporal Representation and Reasoning, International Syposium on (2009)
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
Thomas Schneider, Michael Thomas, Heribert Vollmer, Arne Meier, Martin Mundhenk, Olaf Beyersdorff, "Model Checking CTL is Almost Always Inherently Sequential", Temporal Representation and Reasoning, International Syposium on, vol. 00, no. , pp. 21-28, 2009, doi:10.1109/TIME.2009.12