The formal method

The probabilistic guarded-command language has been provided with a relational semantics [8] and a predicate-transformer-like semantics [22]. In the relational model each (generally nondeterminisitc) program is denoted by a function mapping each initial state to a set of distributions over final states. To reflect possible nontermination, distributions sum to at most 1; the deficiency from 1 determines their probability of divergence. Program refinement is modelled by inclusion of distribution sets, and the expected standard and probabilistic laws are shown to hold. (A second model, obtained by using the Jones and Plotkin probabilistic lifting [13] and satisfying more specialised laws, is also given in [8] for comparison.)

In the predicate-transformer-like model [22, 37] predicates are replaced by expectations: real-valued random variables on state space, interpreted as expected payoffs. Thus post expectations define expected payoffs on termination and pre expectations define expected payoffs from the corresponding initial states. Each program (again, in general nondeterministic) is denoted by a function from post expectations to pre expectations. The `weakest precondition' approach for embracing demonic nondeterminism in the standard case becomes a definition in which expected yields over final states are mapped to `most-pessimistic' expected payoffs over initial states. Program refinement is modelled by pointwise domination of the corresponding expectation transformers. The resulting model extends to nondeterministic programs that of Kozen [14] and satisfies the expected laws, suitably generalised. It is extended to infinite state spaces and to specification constructs (for example angelic nondeterminism) in [23].

Dijkstra's healthiness conditions (strictness, monotonicity, conjunctivity and continuity) [5], which in the standard case characterise predicate transformers corresponding to relational programs, is extended in [22] to characterise those expectation transformers corresponding to programs in the relational model of the probabilistic guarded command language. A single simple condition, sublinearity, replaces Dijkstra's conditions.

Even though those semantic forms are, as usual, suitable for specifying constructs more abstract than code they do not, as they stand, provide a sufficiently abstract vehicle for specifying probability in the presence of nondeterminism. Experiments have been conducted into the combination of the state-based specification notation Z with probability [39, 15, 38]; but it is too early to decide upon a satisfactory approach.

The models mentioned above form complete partial orders in which the standard model is embedded. The notion of refinement between programs is thus central to the theory; it is the touchstone for valid program development. In [37] the development laws are shown to work -- with little more complication than in the standard case -- on the well-known Monty Hall problem (variants of which are considered in [19]). That problem, whilst exhibiting nondeterminism and probability, contains no iteration. Laws for the partial and total correctness of probabilistic loops are considered in [24]. The 0/1 law (for the probability with which a loop terminates, using a probabilistic variant) of Hart, Sharir and Pnueli [7] is incorporated in the expectation-transformer model and slightly extended. In the presence of nondeterminism the elegant result mentioned earlier holds: a (probabilistic and nondeterministic) loop terminates if on each iteration its body offers a nonzero probability of decreasing some variant. Partial correctness of a probabilistic loop requires that a probabilistic temporal formula be established. Techniques for that are provided by probabilistic temporal logic; and so such a logic has been given an expectation-transformer model [28, 30] and applied in [17, 29]. It generalises to probabilities Ben-Ari's eight axioms for standard branching-time temporal logic [2], using an expectation-transformer model of the modal -calculus. It strengthens previous logics by being able to express explicit probabilites (not merely establishing results with probability 1).

The refinement laws referred to so far aid operation refinement (in which the state space of the program remains unchanged). The alternative case, of data refinement, is considerably more subtle and has been studied via a well-known safety-critical case study: the steam boiler [18]. There the simulations of standard data refinement, which relate abstract and concrete states and are used to justify a change of state space, are replaced by transformers embodying conditional probabilities. In the standard case a single predicate-transformer simulation rule is sufficient to establish all valid data refinements [6]. A probabilistic version of that single rule is no longer sufficient in the probabilistic case; a completeness result is an important topic for future work.

In terms of the four goals of this part of the project, a comprehensive formal method has been produced.

Next: Validating examples Up: Specific results Previous: Overview of results