Probabilistic guarded commands mechanized in HOL
<p>The probabilistic guarded-command language (<em>pGCL</em>) 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- (...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Elsevier
2005
|
| Subjects: |
| Summary: | <p>The probabilistic guarded-command language (<em>pGCL</em>) 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.</p> <p>We present a mechanization of the quantitative logic for <em>pGCL</em>using the <em>HOL</em> theorem prover, including a proof that all <em>pGCL</em>commands satisfy the new condition <em>sublinearity</em>, the quantitative generalization of <em>conjunctivity</em> for standard <em>GCL</em>.</p> <p>The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated <em>pGCL</em>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 <em>mutual-exclusion</em> algorithm.</p> |
|---|