Expectation-based reasoning for sequential probabilistic
programs
Presented at ZB-2005, 12–15 April 2005 in Guildford, UK
by Carroll Morgan
from the
University of New South Wales
(near Botany Bay).
| |
One of the many approaches to the formal treatment of probabilistic programs is
the use of real-valued rather than Boolean-valued predicates for assertions.
These “probabilistic predicates”, which we call “expectations”, generalise
Hoare-, Dijkstra- and B- style semantics in the same way: rather than assure a
program will achieve a postcondition from some precondition, instead one assures
that the “weighted average” of the real-valued “post-expectation” will never be
less than a certain initial-state-dependent minimum.
This generalises the usual approach, provided we identify false/true with zero/one,
since then we have false < true — and the weighted average of a postcondition
over a single final state is just one if the state satisfies the postcondition
and zero otherwise. The correctness condition then requires that the
postcondition is one if the precondition was.
However the real-valued expectations allow much more: they can be used to
specify and/or validate a program’s probability of achieving a postcondition and
—more generally still— they can be used to describe the “cost” (or some
other quantified measure) of running a program.
In this tutorial I will introduce the basics of this relatively new approoach,
and discuss how it applies to B and/or Z.
For more information have a look at
the recently published text
(in whose downloadable preface you can find out
where the strange picture at right comes from).
|
|
|
The tutorial will be in two parts, as listed below with pdf slides for viewing (full-sized) and
printing (four-to-a-page).
A list of papers for background reading is given in the preface of
Abstraction, Refinement and Proof for Probabilistic Systems,
and many of the papers referred to in that list can be found at our
collection of publications.
There are two papers in particular that give gentle introductions, one in the B-style,
and the other in the guarded-command style. (They treat different sets of examples, hence it
might be worth glancing at both.)