{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T02:45:10Z","timestamp":1783392310272,"version":"3.54.6"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540647812","type":"print"},{"value":"9783540686811","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055036","type":"book-chapter","created":{"date-parts":[[2006,8,1]],"date-time":"2006-08-01T12:08:05Z","timestamp":1154434085000},"page":"1-16","source":"Crossref","is-referenced-by-count":69,"title":["Algorithmic verification of linear temporal logic specifications"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li-on","family":"Raviv","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2006,5,26]]},"reference":[{"issue":"2","key":"1_CR1","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. IBM Workshop on Logics of Programs, volume 131 of Lect. Notes in Comp. Sci., pages 52\u201371. Springer-Verlag, 1981.","DOI":"10.1007\/BFb0025774"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at ltl model checking. In D. L. Dill, editor, Proc. 6th Conference on Computer Aided Verification, volume 818 of Lect. Notes in Comp. Sci., pages 415\u2013427. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_72"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.L. Lei. Modalities for model checking: Branching time strikes back. In Proc. 12th ACM Symp. Princ. of Prog. Lang., pages 84\u201396, 1985.","DOI":"10.1145\/318593.318620"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"N. Francez. Fairness. Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proc. 7th ACM Symp. Princ. of Prog. Lang., pages 163\u2013173, 1980.","DOI":"10.1145\/567446.567462"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"R. H. Hardin, R. P. Kurshan, S. K. Shukla, and M. Y. Vardi. A new heuristic for bad cycle detection using BDDs. In O. Grumberg, editor, Proc. 9th Intl. Conference on Computer Aided Verification (CAV'97), Lect. Notes in Comp. Sci., pages 268\u2013278. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_27"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"M. R. Henzinger and J. A. Telle. Faster algorithms for the nonemptiness of street automata and for communication protocol prunning. In Proceedings of the 5th Scandinavian Workshop on Algorithm Theory, pages 10\u201320, 1996.","DOI":"10.1007\/3-540-61422-2_117"},{"key":"1_CR9","unstructured":"O. Lichtenstein. Decidability, Completeness, and Extensions of Linear Time Temporal Logic. PhD thesis, Weizmann Institute of Science, 1991."},{"key":"1_CR10","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":"1_CR11","doi-asserted-by":"crossref","unstructured":"D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In Proc. 8th Int. Colloq. Aut. Lang. Prog., volume 115 of Lect. Notes in Comp. Sci., pages 264\u2013277. Springer-Verlag, 1981.","DOI":"10.1007\/3-540-10843-2_22"},{"key":"1_CR12","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"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97\u2013130, 1991.","journal-title":"Theor. Comp. Sci."},{"key":"1_CR14","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":"1_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification (CAV'96), Lect. Notes in Comp. Sci., pages 184\u2013195. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in cesar. In M. Dezani-Ciancaglini and M. Montanari, editors, International Symposium on Programming, volume 137 of Lect. Notes in Comp. Sci., pages 337\u2013351. Springer-Verlag, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1016\/0890-5401(89)90004-7","volume":"82","author":"F.A. Stomp","year":"1989","unstructured":"F.A. Stomp, W.-P. de Roever, and R.T. Gerth. The \u039c-calculus as an assertion language for fairness arguments. Inf. and Comp., 82:278\u2013322, 1989.","journal-title":"Inf. and Comp."},{"key":"1_CR19","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 332\u2013344, 1986."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055036","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T10:24:12Z","timestamp":1683541452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055036"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540647812","9783540686811"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0055036","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998]]}}}