{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T04:08:27Z","timestamp":1752984507707},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540378730"},{"type":"electronic","value":"9783540378747"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11828563_20","type":"book-chapter","created":{"date-parts":[[2006,10,3]],"date-time":"2006-10-03T06:43:15Z","timestamp":1159857795000},"page":"296-310","source":"Crossref","is-referenced-by-count":16,"title":["Using Probabilistic Kleene Algebra for Protocol Verification"],"prefix":"10.1007","author":[{"given":"A. K.","family":"McIver","sequence":"first","affiliation":[]},{"given":"E.","family":"Cohen","sequence":"additional","affiliation":[]},{"given":"C. C.","family":"Morgan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In Mathematics of Program Construction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"issue":"4","key":"20_CR2","doi-asserted-by":"publisher","first-page":"917","DOI":"10.1145\/153724.153770","volume":"40","author":"J. Halpern","year":"1993","unstructured":"Halpern, J., Tuttle, M.: Knowledge, probabilities and adversaries. J. ACM\u00a040(4), 917\u2013962 (1993)","journal-title":"J. ACM"},{"key":"20_CR3","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"J. He","year":"1997","unstructured":"He, J., Seidel, K., McIver, A.K.: Probabilistic models for the guarded command language. Science of Computer Programming\u00a028, 171\u2013192 (1997); Earlier appeared in Proc. FMTA 1995, Warsaw (May 1995). Available at [9, key HSM 1995]","journal-title":"Science of Computer Programming"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45685-6_16","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"2002","unstructured":"Hurd, J.: A formal approach to probabilistic termination. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, Springer, Heidelberg (2002), \n                  \n                    www.cl.cam.ac.uk\/~jeh1004\/research\/papers"},{"issue":"3","key":"20_CR5","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Kushilevitz, E., Rabin, M.O.: Randomized mutual exclusion algorithms revisited. In: Proc. 11th Annual ACM Symp. on Principles of Distributed Computing (1992)","DOI":"10.1145\/135419.135468"},{"issue":"3","key":"20_CR7","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"Lehmann, D., Shelah, S.: Reasoning with time and chance. Information and Control\u00a053(3), 165\u2013198 (1982)","journal-title":"Information and Control"},{"key":"20_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11591191_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. McIver","year":"2005","unstructured":"McIver, A., Weber, T.: Towards automated proof support for probabilistic distributed systems. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 534\u2013548. Springer, Heidelberg (2005)"},{"key":"20_CR9","unstructured":"McIver, A.K., Morgan, C.C., Sanders, J.W., Seidel, K.: Probabilistic Systems Group: Collected reports, \n                  \n                    http:\/\/web.comlab.ox.ac.uk\/oucl\/research\/areas\/probs"},{"key":"20_CR10","series-title":"Technical Monographs in Computer Science","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A. McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Technical Monographs in Computer Science. Springer, Heidelberg (2004)"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-27764-4_14","volume-title":"Mathematics of Program Construction","author":"B. Moeller","year":"2004","unstructured":"Moeller, B.: Lazy Kleene Algebra. In: Kozen, D., Shankland, C. (eds.) MPC 2004. LNCS, vol.\u00a03125, pp. 252\u2013273. Springer, Heidelberg (2004)"},{"issue":"3","key":"20_CR12","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C.C. Morgan","year":"1996","unstructured":"Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems\u00a018(3), 325\u2013353 (1996), doi.acm.org\/10.1145\/229542.229547","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR13","unstructured":"PRISM. Probabilistic symbolic model checker \n                  \n                    www.cs.bham.ac.uk\/~dxp\/prism"},{"issue":"1","key":"20_CR14","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/0022-0000(82)90010-1","volume":"25","author":"M.O. Rabin","year":"1982","unstructured":"Rabin, M.O.: N-process mutual exclusion with bounded waiting by 4 log 2n-valued shared variable. Journal of Computer and System Sciences\u00a025(1), 66\u201375 (1982)","journal-title":"Journal of Computer and System Sciences"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Saias, I.: Proving probabilistic correctness statements: the case of Rabin\u2019s algorithm for mutual exclusion. In: Proc. 11th Annual ACM Symp. on Principles of Distributed Computing (1992)","DOI":"10.1145\/135419.135466"},{"key":"20_CR16","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT (1995)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11828563_27","volume-title":"Relations and Kleene Algebra in Computer Science","author":"T. Takai","year":"2006","unstructured":"Takai, T., Furusawa, H.: Monadic tree Kleene Algebra. In: Schmidt, R.A. (ed.) RelMiCS\/AKA 2006. LNCS, vol.\u00a04136, Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Relations and Kleene Algebra in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11828563_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:13:17Z","timestamp":1619493197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11828563_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540378730","9783540378747"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11828563_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}