Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering (FOSE 2014). ACM, New York, NY, USA, 167-181. DOI=10.1145/2593882.2593900 doi.acm.org/10.1145/2593882.2593900

"This simple probabilistic algorithm due to Knuth and Yao [KY76]. for emulating a 6-sided die with a fair coin. The idea of the algorithm is as follows. Starting from step 0 (i.e. the circle labelled 0), at every step a coin is tossed and there is 50% chance of taking each of the two possible choices. The algorithm terminates when you reach one of the values for the die on the right-hand side" (PRISM-Tutorial)

"The DTMC-graph (left) shows an example with 13 vertices. The DTMC implements the Knuth-Yao algorithm for obtaining a fair die from fair coin tosses. It turns out that the steady state probability pi(v) for each of the vertices 11 through 16 is 1/6 and for each of the other vertices is 0. Every DTMC can be encoded as a probabilistic program. Cycles in the DTMC graph can be encoded using while-loops in the probabilistic program.

Unlike the semantics we have given for probabilistic programs, which considers terminating runs (which are finite), the semantics of DTMCs inherently considers infinite runs. However, in cases where every terminal SCC (strongly-connected component) of a DTMC is a singleton vertex (which is the case, here), we can terminate the execution of the probabilistic program on reaching the terminal SCC..." (Gordon et al., 2014).