P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols.

Liveness of many probabilistic parameterized protocols are proven by first crafting a family of sequences of "good" random draws, thus, in effect "de-probabilizing" the system, and then proving the system just as one would for a non-probabilistic parameterized system. The family of "good" random draws (known in different names, such as "planner" and "strategy") is often an intricate piece of machinery, arising from the need to reason about a parameterized Markov Decision Process (MDP). In effect, it represents a parameterized strategy for an infinite game played between a probabilistic player and a non-deterministic adversary. We present a novel approach to the problem that avoids the need to de-probabilize the system. First, we abstract the parameterized MDP to a finite MDP. The probabilistic choices of this abstraction are drawn not from an independent identically distributed random variable, but instead from a parameterized Markov chain. That is, the distribution of the random variable at any time is dependent on its history and also on the system's parameters. Then, we prove properties about infinite behaviors of the Markov chain and transfer these to the finite MDP. At this point, the proof can be completed by ordinary finite-state model checking. By using abstraction to separate parameterization from nondeterminism, we eliminate the parameterized game and avoid the need for a planner.