Model checking CTL is almost always inherently sequential

Show simple item record

dc.identifier.uri http://dx.doi.org/10.15488/621
dc.identifier.uri http://www.repo.uni-hannover.de/handle/123456789/645
dc.contributor.author Beyersdorff, Olaf
dc.contributor.author Meier, Arne
dc.contributor.author Mundhenk, Martin
dc.contributor.author Schneider, Thomas
dc.contributor.author Thomas, Michael
dc.contributor.author Vollmer, Heribert
dc.date.accessioned 2016-11-02T13:35:59Z
dc.date.available 2016-11-02T13:35:59Z
dc.date.issued 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: http://dx.doi.org/10.2168/LMCS-7(2:12)2011
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.rights.uri https://creativecommons.org/licenses/by-nd/2.0/
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.relation.doi http://dx.doi.org/10.2168/LMCS-7(2:12)2011
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


Browse

My Account

Usage Statistics