{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:10:09Z","timestamp":1781853009092,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540436317","type":"print"},{"value":"9783540478133","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-47813-2_15","type":"book-chapter","created":{"date-parts":[[2007,5,31]],"date-time":"2007-05-31T02:35:31Z","timestamp":1180578931000},"page":"208-224","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Verification of Probabilistic Free Choice"],"prefix":"10.1007","author":[{"given":"Lenore","family":"Zuck","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yonit","family":"Kesten","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,4,10]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Proc. 13 rd Intl. Conference on Computer Aided Verification (CAV\u201901), volume 2102 ofLect. Notes in Comp. Sci., Springer-Verlag, pages 221\u2013234, 2001.","DOI":"10.1007\/3-540-44585-4_19"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In Proc. 5th ACM Symp. Princ. of Dist. Comp., pages 240\u2013248, 1986.","DOI":"10.1145\/10590.10611"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In 6th International Conference on Concurrency Theory (CONCUR\u201995), pages 395\u2013407, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/0304-3975(84)90118-X","volume":"34","author":"S. Cohen","year":"1984","unstructured":"S. Cohen, D. Lehmann, and A. Pnueli. Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Theor. Comp. Sci., 34:215\u2013225, 1984.","journal-title":"Theor. Comp. Sci."},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In 17th International Conference on Automated Deduction (CADE-17), pages 236\u2013255, 2000.","DOI":"10.1007\/10721959_19"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In Proc. 22th ACM Conf. on Principles of Programming Languages, POPL\u201995, San Francisco, 1995.","DOI":"10.1145\/199448.199468"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, Proc. 8th Intl. Conference on Computer Aided Verification (CAV\u201996), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"S. Hart, M. Sharir, and A. Pnueli. Termination of probabilistic concurrent programs. In Proc. 9th ACM Symp. Princ. of Prog. Lang., pages 1\u20136, 1982.","DOI":"10.1145\/582153.582154"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R.P. Kurshan","year":"1995","unstructured":"R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1\u201311, 1995.","journal-title":"Information and Computation"},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 4(2):328\u2013342, 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"15_CR12","unstructured":"Zuck L. Interim report to PhD Committee. Technical report, Weizmann Institute of Sciences, 1985."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"D. Lehmann and M.O. Rabin. On the advantages of free choice: A symmetric and fully distibuted solution to the dining philosophers problem. In Proc. 8th ACM Symp. Princ. of Prog. Lang., pages 133\u2013138, 1981.","DOI":"10.1145\/567532.567547"},{"key":"15_CR14","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA324036","volume-title":"STeP: The Stanford Temporal Prover","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994."},{"key":"15_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":"15_CR16","doi-asserted-by":"crossref","unstructured":"A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Proc. 7 th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), volume 2031, pages 82\u201397, 2001.","DOI":"10.1007\/3-540-45319-9_7"},{"key":"15_CR17","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\u201996), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 184\u2013195, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"15_CR18","unstructured":"A. Pnueli and L. Zuck. Probablistic verification by tableaux. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 322\u2013331, 1986."},{"key":"15_CR19","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"A. Pnueli and L. Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing, 1:53\u201372, 1986.","journal-title":"Distributed Computing"},{"issue":"1","key":"15_CR20","first-page":"1","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"A. Pnueli and L.D. Zuck. Probabilistic verification. Inf. and Cont., 103(1):1\u201329, 1993.","journal-title":"Inf. and Cont."},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF00288965","volume":"17","author":"M.O. Rabin","year":"1982","unstructured":"M.O. Rabin. The choice coordination problem. Acta Informatica, 17:121\u2013134, 1982.","journal-title":"Acta Informatica"},{"issue":"2","key":"15_CR22","first-page":"167","volume":"102","author":"A.P. Sistla","year":"1993","unstructured":"A.P. Sistla and L.D. Zuck. Reasoning in a restricted temporal logic. Inf. and Cont., 102(2):167\u2013195, 1993.","journal-title":"Inf. and Cont."},{"key":"15_CR23","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."},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of Lect. Notes in Comp. Sci., pages 68\u201380. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47813-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T20:14:31Z","timestamp":1737058471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47813-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540436317","9783540478133"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-47813-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}