Collections

Abstraction, refinement and proof for probabilistic systems , a tutorial and reference guide to the principal publications, Springer Verlag Monographs in Computer Science Published January 2005

Themes

Examples and case studies;

Probabilistic process algebra;

Probability and nondeterminism in sequential programming;

Probabilistic temporal logic, and applications to Markov processes;

Security and modularity;

Quantum computation;

Reports in progress.

Examples and case studies

Stop-and-wait protocol MMSS94a.

Probabilistically-failing buffers in series: MMSS95.

Probabilistic dining philosophers: RDP98, QLE.

Simple loops and probabilistic invariants: M95, pGCL, B98.

Simple loops and probabilistic variants: M95, pGCL.

Rabin's choice-coordination: pGCL, DC96.

Herman's self-stabilisation: M95.

The steam boiler: STEAM96.

Mr Bean's socks: SMM96.

Symmetric random walk: MM97, RW96.

Spies, modules and information security: QMSRM, QMSPL.

Tutorials: pGCL, SMM96.

Probabilistic data refinement: STEAM96, DR96.

Expected efficiency/complexity: SMM96, EFF98, QLE.

Probabilistic process algebra

MMSS94a A probabilistic process algebra including demonic nondeterminism.

Refinement-oriented probability for CSP.
Carroll Morgan, AK McIver, Karen Seidel and J.W. Sanders.
PRG Technical Report PRG-TR-12-94, 1994.
Also Formal Aspects of Computing 8(6), pp.617-647.

MMSS95 Addresses some of the unruliness of demonic nondeterminism in MMSS94a.

Argument Duplication in probabilistic CSP.
Carroll Morgan, AK McIver, Karen Seidel and J.W. Sanders.
PRG Technical Report PRG-TR-11-95, 1995.

MM95a Characterises deterministic (non-demonic) processes in MMSS94a.

Probabilistic Determinism.
AK McIver and Carroll Morgan.
PRG Technical Report PRG-TR-13-95, 1995.

SM95 Links some of the above models.

Hierarchical Reasoning in Probabilistic CSP.
Karen Seidel and Carroll Morgan.
PRG Technical Report PRG-TR-3-96, 1996.
Also Programmirovanie (Russian journal of Programming and Computer Software) 23(5), 1997.

Probability and nondeterminism in sequential programming

GD03 Investigates techniques within pGCL for reasoning about programs intgended to generate specific distributions of results.

Generating distributions.
John Yu.
M.Sc. dissertation, supervised by JW Sanders, 2003.

HOL04b Provides a HOL formalisation for analysing expected time bounds of probabilistic programs, based on pGCL.

Cost-based analysis of probabilistic programs mechanised in HOL.
Orieta Celiku and AK McIver
Submitted for publication.

HOL04a Presents a HOL mechanisation of the probabilistic guarded-command language, and its logic, and uses that to construct an automatic proof tool for verification-condition generation.

Probabilistic guarded commands mechanized in HOL.
Joe Hurd, AK McIver and C.C. Morgan.
To appear in Proc. QAPL 04 (ETAPS satellite).

HR04 Gives upper- and lower bound for stabilisation of Herman's Ring, illustrating abstraction and nondeterminism in probabilistic systems.

An elementary proof that Herman's Ring is THETA(N^2).
AK McIver and C.C. Morgan.
Submitted for publication.

EFF98 Proposes mu-calculus expressions for efficiency, extending MM97, and applies the result to Rabin's Choice Coordination.

Reasoning about efficiency within a probabilistic mu-calculus.
AK McIver.
Presented at the Pre-LICS 98 workshop on Probabilistic Methods in Verification, Indianapolis, May 1998.
To appear in Electronic Notes in Theoretical Computer Science 22 (1999), http://www.elsevier.nl/locate/entcs/volume22.html

QLE Extends EFF98 to incorporate the notions of fairness and compositionality in performance analyses; the methods are applied to Rabin and Lehmann's probabilistic dining philosophers.

Quantitative program logic and efficiency in probabilistic distributed algorithms.
AK McIver.
This is an extended version of the paper Quantitative program logic and performance, Proceedings of 5th International AMAST Workshop, ARTS '99, Bamberg, Germany, May 26-28, 1999. LNCS 1601.

