Journal article icon

Journal article

Probabilistic guarded commands mechanized in HOL

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 pGCLusing the HOL theorem prover, including a proof that all pGCLcommands satisfy th...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Publisher's version

Actions


Access Document


Files:
Publisher copy:
10.1016/j.tcs.2005.08.005

Authors


More by this author
Institution:
University of Oxford
Oxford college:
Magdalen College
Department:
Mathematical, Physical & Life Sciences Division - Department of Computer Science
Role:
Author
More by this author
Institution:
Macquarie University
Role:
Author
More by this author
Institution:
University of New South Wales
Role:
Author
More from this funder
Funding agency for:
Joe Hurd
Publisher:
Elsevier Publisher's website
Journal:
Theoretical Computer Science Journal website
Volume:
346
Issue:
1
Pages:
96–112
Publication date:
2005-11-05
DOI:
ISSN:
0304-3975
URN:
uuid:85e3a354-dd4d-49f3-9f21-c9e03a0565f9
Local pid:
ora:10764

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP