Probabilistic guarded commands mechanized in HOL

Joe Hurd*, Annabelle McIver, Carroll Morgan

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

48 Citations (Scopus)

Abstract

The probabilistic guarded-command language (pGCL) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-)valued functions. We present a mechanization of the quantitative logic for pGCL using the HOL theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL. The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm.

Original languageEnglish
Pages (from-to)96-112
Number of pages17
JournalTheoretical Computer Science
Volume346
Issue number1
DOIs
Publication statusPublished - 23 Nov 2005

Fingerprint

Dive into the research topics of 'Probabilistic guarded commands mechanized in HOL'. Together they form a unique fingerprint.

Cite this