HSM95 An operational (relational) model for probabilistic and demonic sequential programs.

Probabilistic models for the guarded command language.
He Jifeng, Karen Seidel and AK McIver.
Science of Computer Programming 28, 1997, pp.171-192.

MMSS94b A wp-style logic for HSM95.

Probabilistic predicate transformers.
Carroll Morgan, AK McIver and Karen Seidel.
PRG Technical Report PRG-TR-4-95, 1995.
Also ACM Transactions on Programming Languages and Systems 18(3), pp.325-353.

pGCL An introduction to MMSS94b .

pGCL: formal reasoning for random algorithms.
Carroll Morgan and AK McIver.
To appear in the South African Computer Journal in 1999.

M95 Introduces probabilistic invariants and variants for MMSS94b , generalising the standard rules.

Proof Rules for Probabilistic Loops.
Carroll Morgan.
PRG Technical Report PRG-TR-25-95, 1995.
Proceedings of the BCS-FACS 7th Refinement Workshop, Springer Verlag Electronic Workshops in Computing, Ed. He Jifeng, John Cooke and Peter Wallis, July 1996. Two illustrations are available as a 180796-byte gzipped PostScript file.

PCfPDP Describes probabilistic weakest-liberal preconditions, the theory necessary for M95.

Partial correctness for probabilistic demonic programs.
AK McIver and Carroll Morgan.
To appear in Acta Informatica.

STEAM96 Treats probabilistic data-refinement in the context of a well-known test case.

The probabilistic steam boiler: a case study in probabilistic data refinement.
AK McIver, Carroll Morgan and Elena Troubitsyna.
To appear in Proceedings of the International Refinement Workshop, Canberra 1998.

PPT2 Revises MM96 : investigates the general structure of the probabilistic predicate-transformer space.

Demonic, angelic and unbounded probabilistic choice in sequential programs.
AK McIver and Carroll Morgan.
To appear in Theoretical Computer Science.

B98 Presents pGCL in the style of Abrial's Generalised Substitution Language.

The Generalised Substitution Language extended to probabilistic programs.
Carroll Morgan.
Proceedings B'98: the 2nd International B Conference. Montpelier, 22-24 April 1998. Springer Verlag LNCS.

SMM96 Another introduction to MMSS94b.

An introduction to probabilistic predicate transformers
Karen Seidel, Carroll Morgan and AK McIver.
PRG Technical Report PRG-TR-6-96, 1996.

MM95 Specialises PCfPDP to standard (non-probabilistic) programs.

Unifying wp and wlp.
Carroll Morgan and AK McIver.
PRG Technical Report PRG-TR-23-95, 1995.
Also Information Processing Letters 59(3), 1996, pp.159-163.

MM96 Extends MMSS94b in various technical ways, including infinite state spaces.

Probabilistic predicate transformers: Part 2.
AK McIver and Carroll Morgan.
PRG Technical Report PRG-TR-5-96, 1996.
See also PPT2.

ZB2003a Treats probability-one termination in the style of Abrial's Generalised Substitution Language.

Probabilistic termination in B.
Annabelle McIver, Carroll Morgan and Thai Son Hoang.
Proceedings ZB'03: Turku, June 2003. Springer Verlag LNCS.

Probabilistic temporal logic

Games03 Much expanded journal version of Games02 on the game- and logical interpretations of the quantitative modal mu-calculus

Results on the quantitative mu-calculus qMu.
AK McIver and CC Morgan, September 2003
To appear in ACM Trans. Computational Logic, 2005.

Games02 Establishes an equivalence between Kozen- (logical-) and Stirling- (game-based operational) interpretations of the quantitative modal mu-calculus

Games, probability and the Quantitative Mu-Calculus.
(Extended abstract)
AK McIver and CC Morgan, June 2002.
Here are draft presentations of full proofs for lemmas 6.2, A.2, A.5, A.7 and A.8.

MDP01 Applies the probabilistic programming/temporal logic to Markov Decision Processes.

Cost analysis of games, using programming logic.
Annabelle McIver and Carroll Morgan.
Presented at APSEC '01, University of Macau, December 2001.

