{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:16:08Z","timestamp":1778249768632,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440437","type":"print"},{"value":"9783540456940","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45694-5_2","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T03:44:18Z","timestamp":1191555858000},"page":"24-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["A Deductive Proof System for CTL*"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yonit","family":"Kesten","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Sys., 8:244\u2013263, 1986.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"CAV\u201994","author":"E. Clarke","year":"1994","unstructured":"E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. CAV\u201994, LNCS 818, pages 415\u2013427."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","first-page":"255","volume-title":"CAV\u201999","author":"M. Daniele","year":"1999","unstructured":"M. Daniele, F. Giunchiglia, and M.Y. Vardi. Improved automata generation for linear time temporal logic. CAV\u201999, LNCS 1633, pages 255\u2013265."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"E. Emerson. Temporal and modal logics. In J. van Leeuwen, editor, Handbook of theoretical computer science, volume B, pages 995\u20131072. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"E. Emerson and C. Lei. Modalities for model checking: Branching time strikes back. POPL\u201985, pages 84\u201396.","DOI":"10.1145\/318593.318620"},{"key":"2_CR6","unstructured":"D. Gabbay. The declarative past and imperative future.In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Temporal Logic in Specification, volume 398 of Lect. Notes in Comp. Sci., pages 407\u2013448. Springer-Verlag, 1987."},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"P. Gastin","year":"2001","unstructured":"P. Gastin and D. Oddoux. Fast LTL to B\u00fcchi automata translation. CAV\u201901, LNCS 2102."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. PSTV\u201995, pages 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. PSTV\u201995, pages 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. CAV\u201993, pages 97\u2013109.","DOI":"10.1007\/3-540-56922-7_9"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, a special issue on Compositionality, 163:203\u2013243, 2000.","journal-title":"Information and Computation, a special issue on Compositionality"},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Algorithmic verification of linear temporal logic specifications","author":"Y. Kesten","year":"1998","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. Proc. 25th Int. Colloq. Aut. Lang. Prog., LNCS 1443, pages 1\u201316, 1998."},{"key":"2_CR13","unstructured":"Y. Kesten, A. Pnueli, L. Raviv, and E. Shahar. LTL Model Checking with Strong Fairness. Technical Report mcs01-07, The Weizmann Institute of Science, 2001. Submitted to Formal Methods in System Design."},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Impartiality, justice and fairness: The ethics of concurrent termination","author":"D. Lehmann","year":"1981","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., LNCS 115, pages 264\u2013277, 1981."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite-state concurrent programs satisfy their linear specification. POPL\u201985, pages 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L.D. Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Stanford University, 1994.","DOI":"10.21236\/ADA324036"},{"issue":"1","key":"2_CR17","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":"2_CR18","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":"2_CR19","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":"2_CR20","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"K. Namjoshi","year":"2001","unstructured":"K. Namjoshi. Certifying model checkers. CAV\u201901, LNCS 2102."},{"key":"2_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-45294-X_25","volume-title":"FTTCS\u201901","author":"D. Peled","year":"2001","unstructured":"D. Peled, A. Pnueli, and L. Zuck. From falsification to verification. FTTCS\u201901, LNCS 2245, pages 292\u2013304."},{"key":"2_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/3-540-50403-6_28","volume-title":"Concurrency 88","author":"A. Pnueli","year":"1988","unstructured":"A. Pnueli and R. Rosner. A framework for the synthesis of reactive modules. Concurrency 88, LNCS 335, pages 4\u201317."},{"issue":"3","key":"2_CR23","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.2307\/2695091","volume":"66","author":"M. Reynolds","year":"2001","unstructured":"M. Reynolds. An axiomatization of full computation tree logic. Journal of Symbolic Logic, 66(3):1011\u20131057, 2001.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"2_CR24","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1008791913551","volume":"15","author":"H. Sipma","year":"1999","unstructured":"H. Sipma, T. Uribe, and Z. Manna. Deductive model checking. Formal Methods in System Design, 15(1):49\u201374, 1999.","journal-title":"Formal Methods in System Design"},{"key":"2_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"CAV\u201900","author":"F. Somenzi","year":"2000","unstructured":"F. Somenzi and R. Bloem. Efficient B\u00fcchi automata from LTL formulae. CAV\u201900, LNCS 1855, pages 248\u2013263."},{"key":"2_CR26","unstructured":"C. Sprenger. On the Verification of CTL Properties of Infinite-State Reactive Systems. PhD thesis, Swiss Federal Institute of Technology, Lausanne, 2000."},{"key":"2_CR27","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1016\/0890-5401(89)90004-7","volume":"82","author":"F. Stomp","year":"1989","unstructured":"F. Stomp, W.-P. de Roever, and R. Gerth. The \u03bc-calculus as an assertion language for fairness arguments. Inf. and Comp., 82:278\u2013322, 1989.","journal-title":"Inf. and Comp."},{"issue":"1","key":"2_CR28","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. Inf. and Comp., 115(1):1\u201337, 1994.","journal-title":"Inf. and Comp."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2002 \u2014 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45694-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:50:02Z","timestamp":1778248202000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-45694-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440437","9783540456940"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45694-5_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 September 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}