{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:41:08Z","timestamp":1770291668119,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540008972","type":"print"},{"value":"9783540365761","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36576-1_6","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"87-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Parameterized Verification by Probabilistic Abstraction"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"issue":"6","key":"6_CR1","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"Krzysztof R. Apt","year":"1986","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.","journal-title":"Information Processing Letters"},{"key":"6_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 thIntl. 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":"6_CR3","unstructured":"T. Arons, A. Pnueli, and L. Zuck. Verification by probabilistic abstraction. Weizmann Institute of Science Technical Report, 2003."},{"key":"6_CR4","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"},{"issue":"2","key":"6_CR5","first-page":"141","volume":"7","author":"K. Baukus","year":"2001","unstructured":"K. Baukus, Y. Lakhnesche, and K. Stahl. Verification of parameterized protocols. Journal of Universal Computer Science, 7(2):141\u2013158, 2001.","journal-title":"Journal of Universal Computer Science"},{"key":"6_CR6","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":"6_CR7","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E. Allen Emerson","year":"2000","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."},{"key":"6_CR8","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":"6_CR9","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":"6_CR10","unstructured":"W. Feller. An Introduction to Probability Theory and its Applicaitons, volume 1. John Wiley & Sons, 3 edition, 1968."},{"key":"6_CR11","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":"6_CR12","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"},{"key":"6_CR13","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Verifying randomized distributed algorithms with prism. In Proc. of the Workshop on Advances in Verification (WAVe) 2000. 2000."},{"key":"6_CR14","series-title":"Lect Notes Comput Sci","volume-title":"TOOLS 2002","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In TOOLS 2002, volume 2324 of LNCS, 2002."},{"issue":"2","key":"6_CR15","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":"6_CR16","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. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proc. 25th Int. Colloq. Aut. Lang. Prog., volume 1443 of LNCS, pages 1\u201316. Springer-Verlag, 1998."},{"key":"6_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Network invariants in action","author":"Y. Kesten","year":"2002","unstructured":"Y. Kesten, A. Pnueli, E. Shahar, and L. Zuck. Network invariants in action. In Proceedings of Concur\u201902, volume 2421 of LNCS. Springer-Verlag, 2002."},{"key":"6_CR18","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 (exended abstract). In Proc. 8th ACM Symp. Princ. of Prog. Lang., pages 133\u2013138, 1981.","DOI":"10.1145\/567532.567547"},{"issue":"2","key":"6_CR19","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"Boris D. Lubachevsky","year":"1984","unstructured":"B.D. Lubachevsky. An approach to automating the verification of compact parallel coordination programs. Acta Infromatica, 21, 1984.","journal-title":"Acta Informatica"},{"key":"6_CR20","series-title":"Technical Report","doi-asserted-by":"publisher","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":"6_CR21","doi-asserted-by":"publisher","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":"6_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. On the extremely fair treatment of probabilistic algorithms. In Proc. 15th ACM Symp. Theory of Comp., pages 278\u2013290, 1983.","DOI":"10.1145\/800061.808757"},{"key":"6_CR23","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":"6_CR24","doi-asserted-by":"crossref","unstructured":"A. Pnueli, J. Xu, and L. Zuck. The (0, 1,\u2208) counter abstraction. In Proc. 14 thIntl. Conference on Computer Aided Verification (CAV\u201902), volume 2404 ofLect. Notes in Comp. Sci., Springer-Verlag, 2002. http:\/\/www.cs.nyu.edu\/~zuck\/pubs\/cav02.ps.","DOI":"10.1007\/3-540-45657-0_9"},{"key":"6_CR25","unstructured":"A. Pnueli and L. Zuck. Probablistic verification by tableaux. In Proc. First IEEE Symp. Logic in Comp. Sci., pages 322\u2013331, 1986."},{"key":"6_CR26","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":"6_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"A. Pnueli and L.D. Zuck. Probabilistic verification. Information and Computation, 103(1):1\u201329, 1993.","journal-title":"Information and Computation"},{"key":"6_CR28","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"},{"key":"6_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-52148-8_13","volume-title":"Automatic Verification Methods for Finite State Systems","author":"Z. Shtadler","year":"1990","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of LNCS, pages 151\u2013165. Springer-Verlag, 1989."},{"key":"6_CR30","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":"6_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1989","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 LNCS, pages 68\u201380. Springer-Verlag, 1989."},{"key":"6_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Automatic verification of probabilistic free choice","author":"L. Zuck","year":"2002","unstructured":"L. Zuck, A. Pnueli, and Y. Kesten. Automatic verification of probabilistic free choice. In Proc. of the 3 rdworkshop on Verification, Model Checking, and Abstract Interpretation, volume 2294 of LNCS, 2002."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:53:51Z","timestamp":1737093231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-36576-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 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"}]}}