{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:32:19Z","timestamp":1778297539667,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540569220","type":"print"},{"value":"9783540477877","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56922-7_9","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:54:46Z","timestamp":1330257286000},"page":"97-109","source":"Crossref","is-referenced-by-count":41,"title":["A decision algorithm for full propositional temporal logic"],"prefix":"10.1007","author":[{"given":"Y.","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Z.","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"McGuire","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207\u2013226, 1983.","journal-title":"Acta Informatica"},{"key":"9_CR2","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. J. Comp. Sys. Sci., 18:194\u2013211, 1979.","journal-title":"J. Comp. Sys. Sci."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"G. D. Gough and H. Barringer. A semantic driven temporal verification. In Proceedings of ESOP'88, 1988.","DOI":"10.1007\/3-540-19027-9_2"},{"key":"9_CR4","volume-title":"Master's thesis","author":"G. D. Gough","year":"1984","unstructured":"G. D. Gough. Decision procedures for temporal logic, Master's thesis, University of Manchester, England, 1984."},{"key":"9_CR5","unstructured":"J.A.W. Kamp. Tense Logic and the Theory of Order. PhD thesis, UCLA, 1968."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symp. Princ. of Prog. Lang., pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Proc. Conf. Logics of Programs, volume 193 of Lect. Notes in Comp. Sci., pages 196\u2013218. Springer-Verlag, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"9_CR8","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"9_CR9","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Trans. Prog. Lang. Sys., 6:68\u201393, 1984.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"9_CR10","unstructured":"A. Pnueli and R. Sherman. Semantic tableau for temporal logic. Technical Report CS81-21, The Weizmann Institute, 1981."},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. J. ACM, 32:733\u2013749, 1985.","journal-title":"J. ACM"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"R. Sherman and A. Pnueli. Model checking for linear temporal logic: An efficient implementation. Technical report, Information Science Institute, USC, 1989.","DOI":"10.21236\/ADA225189"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56922-7_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:20Z","timestamp":1605647240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56922-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569220","9783540477877"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-56922-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}