Coin Lemmas with Random Variables
Author: K. Folegati, R. Segala
Appears: in Proceedings of the First Joint Workshop on Process Algebra and Performance Modelling, Probabilistic Methods in Verification, Aachen, Germany, LNCS 2165, pages 71-86, September 2001.
Abstract: Coin lemmas are a tool for decoupling probabilistic and nondeterministic 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 new collection of coin lemmas that is independent of the underlying computational model and of more general applicability to the study of concurrent nondeterministic probabilistic systems.