Flooded fens

The goal of this research is to demonstrate that probabilistic algorithms can be formally verified just like deterministic ones.

Approach

The key idea is to model a random number generator with an infinite sequence of bits; functions explicitly pass around this sequence as an extra parameter. When the algorithm needs to make a random choice, it pulls some bits off the sequence, and passes on the rest of the sequence. The question "What is the probability that this algorithm does X?" then becomes "What set of infinite bit sequences cause the algorithm to do X?" A formalization of mathematical measure theory is used to assign sets of infinite bit sequences a probability between 0 and 1.

Case Studies

This approach has been used to verify:

  • sampling algorithms for four probability distributions;
  • some optimal procedures for generating dice rolls from coin flips;
  • the symmetric simple random walk; and
  • the Miller-Rabin probabilistic primality test.

The algorithm that generates dice rolls from coin flips belongs to an interesting class that is not guaranteed to terminate, but nevertheless terminates with probability 1. For a simple example of this phenomenon consider repeatedly flipping a coin and stopping the first time it shows heads: if the coin shows tails forever you will never terminate, but this event occurs with probability 0. Formalizing this concept of probabilistic termination was necessary to verify interesting probabilistic algorithms.

Publications