Reducing Probabilistic Choice to Nondeterministic Choice

Okay, this isn’t really semantics, just a simple way to use ordinary invariants to reason about probabilistic transition systems (or programs). The trick is to to prove invariants of the form M + L >= 0, where L (“luck”) is a linear combination of “gambling balance” ghost variables that are initially 0 and are only updated with (state-dependent) fair bets on probabilistic choices. Since the expected value of luck is 0, this implies that the expected value of M is always nonnegative.

This entry was posted in Uncategorized. Bookmark the permalink.