{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T22:13:22Z","timestamp":1757456002343},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319737201"},{"type":"electronic","value":"9783319737218"}],"license":[{"start":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T00:00:00Z","timestamp":1514505600000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-73721-8_16","type":"book-chapter","created":{"date-parts":[[2017,12,28]],"date-time":"2017-12-28T04:13:05Z","timestamp":1514434385000},"page":"336-357","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["$$P^5$$ : Planner-less Proofs of Probabilistic Parameterized Protocols"],"prefix":"10.1007","author":[{"given":"Lenore D.","family":"Zuck","sequence":"first","affiliation":[]},{"given":"Kenneth L.","family":"McMillan","sequence":"additional","affiliation":[]},{"given":"Jordan","family":"Torf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,12,29]]},"reference":[{"key":"16_CR1","unstructured":"IEEE standard for a high-performance serial bus. IEEE standard 1394\u20131008 (2008)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic program verification of finite-state concurrent systems. Inf. Process. Lett. 22(6) (1986)","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 221\u2013234. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_19"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Arons, T., Pnueli, A., Zuck, L.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 87\u2013102. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_6","DOI":"10.1007\/3-540-36576-1_6"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Beauquier, J., Gradinariu, M., Johnen, C.: Memory space requirements for self-stabilizing leader election protocols. In: PODC 1999, pp. 199\u2013207 (1999)","DOI":"10.1145\/301308.301358"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Cohen, S., Lehmann, D., Pnueli, A.: Symmetric and economical solutions to the mutual exclusion problem in a distributed system. Theoretical Comput. Sci. 34, 215\u2013225 (1984)","DOI":"10.1016\/0304-3975(84)90118-X"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th Annual Symposium on Principles of Programming Languages. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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":"Allen Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol. 1831, pp. 236\u2013254. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721959_19"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E Allen Emerson","year":"1996","unstructured":"Allen Emerson, E., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 87\u201398. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_60"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL 1995, San Francisco (1995)","DOI":"10.1145\/199448.199468"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31424-7_14","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2012","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123\u2013138. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_14"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. In: POPL 1982, pp. 1\u20136 (1982)","DOI":"10.1145\/582153.582154"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Herman, T.: Probabilistic self-stabilization. Information Processing Letters 35(2), 63\u201367 (1990)","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: Proc. 9th Annual ACM Symposium on Principles of Distributed Computing (PODC 1990), pp. 119\u2013131. ACM New York (1990)","DOI":"10.1145\/93385.93409"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed network. In: FOCS 1981, pp. 245\u2013260 (1981)","DOI":"10.1109\/SFCS.1981.41"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Kempe, D., Dobra, A., Gehrke, J.: Gossip-based computation of aggregate information. In: Proceedings of 44th Symposium on Foundations of Computer Science (FOCS 2003), Cambridge, MA, USA, October 11-14, pp. 482\u2013491 (2003)","DOI":"10.1109\/SFCS.2003.1238221"},{"key":"16_CR17","first-page":"2000","volume":"163","author":"Y Kesten","year":"1999","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Information and Computation 163, 2000 (1999)","journal-title":"Information and Computation"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: The cornerstones of practical formal verification. Software Tools for Technology Transfer 4, 2000 (2000)","DOI":"10.1007\/s100090050040"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Lehmann, D., Rabin, M.: On the advantages of free choice: A symmetric and fully distibuted solution to the dining philosophers problem (exended abstract). In: POPL 1981, pp. 133\u2013138 (1981)","DOI":"10.1145\/567532.567547"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-41540-6_7","volume-title":"Computer Aided Verification","author":"AW Lin","year":"2016","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 112\u2013133. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_7"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 24\u201335. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_6"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A. : On the extremely fair treatment of probabilistic algorithms. In: STOC 1983, pp. 278\u2013290. ACM New York (1983)","DOI":"10.1145\/800061.808757"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 82\u201397. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_7"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0, 1, $$\\infty $$ )-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107\u2013122. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_9"},{"key":"16_CR26","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification by tableaux. In: LICS 1986, pp. 322\u2013331 (1986)"},{"issue":"1","key":"16_CR27","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distributed Computing 1(1), 53\u201372 (1986)","journal-title":"Distributed Computing"},{"issue":"1","key":"16_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput. 103(1), 1\u201329 (1993)","journal-title":"Inf. Comput."},{"key":"16_CR29","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF00288965","volume":"17","author":"M Rabin","year":"1982","unstructured":"Rabin, M.: The choice coordination problem. Acta Informatica 17, 121\u2013134 (1982)","journal-title":"Acta Informatica"},{"key":"16_CR30","unstructured":"Shakespeare, W.: The Tragedy of Macbeth. ca. 1606 (4.3.225)"},{"key":"16_CR31","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS 1986, pp. 332\u2013344 (1986)"},{"key":"16_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-47813-2_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Zuck","year":"2002","unstructured":"Zuck, L., Pnueli, A., Kesten, Y.: Automatic verification of probabilistic free choice. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 208\u2013224. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-47813-2_15"}],"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\/978-3-319-73721-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T16:01:08Z","timestamp":1570550468000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-73721-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,29]]},"ISBN":["9783319737201","9783319737218"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-73721-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017,12,29]]}}}