Beyersdorff, Olaf and Meier, Arne and Mundhenk, Martin and Schneider, Thomas and Thomas, Michaelet al. - Model Checking CTL is Almost Always Inherently Sequential

lmcs:1007 - Logical Methods in Computer Science, May 17, 2011, Volume 7, Issue 2
Model Checking CTL is Almost Always Inherently Sequential

Authors: Beyersdorff, Olaf and Meier, Arne and Mundhenk, Martin and Schneider, Thomas and Thomas, Michael and Vollmer, Heribert

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


Source : oai:arXiv.org:1103.4990
DOI : 10.2168/LMCS-7(2:12)2011
Volume: Volume 7, Issue 2
Published on: May 17, 2011
Submitted on: January 14, 2010
Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,cs.CC


Share

Consultation statistics

This page has been seen 85 times.
This article's PDF has been downloaded 108 times.