Coin Lemmas with Random Variables

  • Katia Folegati
  • Roberto Segala
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


Coin lemmas are a tool for decoupling probabilistic and non-deterministic arguments in the analysis of concurrent probabilistic systems. They have revealed to be fundamental in the analysis of randomized distributed algorithms, where the interplay between probability and nondeterminism has proved to be subtle and difficult to handle.

We reformulate coin lemmas in terms of random variables obtaining a newcollection of coin lemmas that is independent of the underlying computational model and of more general applicability to the study of concurrent nondeterministic probabilistic systems.


Root Function Label Transition System Probabilistic Automaton General Stochastic Process Binary Experiment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Ben-Or. Another advantage of free choice: completely asynchronous agreement protocols. In Proceedings of the 2 nd Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 1983.Google Scholar
  2. 2.
    C. Derman. Finite State Markovian Decision Processes. Academic Press, 1970.Google Scholar
  3. 3.
    H. Hansson. Time and Probability in Formal Design of Distributed Systems, volume 1 of Real-Time Safety Critical Systems. Elsevier, 1994.Google Scholar
  4. 4.
    J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer-Verlag, second edition, 1976.Google Scholar
  5. 5.
    K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. In Conference Record of the 16 th ACM Symposium on Principles of Programming Languages, Austin, Texas, pages 344–352, 1989.Google Scholar
  6. 6.
    D. Lehmann and M. Rabin. On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8 th Annual ACM Symposium on Principles of Programming Languages, pages 133–138, January 1981.Google Scholar
  7. 7.
    A. Pogosyants and R. Segala. Formal verification of timed properties of randomized distributed algorithms. In Proceedings of the 14 th Annual ACM Symposium on Principles of Distributed Computing, pages 174–183, August 1995.Google Scholar
  8. 8.
    A. Pogosyants, R. Segala, and N. Lynch. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing, 13:155–186, July 2000.CrossRefGoogle Scholar
  9. 9.
    M.O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963.CrossRefGoogle Scholar
  10. 10.
    I. Saias. Proving probabilistic correctness: the case of Rabin’s algorithm for mutual exclusion. In Proceedings of the 11 th Annual ACM Symposium on Principles of Distributed Computing, Quebec, Canada, August 1992.Google Scholar
  11. 11.
    R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Dept. of Electrical Engineering and Computer Science, 1995. Also appears as technical report MIT/LCS/TR-676.Google Scholar
  12. 12.
    R. Segala. The essence of coin lemmas. In Proceedings of PROBMIV’98, volume 22 of Electronic Notes in Theoretical Computer Science, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Katia Folegati
    • 1
  • Roberto Segala
    • 1
  1. 1.Department of Computer ScienceUniversity of BolognaItaly

Personalised recommendations