{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T09:38:17Z","timestamp":1777541897414,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":106,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540222651","type":"print"},{"value":"9783540246114","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24611-4_11","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T19:01:10Z","timestamp":1267124470000},"page":"384-418","source":"Crossref","is-referenced-by-count":21,"title":["Analysing Randomized Distributed Algorithms"],"prefix":"10.1007","author":[{"given":"Gethin","family":"Norman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","first-page":"15","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"S. Aggarwal","year":"1993","unstructured":"Aggarwal, S., Kutten, S.: Time-optimal self stabilizing spanning tree algorithms. In: Shyamasundar, R. (ed.) FSTTCS 1993. LNCS, vol.\u00a0761, pp. 15\u201317. Springer, Heidelberg (1993)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Albert, J., Monien, B., Rodrf\u03018guez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 115\u2013136. Springer, Heidelberg (1991)"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information and Computation"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design\u00a015, 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a011(3), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"key":"11_CR6","series-title":"ENTCS","volume-title":"Proc. Int. Workshop Probabilistic Methods in Verification (PROBMIV 1998)","year":"1998","unstructured":"Baier, C., Huth, M., Kwiatkowska, M., Ryan, M. (eds.): Proc. Int. Workshop Probabilistic Methods in Verification (PROBMIV 1998). ENTCS, vol.\u00a022. Elsevier Science, Amsterdam (1998)"},{"key":"11_CR7","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011, 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1145\/800221.806707","volume-title":"Proc. Symp. Principles of Distributed Computing (PODC 1983)","author":"M. Ben-Or","year":"1983","unstructured":"Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols. In: Proc. Symp. Principles of Distributed Computing (PODC 1983), pp. 27\u201330. ACM Press, New York (1983)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/3-540-44647-8_31","volume-title":"Advances in Cryptology - CRYPTO 2001","author":"C. Cachin","year":"2001","unstructured":"Cachin, C., Kursawe, K., Petzold, F., Shoup, V.: Secure and efficient asynchronous broadcast protocols. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol.\u00a02139, pp. 524\u2013541. Springer, Heidelberg (2001)"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/343477.343531","volume-title":"Proc. Symp. Principles of Distributed Computing (PODC 2000)","author":"C. Cachin","year":"2000","unstructured":"Cachin, C., Kursawe, K., Shoup, V.: Random oracles in Constantinople: practical asynchronous Byzantine agreement using cryptography (extended abstract). In: Proc. Symp. Principles of Distributed Computing (PODC 2000), pp. 123\u2013132. ACM Press, New York (2000)"},{"key":"11_CR12","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"708","DOI":"10.1007\/3-540-55719-9_116","volume-title":"Automata, Languages and Programming","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., Smolka, S., Zwarico, A.: Testing preorders for probabilistic processes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 708\u2013719. Springer, Heidelberg (1992)"},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"11_CR15","first-page":"238","volume-title":"Proc. Symp. Principles of Programming Languages (POPL1977)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. Symp. Principles of Programming Languages (POPL1977), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"11_CR16","unstructured":"Creese, S., Roscoe, A.: Data independent induction over structured networks. In: Arabnia, H. (ed.) Proc. Int. Conf. Parallel and Distributed Processing Techniques and Applications PDPTA 2000, vol.\u00a02. CSREA Press (2000)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, Gilmore [24], pp. 39\u201356","DOI":"10.1007\/3-540-44804-7_3"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic anylsis. In :Hermanns, Segala [42], pp. 57\u201376","DOI":"10.1007\/3-540-45605-8_5"},{"key":"11_CR19","series-title":"ENTCS","volume-title":"Proc. Int. Workshop Formal Methods for Industrial Critical Systems (FMICS 2002)","author":"C. Daws","year":"2002","unstructured":"Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. In: Proc. Int. Workshop Formal Methods for Industrial Critical Systems (FMICS 2002). ENTCS, vol.\u00a066(2). Elsevier Science, Amsterdam (2002)"},{"key":"11_CR20","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BFb0023457","volume-title":"STACS 97","author":"L. Alfaro de","year":"1997","unstructured":"de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 165\u2013176. Springer, Heidelberg (1997)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"de Alfaro,L.: From fairness to chance. In: Baier et al. [6]","DOI":"10.1016\/S1571-0661(05)80597-3"},{"key":"11_CR23","first-page":"454","volume-title":"Proc. Symp. Logic in Computer Science (LICS 1998)","author":"L. Alfaro de","year":"1998","unstructured":"de Alfaro, L.: How to specify and verify the long-run average behaviour of probabilistic systems. In: Proc. Symp. Logic in Computer Science (LICS 1998), pp. 454\u2013465. IEEE Computer Society Press, Los Alamitos (1998)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV 2001)","year":"2001","unstructured":"de Luca, L., Gilmore, S. (eds.): PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165. Springer, Heidelberg (2001)"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen and Nielsen [60], pp. 351\u2013365","DOI":"10.1007\/3-540-44685-0_24"},{"key":"11_CR26","volume-title":"Finite-State Markovian Decision Processes","author":"C. Derman","year":"1970","unstructured":"Derman, C.: Finite-State Markovian Decision Processes. Academic Press, New York (1970)"},{"key":"11_CR27","volume-title":"A Discipine of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipine of Programming. Prentice Hall International, Englewood Cliffs (1976)"},{"issue":"5","key":"11_CR28","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1109\/32.387472","volume":"21","author":"S. Dolev","year":"1995","unstructured":"Dolev, S., Israeli, A., Moran, S.: Analyzing expected time by scheduler-luck games. IEEE Transactions on Software Engineering\u00a021(5), 429\u2013439 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-45414-4_17","volume-title":"Distributed Computing","author":"M. Duflot","year":"2001","unstructured":"Duflot, M., Fribourg, L., Picaronny, C.: Randomized finite-state distributed algorithms as markov chains. In: Welch, J. (ed.) DISC 2001. LNCS, vol.\u00a02180, pp. 240\u2013254. Springer, Heidelberg (2001)"},{"key":"11_CR30","series-title":"IFIP Conference Proceedings","first-page":"169","volume-title":"Proc. IFIP Int. Conf. Theoretical Computer Science TCS 2002","author":"M. Duflot","year":"2002","unstructured":"Duflot, M., Fribourg, L., Picaronny, C.: Randomized dining philosophers without fairness assumption. In: Proc. IFIP Int. Conf. Theoretical Computer Science TCS 2002. IFIP Conference Proceedings, vol.\u00a0223, pp. 169\u2013180. Kluwer Academic, Dordrecht (2002)"},{"key":"11_CR31","unstructured":"Failures divergence refinement (FDR2). Formal Systems (Europe) Limited, http:\/\/www.formal.demon.co.uk\/FDR2.html"},{"key":"11_CR32","volume-title":"An Introduction to Probability Theory and its Applications","author":"W. Feller","year":"1950","unstructured":"Feller, W.: An Introduction to Probability Theory and its Applications, vol.\u00a01. John Wiley & Sons, Chichester (1950)"},{"issue":"5","key":"11_CR33","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M. Fischer","year":"1985","unstructured":"Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. Journal of the ACM\u00a032(5), 374\u2013382 (1985)","journal-title":"Journal of the ACM"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Folegati, K., Segala, R.: Coin lemmas with random variables. In: de Alfaro, Gilmore [24], pp. 71\u201386","DOI":"10.1007\/3-540-44804-7_5"},{"key":"11_CR35","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"H. Hansson","year":"1994","unstructured":"Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)"},{"key":"11_CR36","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1109\/REAL.1990.128759","volume-title":"Proc. Real-Time Systems Symposium","author":"H. Hansson","year":"1990","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proc. Real-Time Systems Symposium, pp. 278\u2013287. IEEE Computer Society Press, Los Alamitos (1990)"},{"issue":"4","key":"11_CR37","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(4), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"3","key":"11_CR38","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.: Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems 5(3), 356\u2013380 (1983); A preliminary version appeared. In: Proc. ACM Symp. Principles of Programming Languages, pp. 1\u20136 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR39","first-page":"394","volume-title":"Proc. Symp. Logic in Computer Science (LICS 1998)","author":"T. Henzinger","year":"1992","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: Proc. Symp. Logic in Computer Science (LICS 1998), pp. 394\u2013406. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BFb0028765","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"1998","unstructured":"Henzinger, T., Qadeer, S., Rajamani, S.: You assume, we guarantee: Methodology and case studies. In: Hu, A., Vardi, M. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 440\u2013451. Springer, Heidelberg (1998)"},{"issue":"2","key":"11_CR41","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T. Herman","year":"1990","unstructured":"Herman, T.: Probabilistic self stabilisation. Information Processing Letters\u00a035(2), 63\u201367 (1990)","journal-title":"Information Processing Letters"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45605-8","volume-title":"Proc. Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification PAPM\/PROBMIV 2002","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H., Segala, R.: PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399. Springer, Heidelberg (2002)"},{"key":"11_CR43","unstructured":"Hurd, J.: Verification of the Miller-Rabin probabilistic primality test. In: Boulton, R., Jackson, P. (eds.) TPHOLs 2001: Supplemental Proceedings, number EDI-INF-RR-0046 in Informatics Report Series, Division of Informatics, University of Edinburgh, pp. 223\u2013238 (2001)"},{"key":"11_CR44","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)"},{"key":"11_CR45","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1109\/LICS.1997.614940","volume-title":"Proc. Symp. Logic in Computer Science LICS 1997","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. Symp. Logic in Computer Science LICS 1997, pp. 111\u2013122. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"11_CR46","unstructured":"IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394\u20131995 (August 1996)"},{"key":"11_CR47","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1145\/93385.93409","volume-title":"Proc. Symp. Principles of Distributed Computing PODC 1990","author":"A. Israeli","year":"1990","unstructured":"Israeli, A., Jalfon, M.: Token management schemes and random walks yield selfstabilizing mutual exclusion. In: Proc. Symp. Principles of Distributed Computing PODC 1990, pp. 119\u2013131. ACM Press, New York (1990)"},{"key":"11_CR48","first-page":"266","volume-title":"Proc. Symp. Logic in Computer Science LICS 1991","author":"B. Jonnsson","year":"1991","unstructured":"Jonnsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. Symp. Logic in Computer Science LICS 1991, pp. 266\u2013277. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"11_CR49","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 1994: Concurrency Theory","year":"1994","unstructured":"Jonsson, B., Parrow, J. (eds.): CONCUR 1994. LNCS, vol.\u00a0836. Springer, Heidelberg (1994)"},{"issue":"2","key":"11_CR50","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstone of practical formal verification. Software Tools for Technology Transfer\u00a04(2), 328\u2013342 (2000)","journal-title":"Software Tools for Technology Transfer"},{"key":"11_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45694-5_8","volume-title":"CONCUR 2002 - Concurrency Theory","author":"Y. Kesten","year":"2002","unstructured":"Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariants in action. In: Brim, L., Jancar, P., Kretinsky, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 101\u2013115. Springer, Heidelberg (2002)"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Kushilevitz, E., Rabin, M.: Randomized mutual exclusion algorithm revisited. In: PODC 1992 [80] pp. 275\u2013284","DOI":"10.1145\/135419.135468"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-36135-9_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G.: Verifying randomized Byzantine agreement. In: Peled, D., Vardi, M. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 194\u2013209. Springer, Heidelberg (2002)"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"11_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"11_CR56","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282, 101\u2013150 (2002)","journal-title":"Theoretical Computer Science"},{"key":"11_CR57","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic computation of maximal probabilistic reachability. In: Larsen, Nielsen [60], pp. 169\u2013183","DOI":"10.1007\/3-540-44685-0_12"},{"key":"11_CR58","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Special Issue of Formal Aspects of Computing (2002) (to appear)","DOI":"10.1007\/s001650300007"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, Segala [42], pp. 169\u2013187","DOI":"10.1007\/3-540-45605-8_11"},{"key":"11_CR60","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR 2001 - Concurrency Theory","year":"2001","unstructured":"Larsen, K., Nielsen, M. (eds.): CONCUR 2001. LNCS, vol.\u00a02154. Springer, Heidelberg (2001)"},{"key":"#cr-split#-11_CR61.1","doi-asserted-by":"crossref","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094(1), 1\u201328 (1991);","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"#cr-split#-11_CR61.2","unstructured":"Preliminary version of this paper appeared. In: Proc. 16th Annual ACM Symposium on Principles of Programming Languages, pp. 134\u2013352 (1989)"},{"key":"11_CR62","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: Hermanns, Segala [42], pp. 213\u2013214","DOI":"10.1007\/3-540-45605-8_16"},{"key":"11_CR63","first-page":"133","volume-title":"Proc. Symp. on Principles of Programming Languages POPL 1981","author":"D. Lehmann","year":"1981","unstructured":"Lehmann, D., Rabin, M.: On the advantage of free choice: A symmetric and fully distributed solution to the dining philosophers problem (extended abstract). In: Proc. Symp. on Principles of Programming Languages POPL 1981, pp. 133\u2013138. ACM Press, New York (1981)"},{"key":"11_CR64","unstructured":"Lowe, G.: Probabilities and Priorities in Timed CSP. PhD thesis, Oxford University Computing Laboratory (1993)"},{"key":"11_CR65","unstructured":"Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes. Technical Report PRG-TR-11-93, Oxford University Computing Laboratory (1993)"},{"key":"11_CR66","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"11_CR67","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1145\/197917.198117","volume-title":"Proc. Symp. Principles of Distributed Computing PODC 1994","author":"N. Lynch","year":"1994","unstructured":"Lynch, N., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proc. Symp. Principles of Distributed Computing PODC 1994, pp. 314\u2013323. ACM Press, New York (1994)"},{"key":"11_CR68","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/S0304-3975(01)00049-4","volume":"282","author":"A. McIver","year":"2002","unstructured":"McIver, A.: Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Computer Science\u00a0282, 191\u2013219 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"11_CR69","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1093\/jigpal\/7.6.779","volume":"7","author":"A. McIver","year":"1999","unstructured":"McIver, A., Morgan, C.: An expectation-based model for probabilistic temporal logic. Logic Journal of the IGPL\u00a07(6), 779\u2013804 (1999)","journal-title":"Logic Journal of the IGPL"},{"key":"11_CR70","first-page":"250","volume-title":"Proc. Int. Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science","author":"A. McIver","year":"1998","unstructured":"McIver, A., Morgan, C., Troubitsyna, E.: The probabilistic steam boiler: a case study in probabilistic data refinement. In: Grundy, J., Schwenke, M., Vickers, T. (eds.) Proc. Int. Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, pp. 250\u2013265. Springer, Heidelberg (1998)"},{"key":"11_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K. McMillan","year":"1999","unstructured":"McMillan, K.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"issue":"1\u20133","key":"11_CR72","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S0167-6423(99)00030-1","volume":"37","author":"K. McMillan","year":"2000","unstructured":"McMillan, K.: A methodology for hardware verification using compositional model checking. Science of Computer Programming\u00a037(1\u20133), 279\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"11_CR73","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"11_CR74","unstructured":"Morgan, C., McIver, A.: pGL: Formal reasoning for randomized distributed algorithms. South African Computer Journal, 14\u201327 (1999)"},{"issue":"3","key":"11_CR75","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems\u00a018(3), 325\u2013353 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"6","key":"11_CR76","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/BF01213492","volume":"8","author":"C. Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K., Sanders, J.: Refinement-oriented probability for CSP. Formal Aspects of Computing\u00a08(6), 617\u2013647 (1996)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR77","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R. Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"issue":"1","key":"11_CR78","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing\u00a01(1), 53\u201372 (1986)","journal-title":"Distributed Computing"},{"key":"11_CR79","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.: Probabilistic verification. Information and Computation\u00a0103, 1\u201329 (1993)","journal-title":"Information and Computation"},{"key":"11_CR80","unstructured":"Proc. Symp. Principles of Distributed Computing (PODC 1992). ACM Press, New York (1992)"},{"key":"11_CR81","volume-title":"Proc. Symp. Principles of Distributed Computing PODC 1995","author":"A. Pogosyants","year":"1995","unstructured":"Pogosyants, A., Segala, R.: Formal verification of timed properties of randomized distributed algorithms. In: Proc. Symp. Principles of Distributed Computing PODC 1995. ACM Press, New York (1995)"},{"issue":"3","key":"11_CR82","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/PL00008917","volume":"13","author":"A. Pogosyants","year":"2000","unstructured":"Pogosyants, A., Segala, R., Lynch, N.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing\u00a013(3), 155\u2013186 (2000)","journal-title":"Distributed Computing"},{"key":"11_CR83","unstructured":"PRISM web page, http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"},{"issue":"1","key":"11_CR84","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1016\/0022-0000(82)90010-1","volume":"25","author":"M. Rabin","year":"1982","unstructured":"Rabin, M.: N-process mutual exclusion with bounded waiting by 4 log2 N-valued shared variable. Journal of Computer and System Sciences\u00a025(1), 66\u201375 (1982)","journal-title":"Journal of Computer and System Sciences"},{"key":"11_CR85","first-page":"21","volume-title":"Algorithms and Complexity: New Directions and Recent Results","author":"M.O. Rabin","year":"1976","unstructured":"Rabin, M.O.: Probabilistic algorithms. In: Traub, J. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 21\u201339. Academic Press, New York (1976)"},{"key":"11_CR86","unstructured":"RAPTURE web page, http:\/\/www.irisa.fr\/prive\/bjeannet\/prob\/prob.html"},{"issue":"1","key":"11_CR87","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M. Reiter","year":"1998","unstructured":"Reiter, M., Rubin, A.: Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security (TISSEC)\u00a01(1), 66\u201392 (1998)","journal-title":"ACM Transactions on Information and System Security (TISSEC)"},{"key":"11_CR88","volume-title":"The Theory and Practice of Concurrency","author":"A. Roscoe","year":"1997","unstructured":"Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"11_CR89","unstructured":"Saias, A.: Randomness versus Non-Determinism in Distributed Computing. PhD thesis, Massachusetts Institute of Technology (1994)"},{"key":"11_CR90","doi-asserted-by":"crossref","unstructured":"Saias, I.: Proving probabilistic correctness statements: the case of Rabin\u2019s algorithm for mutual exclusion. In: Proc. Symp. Principles of Distributed Computing PODC 1992, pp. 263\u2013274 (1992)","DOI":"10.1145\/135419.135466"},{"key":"11_CR91","unstructured":"Segala, R.: Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)"},{"key":"11_CR92","unstructured":"Segala, R., Baier, et al.: The essence of coin lemmas"},{"key":"11_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-44667-2_6","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"R. Segala","year":"2001","unstructured":"Segala, R.: Verification of randomized distributed algorithms. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol.\u00a02090, pp. 232\u2013260. Springer, Heidelberg (2001)"},{"key":"11_CR94","doi-asserted-by":"crossref","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, Parrow [49], pp. 481\u2013496","DOI":"10.1007\/BFb0015027"},{"key":"11_CR95","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1109\/CSFW.2002.1021811","volume-title":"Proc. Computer Security Foundations Workshop CSFW 2002","author":"V. Shmatikov","year":"2002","unstructured":"Shmatikov, V.: Probabilistic analysis of anonymity. In: Proc. Computer Security Foundations Workshop CSFW 2002, pp. 119\u2013128. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"11_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-45539-6_15","volume-title":"Advances in Cryptology - EUROCRYPT 2000","author":"V. Shoup","year":"2000","unstructured":"Shoup, V.: Practical threshold signatures. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol.\u00a01807, pp. 207\u2013220. Springer, Heidelberg (2000)"},{"key":"11_CR97","unstructured":"Speed, T.: Probabilistic risk assessment in the nuclear industry: WASH-1400 and beyond. In: LeCam, L., Olshen, R. (eds.) Proc. Berkeley Conference in honour of Jerzy Neyman and Jack Kiefer, Wadsworth Inc. (1985)"},{"key":"11_CR98","unstructured":"Stark, E., Pemmasani, G.: Implementation of a compositional performance analysis algorithm for probabilistic I\/O automata. In: Hillston, J., Silva, M. (eds.) Proc. Int. Workshop Process Algebra and Performance Modelling PAPM 1999, Prensas Universitarias de Zaragoza, pp. 3\u201324 (1999)"},{"key":"11_CR99","first-page":"466","volume-title":"Proc. Symp. Logic in Computer Science LICS 1998","author":"E. Stark","year":"1988","unstructured":"Stark, E., Smolka, S.: Compositional analysis of expected delays in networks of probabilistic I\/O automata. In: Proc. Symp. Logic in Computer Science LICS 1998, pp. 466\u2013477. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"11_CR100","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-48778-6_4","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"M. Stoelinga","year":"1999","unstructured":"Stoelinga, M., Vaandrager, F.: Root contention in IEEE 1394. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 53\u201374. Springer, Heidelberg (1999)"},{"key":"11_CR101","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1109\/SFCS.1985.12","volume-title":"Proc. Symp. Foundations of Computer Science FOCS 1985","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proc. Symp. Foundations of Computer Science FOCS 1985, pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"},{"key":"11_CR102","first-page":"332","volume-title":"Proc. Symp. Logic in Computer Science LICS 1986","author":"M. Vardi","year":"1986","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. Symp. Logic in Computer Science LICS 1986, pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"11_CR103","doi-asserted-by":"crossref","unstructured":"Wu, S.-H., Smolka, S.A., Stark, E.W.: Composition and behaviour of probabilistic I\/O automata. In: Jonsson, Parrow [49], pp. 513\u2013528","DOI":"10.1007\/BFb0015029"},{"key":"11_CR104","series-title":"IFIP Transactions","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/B978-0-444-89874-6.50010-6","volume-title":"Protocol Specification, Testing and Verification","author":"W. Yi","year":"1992","unstructured":"Yi, W., Larsen, K.G.: Testing probabilistic and non-deterministic processes. In: Linn Jr., R., \u00dcmit Uyar, M. (eds.) Protocol Specification, Testing and Verification. IFIP Transactions, vol.\u00a0C-8, pp. 47\u201361. North-Holland, Amsterdam (1992)"},{"key":"11_CR105","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.\u00a02294, pp. 208\u2013224. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Validation of Stochastic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24611-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T11:46:38Z","timestamp":1558871198000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24611-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540222651","9783540246114"],"references-count":106,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24611-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}