{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:00Z","timestamp":1761611160218},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1986,3,1]],"date-time":"1986-03-01T00:00:00Z","timestamp":510019200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Distrib Comput"],"published-print":{"date-parts":[[1986,3]]},"DOI":"10.1007\/bf01843570","type":"journal-article","created":{"date-parts":[[2005,6,29]],"date-time":"2005-06-29T00:52:45Z","timestamp":1120006365000},"page":"53-72","source":"Crossref","is-referenced-by-count":84,"title":["Verification of multiprocess probabilistic protocols"],"prefix":"10.1007","volume":"1","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF01843570_CR1","unstructured":"Burns JE, Fischer MJ, Jackson P, Lynch NA, Peterson GL (1978) Shared data requirements for imolementation of mutual exclusion using a test-and-set primitive. Proc Intr Conf Parallel Processing, pp 79\u201387"},{"key":"BF01843570_CR2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/0304-3975(84)90118-X","volume":"34","author":"S Cohen","year":"1984","unstructured":"Cohen, S, Lehmann D, Pnueli A (1984) Symmetric and economical solution to the mutual exclusion problem in distributed systems. Theor Comp Sci 34:215\u2013226","journal-title":"Theor Comp Sci"},{"key":"BF01843570_CR3","doi-asserted-by":"crossref","unstructured":"Dijkstra EW (1972) Hierarchical ordering of sequential process. Operating system techniques. Academic Press","DOI":"10.1007\/978-1-4757-3472-0_5"},{"key":"BF01843570_CR4","unstructured":"Feller W (1967) An introduction to probability theory and its appliction 3rd ed, vol 1, ch. XIII, section 7. Wiley, pp 322\u2013324"},{"key":"BF01843570_CR5","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/2166.357214","volume":"5","author":"S Hart","year":"1983","unstructured":"Hart S, Sharir M, Pnueli A (1983) Termintion of probabilistic concurrent programs. TOPLAS 5:356\u2013380","journal-title":"TOPLAS"},{"key":"BF01843570_CR6","series-title":"RJ 3110","volume-title":"The lord of the ring, or probabilistic methods for breaking symmetry in distributive networks","author":"A Itai","year":"1981","unstructured":"Itai A, Rodeh M (1981) The lord of the ring, or probabilistic methods for breaking symmetry in distributive networks. RJ 3110, IBM, San Jose"},{"key":"BF01843570_CR7","doi-asserted-by":"crossref","unstructured":"Lehmann D, Rabin MO (1981) On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract) Conf Record of the 8th Annual ACM Symp on Principles of Programming Languages, Williamsburg, VA, Jan 1981, pp 133\u2013138","DOI":"10.1145\/567532.567547"},{"key":"BF01843570_CR8","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D Lehmann","year":"1982","unstructured":"Lehmann D, Shelah S (1982) Reasoning with time and chance. Inf Control 53: 165\u2013198","journal-title":"Inf Control"},{"key":"BF01843570_CR9","series-title":"Proceedings of the Workshop on Logics of Programs","volume-title":"The glory of the past","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein O, Pnueli A, Zuck L (1985) The glory of the past. Proceedings of the Workshop on Logics of Programs, Spriger-Verlag, New York"},{"key":"BF01843570_CR10","series-title":"Proc of the Workshop on Logic of Programs","doi-asserted-by":"crossref","first-page":"200","DOI":"10.21236\/ADA116035","volume-title":"Verification of concurrent programs: temporal proof principles","author":"Z Manna","year":"1981","unstructured":"Manna Z, Pnueli A (1981) Verification of concurrent programs: temporal proof principles. Proc of the Workshop on Logic of Programs. Springer-Verlag, New York, pp 200\u2013252"},{"key":"BF01843570_CR11","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1982) Verification of concurrent programs: a temporal proof system. Proc 4th School on Advanced Programming, Amsterdam","DOI":"10.21236\/ADA116035"},{"key":"BF01843570_CR12","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1983) How to cook a temporal system for your pet language. Proc of the 10th Annual ACM Symp on Principles of Programming Languages","DOI":"10.1145\/567067.567082"},{"key":"BF01843570_CR13","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"S Owicki","year":"1982","unstructured":"Owicki S, Lamport L (1982) Proving liveness properties of concurrent programs. TOPLAS 4:455\u2013495","journal-title":"TOPLAS"},{"key":"BF01843570_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli A (1983) On the extremely fair treatment of probabilistic algorithms. Proc of the 15th Annual Symp on Theory of Computing","DOI":"10.1145\/800061.808757"},{"key":"BF01843570_CR15","volume-title":"Probabilistic algorithms. Algorithms and complexity new directions and recent results","author":"MO Rabin","year":"1976","unstructured":"Rabin MO (1976) Probabilistic algorithms. Algorithms and complexity new directions and recent results. Academic Press, New York"},{"key":"BF01843570_CR16","series-title":"Tech Report Forschungsinstitute f\u00fcr Mathematik","volume-title":"N-process synchronization by 4 logN-valued shared variables","author":"MO Rabin","year":"1980","unstructured":"Rabin MO (1980) N-process synchronization by 4 logN-valued shared variables. Tech Report Forschungsinstitute f\u00fcr Mathematik, ETH, Z\u00fcrich"},{"key":"BF01843570_CR17","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF00288965","volume":"17","author":"MO Rabin","year":"1982","unstructured":"Rabin MO (1982) The choice coordimation problem, Acta Inf 17:121\u2013134","journal-title":"Acta Inf"},{"key":"BF01843570_CR18","volume-title":"Probabilistic temporal logics for finite and bounded models","author":"M Sharir","year":"1983","unstructured":"Sharir M, Hart S (1983) Probabilistic temporal logics for finite and bounded models. Tel-Aviv University, Tel-Aviv"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01843570.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01843570\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01843570","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T01:40:59Z","timestamp":1586310059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01843570"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,3]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1986,3]]}},"alternative-id":["BF01843570"],"URL":"https:\/\/doi.org\/10.1007\/bf01843570","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"value":"0178-2770","type":"print"},{"value":"1432-0452","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986,3]]}}}