Sciweavers

Share
TIME
2009
IEEE

Model Checking CTL is Almost Always Inherently Sequential

9 years 6 months ago
Model Checking CTL is Almost Always Inherently Sequential
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+ .
Olaf Beyersdorff, Arne Meier, Michael Thomas, Heri
Added 21 May 2010
Updated 21 May 2010
Type Conference
Year 2009
Where TIME
Authors Olaf Beyersdorff, Arne Meier, Michael Thomas, Heribert Vollmer, Martin Mundhenk, Thomas Schneider
Comments (0)
books