Talks

Labyrinth visit

Abstract
In which piglet explains to pooh an algorithm for constructing classical circular mazes, and pooh gets lost.

Refinement-oriented probability for CSP

Abstract
A non-operational approach to probabilistic computation is offered by the general technique of Jones and Plotkin [JP89, Jon90], in which it is shown how a `probabilistic powerdomain' can be formed over any complete partial order.

The technique has been used to produce a semantics for probabilistic CSP, using its ``failures/divergences'' semantics [Hoa84] (a CPO) as a basis for the Jones/Plotkin construction.

The results are extensive, interesting, surprising and in some cases puzzling, treating probability, concurrency and nondeterminism together [MMSS94a]. Lessons learnt from the CSP exercise could well be re-applied elsewhere, to (imperative) weakest-precondition-based CPOs for example.

In this talk I will give a (brief) introduction to the Jones/Plotkin method, and show (less briefly) how it may be used in the special case of CSP. Deep knowledge of CSP is not required (but shallow knowledge may well help).

Probabilistic predicate transformers

Abstract
In her thesis, Claire Jones (Edinburgh) proposed a generalisation of standard predicate transformers which allows reasoning about deterministic imperative programs containing probability.

I will discuss how, with an operational probabilistic model proposed independently of Jones' work by Jifeng He (Oxford), one can extend Jones' transformers to include non-determinism and can as well determine a pleasing structure on the space of probabilistic predicate transformers --- generating probabilistic "healthiness" conditions that generalise those of Dijkstra for standard programs.

And it's all done with a Galois connection.

On the Rigorous Construction of Computer Systems

Abstract
This talk will consist partly of an overview and partly of a discussion of recent results.

We begin with a brief overview of the approach of formal methods to the construction of computer systems. Each formal method provides a notation for describing behaviour at a given level of abstraction, together with a notion of refinement determining which descriptions at one level of abstraction conform to a description at a higher (or the same) level. By ensuring that the refinement criterion preserves behaviour it is guaranteed that an implementation constructed within such a method meets its specification. How much that says about the implementation depends, of course, on how expressive is the notation.

Early formal methods addressed only sequential functional behaviour. As such methods were used extensively over the next two decades demand grew for the incorporation of further functional behaviour, eliminating {\em post hoc} reasoning required by the extra functionality. Success has been achieved with parallelism and to some extent with real-time behaviour.

We survey criteria which have been proposed in various formalisms to ensure refinement. We concentrate on process-based descriptions that are able to express concurrency, non-interference or probability and consider refinement that:

  • preserves state-based functionality;
  • preserves non-interference of users of a distributed system;
  • lowers atomicity of an action;
  • is probabilistic.
It is proposed, subject to audience interest, to concentrate on probabilistic refinement of probabilistic specifications.

Proof rules for probabilistic loops

Abstract
This talk concentrates specifically on using probabilistic weakest preconditions to reason about iterations: the notion of "termination with probabilty 1" is conspicuous. I will describe probabilistic generalisations of the familiar "maintain the invariant" and "decrease the variant" tools for reasoning with loops, sketching their proofs (based on healthiness conditions) and applying them to examples. Some of the material could well be speculative.

Probabilistic weakest preconditions and the "0-1" law for termination.

Abstract
Probabilistic predicate transformers generalise the usual ones by allowing the predicates, seen as characteristic functions from the state space to {0,1}, to take values in the entire interval [0,1]. I'll explain briefly how that works (without very much justification), and then present the probabilistic version of the usual rule for loop correctness, in which partial correctness and termination can be treated separately. A surprising result of the loop rule is this "0-1" law (known at least since 1983, but not as easiy proved then): that for fixed set S of states, and fixed p>0, if for all s in S a process starting at s has probability at least p of leaving S -eventually-, then from all s it is in fact certain to leave S eventually (with probability 1). I'll use that to justify a "probabilistic variant" rule for termination, argue that it's complete over finite state spaces, and then show how it is used to prove the correctness of Herman's Self-stabilising Ring Protocol in a simpler way than he did.

Temporal Logic for Probabilistic Programs

Abstract
Temporal logic, when used to reason about programs, is most often based on a model of execution trees. We formulate the temporal operators ("always", "eventually" and "until") in the probabilistic weakest precondition semantics and use them to reason about a probabilistic algorithm that makes a set of users (processes, diplomats, ...) come to a unanimous decision provided they follow the protocol and are prepared to flip coins.

Visit to Finland The first three days of our visit were spent with talks. Initially the programme looked like this:

Tuesday morning 9.00 - 12.00 and Wednesday morning 9.00 - 12.00
Carroll Morgan, Annabelle McIver, Karen Seidel, Michael Butler:

  1. Introduction to probabilistic predicate transformers.
  2. Probabilistic healthiness conditions and the resulting algebra.
  3. Proof rules for loops: probabilistic invariants and variants.
  4. The steam boiler, and probabilistic data refinement (and the difficulty even of probablistic specification).
  5. Probabilistic temporal logic based on probabilistic predicate transformers (including "game theoretic" interpretations of the temporal operators).
  6. Labelled action systems with probability and fairness
Tuesday afternoon:
14.00
Marina Walden: Backwards refinement for verifying distributed systems
14.30
Kaisa Sere: VLSI design with action sytems
15.00
Jim Grundy: High School Mathematics (demonstration)
15.30
Break
16.00
John Harrision: Readable Proofs in HOL
16.30
Rimvydas Ruksenas: Refinement Calculator (demonstration)
17.00
Eric Hedman: Action Oberon (demonstration)
Wednesday afternoon:
14.00
Michael Butler: Pointer refinement
15.00
Ralph Back: Interpretations of demonic and angelic nondeterminism
15.45
Break
16.15
Jockum von Wright: on data refinement
In fact this time frame turned out to be too ambitious, not least because many of the talks led to lively discussions with the audience. Thus it ended up being spread over Thursday as well.

The talks on data refinement had shown up interesting parallels between the interaction of non-determinism and probabilistic choice on the one hand and that of non-determinism and angelic choice on the other. Friday morning was spent exploring and comparing these.

Our presentation of the probabilistic steam boiler had drawn the criticism that it was simplified to the extent that it was no longer recognizable as a steam boiler. Friday afternoon was spent working on a slightly more believable version.

On Saturday our hosts took us to the beach: