Olaf Beyersdorff ; Arne Meier ; Martin Mundhenk ; Thomas Schneider ; Michael Thomas et al. - Model Checking CTL is Almost Always Inherently Sequential

lmcs:1007 - Logical Methods in Computer Science, May 17, 2011, Volume 7, Issue 2 - https://doi.org/10.2168/LMCS-7(2:12)2011
Model Checking CTL is Almost Always Inherently SequentialArticle

Authors: Olaf Beyersdorff ORCID; Arne Meier ORCID; Martin Mundhenk ; Thomas Schneider ; Michael Thomas ; Heribert Vollmer ORCID

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


    Volume: Volume 7, Issue 2
    Published on: May 17, 2011
    Imported on: January 14, 2010
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,cs.CC

    Publications

    Has review
    • 1 zbMATH Open

    5 Documents citing this article

    Consultation statistics

    This page has been seen 1579 times.
    This article's PDF has been downloaded 588 times.