Model checking CTL is almost always inherently sequential

Show simple item record

dc.identifier.uri Beyersdorff, Olaf Meier, Arne Mundhenk, Martin Schneider, Thomas Thomas, Michael Vollmer, Heribert 2016-11-02T13:35:59Z 2016-11-02T13:35:59Z 2011
dc.identifier.citation Beyersdorff, Olaf; Meier, Arne; Mundhenk, M.; Schneider, T.; Thomas, Michael et al.: Model checking CTL is almost always inherently sequential. In: Logical Methods in Computer Science 7 (2011), Nr. 2, 12. DOI:
dc.description.abstract 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+. eng
dc.language.iso eng
dc.publisher Braunschweig : International Federation for Computational Logic
dc.relation.ispartofseries Logical Methods in Computer Science 7 (2011), Nr. 2
dc.rights CC BY-ND 2.0 Unported
dc.subject Complexity eng
dc.subject Model checking eng
dc.subject Temporal logic eng
dc.subject.ddc 020 | Bibliotheks- und Informationswissenschaft ger
dc.subject.ddc 000 | Informatik, Wissen, Systeme ger
dc.title Model checking CTL is almost always inherently sequential
dc.type article
dc.type Text
dc.relation.issn 1860-5974
dc.bibliographicCitation.issue 2
dc.bibliographicCitation.volume 7
dc.bibliographicCitation.firstPage 12
dc.description.version publishedVersion
tib.accessRights frei zug�nglich

Files in this item

This item appears in the following Collection(s):

Show simple item record


Search the repository


My Account

Usage Statistics