Reconciling nondeterministic and probabilistic choices

This thesis is written in the context of probabilistic verification. Our primary goal is to develop modeling frameworks that can be used for both specification and verification of randomized distributed algorithms. We focus on semantic aspects of such modeling frameworks; for example, we try to give precise mathematical semantics to processes definable in these frameworks and we prove basic theorems that allow us to manipulate and reason with semantic objects. Our models typically allow both nondeterministic and probabilistic choices. In order to obtain well-defined probability distributions from a specification, one must somehow ááuntangle'' these two types of choices. This is usually done by means of adversaries/schedulers, which resolve all nondeterministic choices in a specification. We study mathematical properties of adversaries and try to understand how different definitions of parallel composition translate into different assumptions on the behavior of adversaries. This allows us to identify some key properties of adversaries that affect compositionality of trace-style semantics. We also try to make a connection between the notions of adversaries captured by our formal definitions and those that are actually used in distributed computing,for example, in the areas of security protocols and randomized consensus. This thesis is organized into three parts. In Part I, we work with Segala's Probabilistic Automata model and prove many technical theorems regarding adversaries and their induced probability distributions. These results are then used to extend the testing semantics proposed by Stoelinga and Vaandrager. In Part II, we introduce our own variant of Probabilistic Input/Output Automata and use that as a basis of two specialized models, both of which come with a compositional trace-style semantics. Finally, Part III presents a randomized consensus algorithm, together with a manual correctness proof and a mechanized analysis using the probabilistic model checker PRISM