Model Checking Concurrent Programs With Nondeterminism and Randomization
The use of randomization in concurrent or distributed systems is often key to achieving certain objectives - it is used in distributed algorithms to break symmetry and in cryptographic protocols to achieve semantic security. The formal analysis of such systems has often modelled them as Markov Decision Processes, that has both nondeterministic and probabilistic transitions. In Markov Decision Processes (MDPs), the probability of events depends on the way the nondeterministic choices are resolved during a computation. It is customary to resolve the non-determinism by a scheduler or adversary, who chooses a probabilistic transition from a state based on the past sequence of states visited during the computation.