{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T16:52:25Z","timestamp":1773939145180,"version":"3.50.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["630\/6-1"],"award-info":[{"award-number":["630\/6-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If in contrast, the set of propositional operators is restricted, the complexity may decrease. This article systematically studies the model-checking problem for LTL formulae over restricted sets of propositional and temporal operators. For almost all combinations of temporal and propositional operators, we determine whether the model-checking problem is tractable (in PTIME) or intractable (NP-hard). We then focus on the tractable cases, showing that they all are NL-complete or even logspace solvable. This leads to a surprising gap in complexity between tractable and intractable cases. It is worth noting that our analysis covers an infinite set of problems, since there are infinitely many sets of propositional operators.<\/jats:p>","DOI":"10.1145\/1877714.1877719","type":"journal-article","created":{"date-parts":[[2011,1,25]],"date-time":"2011-01-25T19:12:52Z","timestamp":1295982772000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["The tractability of model checking for LTL"],"prefix":"10.1145","volume":"12","author":[{"given":"Michael","family":"Bauland","sequence":"first","affiliation":[{"name":"Knipp GmbH"}]},{"given":"Martin","family":"Mundhenk","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Jena"}]},{"given":"Thomas","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Manchester"}]},{"given":"Henning","family":"Schnoor","sequence":"additional","affiliation":[{"name":"Christian-Albrechts-Universit\u00e4t Kiel"}]},{"given":"Ilka","family":"Schnoor","sequence":"additional","affiliation":[{"name":"Universit\u00e4t L\u00fcbeck"}]},{"given":"Heribert","family":"Vollmer","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Hannover"}]}],"member":"320","published-online":{"date-parts":[[2011,1,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1813084.1813131"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11672142_41"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.02.041"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760037.1760044"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2009.12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/954092.954101"},{"key":"e_1_2_1_7_1","unstructured":"Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press.   Clarke E. Grumberg O. and Peled D. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3094"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.26"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/876661.876668"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0164-4"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01744287"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-003-0136-5"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006954"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054105003261"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 11th International Conference on Logic for Programming","author":"Nordh G.","unstructured":"Nordh , G. 2005. A trichotomy in the complexity of propositional circumscription . In Proceedings of the 11th International Conference on Logic for Programming . Lecture Notes in Computer Science , vol. 3452 , Springer Verlag , 257--269. Nordh, G. 2005. A trichotomy in the complexity of propositional circumscription. In Proceedings of the 11th International Conference on Logic for Programming. Lecture Notes in Computer Science, vol. 3452, Springer Verlag, 257--269."},{"key":"e_1_2_1_20_1","volume-title":"Computational Complexity","author":"Papadimitriou C. H.","unstructured":"Papadimitriou , C. H. 1994. Computational Complexity . Addison-Wesley , Reading, MA . Papadimitriou, C. H. 1994. Computational Complexity. Addison-Wesley, Reading, MA."},{"key":"e_1_2_1_21_1","volume-title":"Theories of Computability","author":"Pippenger N.","unstructured":"Pippenger , N. 1997. Theories of Computability . Cambridge University Press , Cambridge, UK . Pippenger, N. 1997. Theories of Computability. Cambridge University Press, Cambridge, UK."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_23_1","first-page":"1","article-title":"The two-valued iterative systems of mathematical logic","volume":"5","author":"Post E.","year":"1941","unstructured":"Post , E. 1941 . The two-valued iterative systems of mathematical logic . Annals Mathem. Studies 5 , 1 -- 122 . Post, E. 1941. The two-valued iterative systems of mathematical logic. Annals Mathem. Studies 5, 1--122.","journal-title":"Annals Mathem. Studies"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00092-0"},{"key":"e_1_2_1_26_1","unstructured":"Reith S. and Wagner K. W. 2000. The complexity of problems defined by Boolean circuits. Tech. rep. 255 Institut f\u00fcr Informatik Universit\u00e4t W\u00fcrzburg.  Reith S. and Wagner K. W. 2000. The complexity of problems defined by Boolean circuits. Tech. rep. 255 Institut f\u00fcr Informatik Universit\u00e4t W\u00fcrzburg."},{"key":"e_1_2_1_27_1","volume-title":"Theoretical Computer Science","author":"Schnoor H.","unstructured":"Schnoor , H. 2005. The complexity of the Boolean formula value problem. Tech. rep ., Theoretical Computer Science , University of Hannover. Schnoor, H. 2005. The complexity of the Boolean formula value problem. Tech. rep., Theoretical Computer Science, University of Hannover."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/3127070.3127077"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Wolper P. 1983. Temporal logic can be more expressive. Inform. Control 56 1\/2 72--99.  Wolper P. 1983. Temporal logic can be more expressive. Inform. Control 56 1\/2 72--99.","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877719","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1877714.1877719","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:17:37Z","timestamp":1750249057000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877719"}},"subtitle":["The good, the bad, and the ugly fragments"],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1877714.1877719"],"URL":"https:\/\/doi.org\/10.1145\/1877714.1877719","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2008-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}