PROB-1 Specialises quantitative temporal logic to the case of achieving properties with probability 1.

Almost-certain eventualities and abstract probabilities in quantitative temporal logic.
Annabelle McIver and Carroll Morgan.
Presented at CATS 2001 — Computing: The Australasian Theory Symposium, Bond University, Queensland, January 2001.
Also to appear in Theoretical Computer Science.

STAT01 Uses the built-in nondeterminism of the probabilistic logic to generalise the notion of stationarity in Markov processes.

Stationarity in probabilistic programs.
Annabelle McIver.
Proceedings 17th Conf. Foundations of Programming Semantics.
Aarhus, May 2001.

PTL96 Extends standard temporal logic to probabilistic, using the techniques of MMSS94b.

A probabilistic temporal calculus based on expectations.
Annabelle McIver and Carroll Morgan.
Proceedings Formal Methods Pacific '97, Wellington 9-11 July 1997.
Lindsay Groves and Steve Reeves (Eds).
Springer Verlag Singapore.
Also PRG Technical Report PRG-TR-13-97, 1997.

MM97 A systematic presentation of the theory underlying PTL96.

An expectation-based model for probabilistic temporal logic.
Carroll Morgan and AK McIver.
PRG Technical Report PRG-TR-20-97, 1997.
A more recent version appears in Logic Journal of the IGPL 7,6, 779-804, 1999.

See also RW96, EFF98, DC96, QLE.

Security and modularity

RDC98 Addresses the interactions of probability, nondeterminism and modularity.

Restricted demonic choice for modular probabilistic programs.
Daniel Robinson and Carroll Morgan.
Presented at ESSLLI PLRC Workshop '98, Saarbrucken.

QMSRM A relational "quantum-like" model for the issues raised in RDC98.

A quantified measure of security I: a relational model.
Carroll Morgan and AK McIver.

QMSPL A programming logic for QMSRM.

A quantified measure of security II: a programming logic.
AK McIver and Carroll Morgan.

Quantum computation

Z01 Shows that quantum computation can be treated as precisely as classical computation: defines a suitable high-level programming language; shows that it describes all known quantum algorithms and some quantum systems; and considers the issues that arise when designing a compiler for that language.

Quantum Programming
Paolo Zuliani.
D.Phil. Thesis, 2001.

SZ00 Presents qGCL in which quantum algorithms can be expressed and derived.

Quantum Programming
JW Sanders and P Zuliani.
Proc. Maths. Program Construction 2000.

CQP Uses the normal-form approach to compiler design to study a possible design for a qGCL compiler.

Compiling quantum programs
P Zuliani.

SZ00 Uses qGCL to reason about some famous examples of quantum non-locality.

Formal reasoning for quantum-mechanical locality
P Zuliani.

LR01 Formally defines reversibility and shows how to transform a given pGCL into an equivalent but reversible version

Logical reversibility
P Zuliani.
IBM J. Res. Dev. 45(6), 2001.

Reports in progress

ARP Textbook/monograph introduction to this entire collection.

Abstraction, refinement and proof for probabilistic systems.
Annabelle McIver, Carroll Morgan.

DR96 Extends conventional data-refinement techniques to MMSS94b.

Probabilistic data refinement.
Probabilistic Systems Group.

DC96 Treats termination of Rabin's algorithm using the techniques of MM97.

The choice-coordination problem: notes for a correctness proof.
Probabilistic Systems Group.
Two illustrations are available as a 255318-byte gzipped PostScript file.
See also pGCL for a treatment of Rabin's algorithm, using probabilistic variants rather than temporal logic.

RW96 Analyses the random walk and several variations (random stumble, for example) in the probabilistic temporal logic of MM97.

Notes on the random walk: an example of probabilistic temporal reasoning.

RDP98 Uses probabilistic variants to establish termination in Rabin and Lemann's symmetric and distributed dining philosophers

An example of probabilistic variants: The free philosophers
Carroll Morgan and AK McIver.

Related publications

AB57

The Lognormal Distribution, J. Aitchison and J.A.C. Brown, C.U.P., 1957.

AH90

