Abstract
Randomization is of paramount importance in practical applications and randomized algorithms are used widely, for example in co-ordinating distributed computer networks, message routing and cache management. The appeal of randomized algorithms is their simplicity and elegance. However, this comes at a cost: the analysis of such systems become very complex, particularly in the context of distributed computation. This arises through the interplay between probability and nondeterminism. To prove a randomized distributed algorithm correct one usually involves two levels: classical, assertion-based reasoning, and a probabilistic analysis based on a suitable probability space on computations. In this paper we describe a number of approaches which allows us to verify the correctness of randomized distributed algorithms.
Supported in part by the EPSRC grant GR/N22960.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aggarwal, S., Kutten, S.: Time-optimal self stabilizing spanning tree algorithms. In: Shyamasundar, R. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 15–17. Springer, Heidelberg (1993)
Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Albert, J., Monien, B., Rodrf́8guez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115–136. Springer, Heidelberg (1991)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993)
Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design 15, 7–48 (1999)
Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms 11(3), 441–460 (1990)
Baier, C., Huth, M., Kwiatkowska, M., Ryan, M. (eds.): Proc. Int. Workshop Probabilistic Methods in Verification (PROBMIV 1998). ENTCS, vol. 22. Elsevier Science, Amsterdam (1998)
Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing 11, 125–155 (1998)
Ben-Or, M.: Another advantage of free choice: Completely asynchronous agreement protocols. In: Proc. Symp. Principles of Distributed Computing (PODC 1983), pp. 27–30. ACM Press, New York (1983)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Cachin, C., Kursawe, K., Petzold, F., Shoup, V.: Secure and efficient asynchronous broadcast protocols. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 524–541. Springer, Heidelberg (2001)
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–132. ACM Press, New York (2000)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Cleaveland, R., Smolka, S., Zwarico, A.: Testing preorders for probabilistic processes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 708–719. Springer, Heidelberg (1992)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
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–252. ACM Press, New York (1977)
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. 2. CSREA Press (2000)
D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Alfaro, Gilmore [24], pp. 39–56
D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic anylsis. In :Hermanns, Segala [42], pp. 57–76
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. 66(2). Elsevier Science, Amsterdam (2002)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)
de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol. 1200, pp. 165–176. Springer, Heidelberg (1997)
de Alfaro,L.: From fairness to chance. In: Baier et al. [6]
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–465. IEEE Computer Society Press, Los Alamitos (1998)
de Luca, L., Gilmore, S. (eds.): PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165. Springer, Heidelberg (2001)
de Alfaro, L., Henzinger, T., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen and Nielsen [60], pp. 351–365
Derman, C.: Finite-State Markovian Decision Processes. Academic Press, New York (1970)
Dijkstra, E.: A Discipine of Programming. Prentice Hall International, Englewood Cliffs (1976)
Dolev, S., Israeli, A., Moran, S.: Analyzing expected time by scheduler-luck games. IEEE Transactions on Software Engineering 21(5), 429–439 (1995)
Duflot, M., Fribourg, L., Picaronny, C.: Randomized finite-state distributed algorithms as markov chains. In: Welch, J. (ed.) DISC 2001. LNCS, vol. 2180, pp. 240–254. Springer, Heidelberg (2001)
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. 223, pp. 169–180. Kluwer Academic, Dordrecht (2002)
Failures divergence refinement (FDR2). Formal Systems (Europe) Limited, http://www.formal.demon.co.uk/FDR2.html
Feller, W.: An Introduction to Probability Theory and its Applications, vol. 1. John Wiley & Sons, Chichester (1950)
Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32(5), 374–382 (1985)
Folegati, K., Segala, R.: Coin lemmas with random variables. In: de Alfaro, Gilmore [24], pp. 71–86
Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)
Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proc. Real-Time Systems Symposium, pp. 278–287. IEEE Computer Society Press, Los Alamitos (1990)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(4), 512–535 (1994)
Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. ACM Transactions on Programming Languages and Systems 5(3), 356–380 (1983); A preliminary version appeared. In: Proc. ACM Symp. Principles of Programming Languages, pp. 1–6 (1982)
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–406. IEEE Computer Society Press, Los Alamitos (1992)
Henzinger, T., Qadeer, S., Rajamani, S.: You assume, we guarantee: Methodology and case studies. In: Hu, A., Vardi, M. (eds.) CAV 1998. LNCS, vol. 1427, pp. 440–451. Springer, Heidelberg (1998)
Herman, T.: Probabilistic self stabilisation. Information Processing Letters 35(2), 63–67 (1990)
Hermanns, H., Segala, R.: PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399. Springer, Heidelberg (2002)
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–238 (2001)
Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. Symp. Logic in Computer Science LICS 1997, pp. 111–122. IEEE Computer Society Press, Los Alamitos (1997)
IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394–1995 (August 1996)
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–131. ACM Press, New York (1990)
Jonnsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proc. Symp. Logic in Computer Science LICS 1991, pp. 266–277. IEEE Computer Society Press, Los Alamitos (1991)
Jonsson, B., Parrow, J. (eds.): CONCUR 1994. LNCS, vol. 836. Springer, Heidelberg (1994)
Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstone of practical formal verification. Software Tools for Technology Transfer 4(2), 328–342 (2000)
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. 2421, pp. 101–115. Springer, Heidelberg (2002)
Kushilevitz, E., Rabin, M.: Randomized mutual exclusion algorithm revisited. In: PODC 1992 [80] pp. 275–284
Kwiatkowska, M., Norman, G.: Verifying randomized Byzantine agreement. In: Peled, D., Vardi, M. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 194–209. Springer, Heidelberg (2002)
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. 2324, pp. 200–204. Springer, Heidelberg (2002)
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. 2102, pp. 194–206. Springer, Heidelberg (2001)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 101–150 (2002)
Kwiatkowska, M., Norman, G., Sproston, J.: Symbolic computation of maximal probabilistic reachability. In: Larsen, Nielsen [60], pp. 169–183
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)
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–187
Larsen, K., Nielsen, M. (eds.): CONCUR 2001. LNCS, vol. 2154. Springer, Heidelberg (2001)
Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94(1), 1–28 (1991); Preliminary version of this paper appeared. In: Proc. 16th Annual ACM Symposium on Principles of Programming Languages, pp. 134–352 (1989)
Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: Hermanns, Segala [42], pp. 213–214
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–138. ACM Press, New York (1981)
Lowe, G.: Probabilities and Priorities in Timed CSP. PhD thesis, Oxford University Computing Laboratory (1993)
Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes. Technical Report PRG-TR-11-93, Oxford University Computing Laboratory (1993)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Lynch, N., Saias, I., Segala, R.: Proving time bounds for randomized distributed algorithms. In: Proc. Symp. Principles of Distributed Computing PODC 1994, pp. 314–323. ACM Press, New York (1994)
McIver, A.: Quantitative program logic and expected time bounds in probabilistic distributed algorithms. Theoretical Computer Science 282, 191–219 (2002)
McIver, A., Morgan, C.: An expectation-based model for probabilistic temporal logic. Logic Journal of the IGPL 7(6), 779–804 (1999)
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–265. Springer, Heidelberg (1998)
McMillan, K.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219–237. Springer, Heidelberg (1999)
McMillan, K.: A methodology for hardware verification using compositional model checking. Science of Computer Programming 37(1–3), 279–309 (2000)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Morgan, C., McIver, A.: pGL: Formal reasoning for randomized distributed algorithms. South African Computer Journal, 14–27 (1999)
Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)
Morgan, C., McIver, A., Seidel, K., Sanders, J.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)
Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing 1(1), 53–72 (1986)
Pnueli, A., Zuck, L.: Probabilistic verification. Information and Computation 103, 1–29 (1993)
Proc. Symp. Principles of Distributed Computing (PODC 1992). ACM Press, New York (1992)
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)
Pogosyants, A., Segala, R., Lynch, N.: Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing 13(3), 155–186 (2000)
PRISM web page, http://www.cs.bham.ac.uk/~dxp/prism/
Rabin, M.: N-process mutual exclusion with bounded waiting by 4 log2 N-valued shared variable. Journal of Computer and System Sciences 25(1), 66–75 (1982)
Rabin, M.O.: Probabilistic algorithms. In: Traub, J. (ed.) Algorithms and Complexity: New Directions and Recent Results, pp. 21–39. Academic Press, New York (1976)
RAPTURE web page, http://www.irisa.fr/prive/bjeannet/prob/prob.html
Reiter, M., Rubin, A.: Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security (TISSEC) 1(1), 66–92 (1998)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Saias, A.: Randomness versus Non-Determinism in Distributed Computing. PhD thesis, Massachusetts Institute of Technology (1994)
Saias, I.: Proving probabilistic correctness statements: the case of Rabin’s algorithm for mutual exclusion. In: Proc. Symp. Principles of Distributed Computing PODC 1992, pp. 263–274 (1992)
Segala, R.: Modelling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Segala, R., Baier, et al.: The essence of coin lemmas
Segala, R.: Verification of randomized distributed algorithms. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 232–260. Springer, Heidelberg (2001)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, Parrow [49], pp. 481–496
Shmatikov, V.: Probabilistic analysis of anonymity. In: Proc. Computer Security Foundations Workshop CSFW 2002, pp. 119–128. IEEE Computer Society Press, Los Alamitos (2002)
Shoup, V.: Practical threshold signatures. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 207–220. Springer, Heidelberg (2000)
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)
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–24 (1999)
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–477. IEEE Computer Society Press, Los Alamitos (1988)
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. 1601, pp. 53–74. Springer, Heidelberg (1999)
Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proc. Symp. Foundations of Computer Science FOCS 1985, pp. 327–338. IEEE Computer Society Press, Los Alamitos (1985)
Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. Symp. Logic in Computer Science LICS 1986, pp. 332–344. IEEE Computer Society Press, Los Alamitos (1986)
Wu, S.-H., Smolka, S.A., Stark, E.W.: Composition and behaviour of probabilistic I/O automata. In: Jonsson, Parrow [49], pp. 513–528
Yi, W., Larsen, K.G.: Testing probabilistic and non-deterministic processes. In: Linn Jr., R., Ümit Uyar, M. (eds.) Protocol Specification, Testing and Verification. IFIP Transactions, vol. C-8, pp. 47–61. North-Holland, Amsterdam (1992)
Zuck, L., Pnueli, A., Kesten, Y.: Automatic verification of probabilistic free choice. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 208–224. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Norman, G. (2004). Analysing Randomized Distributed Algorithms . In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, JP., Siegle, M. (eds) Validation of Stochastic Systems. Lecture Notes in Computer Science, vol 2925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24611-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-24611-4_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22265-1
Online ISBN: 978-3-540-24611-4
eBook Packages: Springer Book Archive