Compositional verification techniques for probabilistic and nondeterministic models are discussed in this paper. By emphasizing compositionality, the interacting components can be individually verified and the verification of the complete system can then be inferred. Indeed, the main results of the paper are theorems dealing with the ability to compose probabilistic guarantees.

The basic idea is that one checks queries of this form: “Whenever M is part of a system satisfying the assumption A, then the system is guaranteed to satisfy property G. The systems are modeled as probabilistic automata; indeed, the predicates are allowed to be probabilistic. Proof rules are established for parallel composition of systems. Probabilistic safety properties are defined, and these can represent a wide variety of useful properties such as: “The probability of an error occurring is at most 0.001.” An important concept in the discussion of these systems is that of an “adversary”; essentially, this is a path through the states of a probabilistic automaton whose transitions all have non-zero probabilities, and thus form a possible sequence of states.

In order to obtain useful results for parallel composition, the authors require a notion of fairness that requires that some action from each component appears infinitely often in the composition. This ensures that predicates true for each component can be used to deduce results for the composition. The authors have implemented their approach in an extended version of the PRISM probabilistic model checker. They describe two case studies: Aspnes and Herlihy’s randomized consensus algorithm and the Zeroconf protocol. The authors claim that “on the whole, compositional verification performs very well,” improving on the times of non-compositional methods. The paper is clearly written and should be of interest to those interested in verification, particularly because of the compositional approach.