Lectures on Probabilistic Formal Methods for the 2004
RSISE Logic Summer School
Canberra, 6–17 December 2004
Carroll Morgan
University of New South Wales
|
The presentation explains and motivates a programming logic and semantics that includes
both demonic and probabilistic nondeterminism. The former is used to control
abstraction and refinement while developing algorithms and systems; the latter
allows those systems to contain exhibit probabilistic –that is, quantifiably random– behaviour.
Probability is important for random algorithms, for distributed systems and
for quantification of risk and cost.
The individual lectures will begin with quantitative temporal logic, then returning to cover elementary sequential program logic (based on Dijkstra's minimally-syntaxed programming language GCL), loops and their associated invariant/variant reasoning tools. The final lectures will explore more exotic topics such as the quantitative modal µ-calculus, and its connection to angelic/demonic/probabilistic two-player games. |
|
The specific topics are listed below, together 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.