{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:35:55Z","timestamp":1753889755585,"version":"3.41.2"},"reference-count":24,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T00:00:00Z","timestamp":1305590400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The model checking problem for CTL is known to be P-complete (Clarke,\nEmerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of\nCTL obtained by restricting the use of temporal modalities or the use of\nnegations---restrictions already studied for LTL by Sistla and Clarke (1985)\nand Markey (2004). For all these fragments, except for the trivial case without\nany temporal operator, we systematically prove model checking to be either\ninherently sequential (P-complete) or very efficiently parallelizable\n(LOGCFL-complete). For most fragments, however, model checking for CTL is\nalready P-complete. Hence our results indicate that, in cases where the\ncombined complexity is of relevance, approaching CTL model checking by\nparallelism cannot be expected to result in any significant speedup. We also\ncompletely determine the complexity of the model checking problem for all\nfragments of the extensions ECTL, CTL+, and ECTL+.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:12)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":5,"title":["Model Checking CTL is Almost Always Inherently Sequential"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2870-1648","authenticated-orcid":false,"given":"Olaf","family":"Beyersdorff","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8061-5376","authenticated-orcid":false,"given":"Arne","family":"Meier","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Mundhenk","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Thomas","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9292-1960","authenticated-orcid":false,"given":"Heribert","family":"Vollmer","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,5,17]]},"reference":[{"key":"10.2168\/LMCS-7(2:12)2011_BMMSTV09","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2009.12"},{"key":"10.2168\/LMCS-7(2:12)2011_bamuscscscvo07entcs","doi-asserted-by":"crossref","unstructured":"M. Bauland, M. Mundhenk, T. Schneider, H. Schnoor, I. Schnoor, and H. Vollmer. The tractability of model checking for LTL: the good, the bad, and the ugly fragments. InProc. 5th Methods for Modalities, volume 231 ofElectronic Notes in Theoretical Computer Science, pages 277-292, 2009.","DOI":"10.1016\/j.entcs.2009.02.041"},{"key":"10.2168\/LMCS-7(2:12)2011_bus87","doi-asserted-by":"crossref","unstructured":"S. R. Buss. The Boolean formula value problem is in ALOGTIME. InProc. 19th Symposium on Theory of Computing, pages 123-131. ACM Press, 1987.","DOI":"10.1145\/28395.28409"},{"key":"10.2168\/LMCS-7(2:12)2011_BVW94","doi-asserted-by":"crossref","unstructured":"O. Bernholtz, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking (extended abstract). InProc. 6th International Conference on Computer Aided Verification, volume 818 ofLecture Notes in Computer Science, pages 142-155. Springer, 1994.","DOI":"10.1007\/3-540-58179-0_50"},{"issue":"2","key":"10.2168\/LMCS-7(2:12)2011_clemsi86","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke, E. A. Emerson, and A. Sistla","year":"1986","journal-title":"\u00c3\u0085CM Transactions on Programming Languages and Systems 8(2):244-263, 1986"},{"issue":"3","key":"10.2168\/LMCS-7(2:12)2011_emcl82","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson and E. M. Clarke","year":"1982","journal-title":"Science of Computer Programming"},{"issue":"1","key":"10.2168\/LMCS-7(2:12)2011_emha85","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E. A. Emerson and J. Y. Halpern","year":"1985","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"10.2168\/LMCS-7(2:12)2011_emha86","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson and J. Y. Halpern","year":"1986","journal-title":"Journal of the ACM"},{"issue":"3","key":"10.2168\/LMCS-7(2:12)2011_emle87","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson and C.-L. Lei","year":"1987","journal-title":"Science of Computer Programming"},{"key":"10.2168\/LMCS-7(2:12)2011_KuhFin09","doi-asserted-by":"crossref","unstructured":"L. Kuhtz and B. Finkbeiner. LTL Path Checking is Efficiently Parallelizable.International Colloquium on Automata, Languages and Programming, 2009.","DOI":"10.1007\/978-3-642-02930-1_20"},{"issue":"2","key":"10.2168\/LMCS-7(2:12)2011_KuVaWo00","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman, M. Y. Vardi, and P. Wolper","year":"2000","journal-title":"Journal of the ACM"},{"issue":"6","key":"10.2168\/LMCS-7(2:12)2011_laroussinie95","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0020-0190(95)00053-F","volume":"54","author":"F. Laroussinie","year":"1995","journal-title":"Information Processing Letters"},{"key":"10.2168\/LMCS-7(2:12)2011_lamasc01","doi-asserted-by":"crossref","unstructured":"F. Laroussinie, N. Markey, and P. Schnoebelen. Model checking CTL+and FCTL is hard. InProc. 4th Foundations of Software Science and Computation Structure, volume 2030 ofLecture Notes in Computer Science, pages 318-331. Springer Verlag, 2001.","DOI":"10.1007\/3-540-45315-6_21"},{"issue":"6-7","key":"10.2168\/LMCS-7(2:12)2011_mar04","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/s00236-003-0136-5","volume":"40","author":"N. Markey","year":"2004","journal-title":"\u00c3\u0085cta Informatica"},{"issue":"5","key":"10.2168\/LMCS-7(2:12)2011_memuthvo08","doi-asserted-by":"crossref","first-page":"901","DOI":"10.1142\/S0129054109006954","volume":"20","author":"A. Meier, M. Mundhenk, M. Thomas, and H.","year":"2009","journal-title":"International Journal of Foundations of Computer Science 20(5):901-918, 2009"},{"key":"10.2168\/LMCS-7(2:12)2011_pap94","unstructured":"C. H. Papadimitriou.Computational Complexity. Addison-Wesley, Reading, MA, 1994."},{"key":"10.2168\/LMCS-7(2:12)2011_pnu77","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. InProc. 18th Symposium on Foundations of Computer Science, pages 46-57. IEEE Computer Society Press, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.2168\/LMCS-7(2:12)2011_ruz80","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1016\/0022-0000(80)90036-7","volume":"21","author":"W. L. Ruzzo","year":"1980","journal-title":"Journal of Computer and System Sciences"},{"key":"10.2168\/LMCS-7(2:12)2011_revo97","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(96)00288-5","volume":"188","author":"K. Regan and H. Vollmer","year":"1997","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10.2168\/LMCS-7(2:12)2011_sicl85","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla and E. Clarke","year":"1985","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-7(2:12)2011_schnoeb02","unstructured":"Ph. Schnoebelen.The Complexity of Temporal Logic Model Checking, volume 4 ofAdvances in Modal Logic, pages 393-436. King's College Publications, 2003."},{"issue":"3","key":"10.2168\/LMCS-7(2:12)2011_sc10","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1142\/S0129054110007258","volume":"21","author":"H. Schnoor","year":"2010","journal-title":"Int. Journal on Foundations of Computer Science 21(3):289-309, 2010"},{"key":"10.2168\/LMCS-7(2:12)2011_selman82","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(82)90039-1","volume":"19","author":"A. L. Selman","year":"1982","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(2:12)2011_vol99","doi-asserted-by":"crossref","unstructured":"H. Vollmer.Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer Verlag, Berlin Heidelberg, 1999.","DOI":"10.1007\/978-3-662-03927-4"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1007\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1007\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:59Z","timestamp":1681243259000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1007"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,17]]},"references-count":24,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:12)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1103.4990","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1103.4990","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1186\/s12918-018-0670-y","asserted-by":"subject"},{"id-type":"pmid","id":"30594246","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,5,17]]},"article-number":"1007"}}