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).

Lecture   Topic     Slides in pdf
1–2.   Probabilistic temporal logic: qTL     (for viewing, for printing).
3.   Probabilistic sequential-programming logic: pGCL     (for viewing, for printing).
4–5.   Quantitative modal mu-calculus: qMµ     (for viewing, for printing).
  (Seminar 13 December: pCSP)     (for viewing, for printing).

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.