Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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.
C. Derman. Finite State Markovian Decision Processes. Academic Press, 1970.
H. Hansson. Time and Probability in Formal Design of Distributed Systems, volume 1 of Real-Time Safety Critical Systems. Elsevier, 1994.
J.G. Kemeny, J.L. Snell, and A.W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer-Verlag, second edition, 1976.
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.
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.
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.
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.
M.O. Rabin. Probabilistic automata. Information and Control, 6:230–245, 1963.
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.
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.
R. Segala. The essence of coin lemmas. In Proceedings of PROBMIV’98, volume 22 of Electronic Notes in Theoretical Computer Science, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Folegati, K., Segala, R. (2001). Coin Lemmas with Random Variables. In: de Alfaro, L., Gilmore, S. (eds) Process Algebra and Probabilistic Methods. Performance Modelling and Verification. PAPM-PROBMIV 2001. Lecture Notes in Computer Science, vol 2165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44804-7_5
Download citation
DOI: https://doi.org/10.1007/3-540-44804-7_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42556-4
Online ISBN: 978-3-540-44804-4
eBook Packages: Springer Book Archive