{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T02:42:23Z","timestamp":1772505743133,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662020","type":"print"},{"value":"9783540486831","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_23","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"249-260","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":107,"title":["Improved Automata Generation for Linear Temporal Logic"],"prefix":"10.1007","author":[{"given":"Marco","family":"Daniele","sequence":"first","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"23_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BFb0023737","volume-title":"Proceedings of Computer-Aided Verification (CAV\u2019 90)","author":"C. Courcoubetis","year":"1991","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of Computer-Aided Verification (CAV\u2019 90), volume 531 of LNCS, pages 233\u2013242, Berlin, Germany, June 1991. Springer."},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for linear time temporal logic. Technical Report 9903-10, ITC-IRST, March 1999.","DOI":"10.1007\/3-540-48683-6_23"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3\u201318, Warsaw, Poland, 1995. Chapman & Hall.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures: the case study of modal K. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-96), volume 1104 of LNAI, pages 583\u2013597, Berlin, July30 August-3 1996. Springer.","DOI":"10.1007\/3-540-61511-3_115"},{"issue":"5","key":"23_CR5","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The model checker spin. IEEE Trans. on Software Engineering, 23(5):279\u2013295, May 1997. Special issue on Formal Methods in Software Practice.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"23_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-56922-7_9","volume-title":"Proceedings of Computer-Aided Verification (CAV\u201993)","author":"Y. Kesten","year":"1993","unstructured":"Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In C. Courcoubertis, editor, Proceedings of Computer-Aided Verification (CAV\u201993), volume 697 of LNCS, pages 97\u2013109, Elounda, Greece, June 1993. Springer."},{"key":"23_CR7","unstructured":"D. Mitchell, B. Selman, and H. Levesque. Hard and easy distributions of SAT problems. In W. Swartout, editor, Proceedings of the 10th National Conference on Artificial Intelligence, pages 459\u2013465, San Jose, CA, July 1992. MIT Press."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"S. Schwendimann. A new one-pass tableau calculus for PLTL. Lecture Notes in Computer Science, 1397:277\u2013291, 1998.","DOI":"10.1007\/3-540-69778-0_28"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133\u2013191. Elsevier Science Publishers B. V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"23_CR10","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In lics86, pages 332\u2013344, 1986."},{"issue":"1","key":"23_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Y. Vardi","year":"1994","unstructured":"M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 15 November 1994.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:07:11Z","timestamp":1586153231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}