{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:52:28Z","timestamp":1725483148647},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_2","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T10:18:07Z","timestamp":1178014687000},"page":"19-33","source":"Crossref","is-referenced-by-count":0,"title":["Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Annabelle K.","family":"McIver","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20:207\u2013226, 1983.","journal-title":"Acta Informatica"},{"key":"2_CR2","volume-title":"Parallel Program Design: A Foundation","author":"K. M. Chandy","year":"1988","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, Mass., 1988."},{"key":"2_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of STACS\u2019 97","author":"L. Alfaro de","year":"1997","unstructured":"L. de Alfaro. Temporal logics for the specification of performance and reliability. Proceedings of STACS\u2019 97, LNCS volume 1200, 1997."},{"key":"2_CR4","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976."},{"key":"2_CR5","unstructured":"W. Feller. An Introduction to Probability Theory and its Applications, volume 1. Wiley, second edition, 1971."},{"issue":"5","key":"2_CR6","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"issue":"23","key":"2_CR7","first-page":"171","volume":"28","author":"J. He","year":"1997","unstructured":"Jifeng He, K. Seidel, and A. K. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2,3):171\u2013192, January 1997.","journal-title":"Science of Computer Programming"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"D. Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, New York, 1983. ACM.","DOI":"10.1145\/800061.808758"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"D. Lehmann and M. O. Rabin. On the advantages of free choice: a symmetric and fully-distributed solution to the Dining Philosophers Problem. In Proceedings of the 8th Annual ACM Symposium on Principles of Programming Languages, pages 133\u2013138, New York, 1981. ACM","DOI":"10.1145\/567532.567547"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"N. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. Proceedings of 13th Annual Symposium on Principles of Distributed Algorithms, pages 314\u2013323, 1994.","DOI":"10.1145\/197917.198117"},{"key":"2_CR12","unstructured":"A.K. McIver. Quantitative program logic and efficiency in probabilistic distributed algorithms. Technical report. See QLE98 at http [18]."},{"key":"2_CR13","unstructured":"A.K. McIver. Reasoning about efficiency within a probabilistic mucalculus. 1998. Submitted to pre-LICS98 workshop on Probabilistic Methods in Verification."},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C. C. Morgan","year":"1996","unstructured":"C. C. Morgan, A. K. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325\u2013353, May 1996.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of B\u201998: the Second International B Conference. See B98 at http [18]","author":"C. Morgan","year":"1998","unstructured":"Carroll Morgan. The generalised substitution language extended to probabilistic programs. In Proceedings of B\u201998: the Second International B Conference. See B98 at http [18], number 1397 in LNCS. Springer Verlag, April 1998."},{"key":"2_CR16","unstructured":"Carroll Morgan and Annabelle McIver. A probabilistic temporal calculus based on expectations. In Lindsay Groves and Steve Reeves, editors, Proc. Formal Methods Pacific\u2019 97. Springer Verlag Singapore, July 1997. Available at [18]."},{"key":"2_CR17","unstructured":"C.C. Morgan and A.K. McIver. Correctness proof for the randomised dining philosophers. See RDP96 at http [18]."},{"key":"2_CR18","unstructured":"PSG. Probabilistic Systems Group: Collected reports. http:\/\/www.comlab.ox.ac.uk\/oucl\/groups\/probs\/bibliography.html."},{"issue":"2","key":"2_CR19","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1137\/0213021","volume":"13","author":"M. Sharir","year":"1984","unstructured":"M. Sharir, A. Pnueli, and S. Hart. Verification of probabilistic programs. SIAM Journal on Computing, 13(2):292\u2013314, May 1984.","journal-title":"SIAM Journal on Computing"},{"key":"2_CR20","unstructured":"P. Whittle. Probability via expectations. Wiley, second edition, 1980."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T16:34:53Z","timestamp":1556382893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}