Fast randomized consensus using shared memory, J. Aspnes and M. Herlihy, J. Algorithms, 11, 441-461, 1990.

Bac88

A calculus of refinements for program derivations, R-J.R. Back, Acta Informatica, 25, 593-624, 1988.

BS81

Lognormal Genesis, G. Brown and J.W. Sanders, J. Applied Probability, 18, 12 pages, 1981.

But92

A CSP Approach to Action Systems, M. Butler, DPhil thesis, Oxford University, December 1992.

Col93

The Refinement of Action Systems, I.M. Collier, DPhil thesis, Oxford University, to be submitted 1993.

CP88

A Multicast Transport Protocol, J. Crowcroft, K. Paliwoda, 1988 SIGCOMM Conference Proceedings, p. 247 - 256,July 1988.

Fra86

Fairness, N. Francez, Springer Verlag, 1986.

GM89

A single complete rule for data refinement, P.H.B. Gardiner and C.C. Morgan, Technical Report PRG-TR-7-89, Programming Research Group, Oxford University, November 1989. To appear in Formal Aspects of Computing.

GS91

On the Refinement of Non-interference, J. Graham-Cumming and J.W. Sanders, Proceedings of the 1991 Franconia Security Workshop, IEEE Computer Society Press, 35-42, 1991.

Hay87

Specification Case Studies, I.J. Hayes, editor, Prentice-Hall, London, 1987.

HHS86

Data refinement refined, J. He, C.A.R. Hoare and J.W. Sanders, First Europ. Symp. on Prog., SLNCS #213, 187-197, 1986.

Her90

Probabilistic Self-Stabilization, T. Hermann, IPL, 35, 63-67, 1990.

Hoa84

Communicating Sequential Processes, C.A.R. Hoare, Prentice Hall International, 1984.

HHS87

Prespecification in data refinement, C.A.R. Hoare, J. He and J.W. Sanders, IPL, 25, 71-76, 1987.

inm88

occam2 Reference Manual, INMOS Ltd., Prentice Hall International, 1988.

Ip90

Development into Hardware and Software, N. Ip. Fourth-year project, Oxford, 1990.

ISO

The ISO standard.

CBJ86

Systematic Software Development using VDM (2nd edition), C.B. Jones, Prentice Hall International, 1986.

Jon90

Probabilistic Nondeterminism, C. Jones, Edinburgh, 1990. Available as Technical Report ECS-LFCS-90-105.

JP89

A probabilistic powerdomain of evaluations, C. Jones and B. Plotkin, Proc. 4th Annual Symposium on LICS, 1989.

Kin90

Computer and Communication Systems Performance Modelling, P.J.B. King, Prentice-Hall International, 1990.

Knu73

The Art of Computer Programming, D.E. Knuth, Volume 3, Addison Wesley, 1973.

Kol41

On the lognormal distribution of the dimension of crushed particles, Comptes Rendus (Doklady) de L'Academie de l'URSS, xxxi(2), 99-101, 1941.

lot

lotos.

LP88

Using Multicast in a Distributed Robust Filestore, J. Lu, K. Paliwoda, UK IT 88 Conference Publication, University College Swansea, p. 588 - 592, July 1988.

LS90

The Projection of Systolic Programs, C. Lengauer and J.W. Sanders, Formal Aspects of Computing, 2, 273-293, 1990.

LS80

On an Inversion Theorem of Möbius, J.H. Loxton and J.W. Sanders, J. Austral. Math. Soc. (series A), 30, 15-32, 1980.

Mil89

Communication and Concurrency, R. Milner, Prentice Hall International, 1989.

Mor85a

Specification of a simplified network system in Z, C.C. Morgan, in T. Denvir et al, editors, Proceedings of the Workshop on Analysis of Concurrent Systems, Springer, LNCS 207, 1985.

Mor90b

Of wp and CSP, C.C. Morgan, in A.J.M. van Gasteren, W.H.J. Feijen, D. Gries, and J. Misra, editors, Beauty is our Business, Springer, 1990.

Mor94

Programming from Specifications, C.C. Morgan, Prentice Hall International, 2ed 1994.

MG84

