Coin Lemmas with Random Variables
- 294 Downloads
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.
KeywordsRoot Function Label Transition System Probabilistic Automaton General Stochastic Process Binary Experiment
Unable to display preview. Download preview PDF.
- 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.C. Derman. Finite State Markovian Decision Processes. Academic Press, 1970.Google Scholar
- 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.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.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.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.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
- 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.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.R. Segala. The essence of coin lemmas. In Proceedings of PROBMIV’98, volume 22 of Electronic Notes in Theoretical Computer Science, 1999.Google Scholar