Ease of use through proper specification, C.C. Morgan and R.B. Gimson, in D. Duce, editor, Proceedings of the Distributed Computing Systems Conference, Peter Perigrinus, 1984.

Mor85b

Specification of a simplified network system in CSP, C.C. Morgan and C.A.R. Hoare, in T. Denvir et al, editor, Proceedings of the Workshop on Analysis of Concurrent Systems, Springer, LNCS 207, 1985.

MRG88

On the refinement calculus, C.C. Morgan, K.A. Robinson, and P.H.B. Gardiner, Technical Report PRG-70, Programming Research Group, 1988.

Nel90

A Formal Approach to Communcation Protocols, N. Nelkon, MSc thesis, Oxford, September 1990.

Pal88a

Performance Analysis of Loadsharing Algorithms, K. Paliwoda, Master's thesis, Birkbeck College, London, Dec 1988.

Pal88b

Transactions involving Multicast, K. Paliwoda, Computer Communications, Vol. 11, p. 313 - 318, Dec 1988.

San83

Chapters 14, 15 in the second edition of R.E. Edwards: Fourier Series: A Modern Introduction, Springer-Verlag, 1983.

PS91

An incremental specification of the sliding-window protocol, K. Paliwoda and and J.W. Sanders, Distributed Computing, 83-94, May 1991.

PS83

Asymptotic frequency of switchyard permutations, J.M. Potter and J.W. Sanders, Austral. Comp. Sci. Conf. 6, 1983.

QA92

The Queen's Award for Technological Achievement 1992, awarded jointly with IBM, 1992.

QA90

The Queen's Award for Technological Achievement 1990, awarded jointly with INMOS, 1990.

Rab91

Optimal parallel pattern matching through randomisation, M.O. Rabin, In Proc. Sequences 91 Conference, 1991.

Rao94

Reasoning about probabilistic parallel programs, J.R. Rao, ACM Transactions on Programming Languages and Systems, June 1994.

San89

Refinement for Z, J.W. Sanders, Z course monograph, Oxford, 36 pages, 1988, 1989.

San92

Lectures on VLSI Design, J.W. Sanders, draft book, 1992.

San94

Hardware Design: A Modern Introduction, J.W. Sanders, to appear Prentice Hall International, 1994.

Sei92

Probabilistic Communicating Processes, K. Seidel, DPhil thesis, Oxford University, PRG Monograph PRG-102, May 1992.

SS94

Translating occam2 into CSP, B. Scattergood, K. Seidel, in: Transputer Applications and Systems '94, Editors: A.De Gloria, M.R. Jane, D. Marini, IOS press.

SMG95

A Structured Development of a Distributed Shared Memory System K. Seidel, A. McIver, P.Gardiner, to appear in Formal Aspects of Computing

Sei94

Case Study: Specification and Refinement of the PI-Bus, K. Seidel, in Proceedings of FME '94: Industrial Benefit of Formal Methods, (M Naftalin, T Denvir and M Bertran, eds) LNCS 873, Springer-Verlag, Heidelberg, 1994. (pp 532--546).

Sei95

Probabilistic CSP, K. Seidel, to appear in Distributed Computing, 1994.

SNH93

From CSP models to markov models, E.V. Sorensen, J. Nordahl and N.H. Hansen, IEEE Transactions on Software Engineering, to appear, 1993.

Spi89

The Z Notation: A reference manual, J.M. Spivey, Prentice Hall International, 1989.

Tan90

Computer Networks, second edition, A. Tanenbaum, Prentice Hall International, 1990.

Tar85

Amortised computational complexity, R.E. Tarjan, SIAM Journal on Algebraic and Discrete Methods 6, 306-318, 1985.

Val82

A scheme for fast parallel communication, L.G. Valiant, SIAM Journal on Computing, 11(2), 350-361, 1982.

VPV92

Protocol Design and Implementation Using Formal Methods, M. Vansinderen, L.F. Pires and C.A. Vissers, Computer Journal 1992 Vol.35 No.5 pp.478-491.

WM90

Refinement of state-based concurrent systems, J.C.P. Woodcock and C.C. Morgan, in Proceedings of the 3rd VDM-Eurpope Symposium, pages 340-351, Kiel, Springer, LNCS 428, 1990.