zbMATH — the first resource for mathematics

Probabilistic guarded commands mechanized in HOL. (English) Zbl 1080.68063
Summary: 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.

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[2] Gordon, M.J.C., Mechanizing programming logics in higher order logic, (), 387-439
[3] Gordon, M.J.C.; Melham, T.F., Introduction to HOL (A theorem-proving environment for higher order logic), (1993), Cambridge University Press Cambridge · Zbl 0779.68007
[4] M. Gordon, R. Milner, C. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science, Vol. 78, Springer, Berlin, 1979.
[5] J. Harrison, Formalizing Dijkstra, in: J. Grundy, M. Newey (Eds.), Theorem Proving in Higher Order Logics, 11th Internat. Conf., TPHOLs ’98, Lecture Notes in Computer Science, Vol. 1497, Canberra, Australia, Springer, Berlin, September 1998, pp. 171-188.
[6] T.S. Hoang, Z. Jin, K. Robinsion, A.K. McIver, C.C. Morgan, Probabilistic invariants for probabilistic machines, in: Proc. third Internat. Conf. of B and Z Users 2003, Lecture Notes in Computer Science, Vol. 2651, Springer, Berlin, pp. 240-159. · Zbl 1028.68547
[7] J. Hurd, Formal verification of probabilistic algorithms, Ph.D. Thesis, University of Cambridge, 2002. · Zbl 1013.68193
[8] M. Huth, The interval domain: a matchmaker for aCTL and aPCTL, in: R. Cleaveland, M. Mislove, P. Mulry (Eds.), US-Brazil Joint Workshops on the Formal Foundations of Software Systems, Electronic Notes in Theoretical Computer Science, Vol. 14, Elsevier, Amsterdam, 2000.
[9] D. Kozen. A probabilistic PDL, Proc. 15th ACM Symp. on Theory of Computing, 1983. · Zbl 0575.03013
[10] E. Kushilevitz, M.O. Rabin, Randomized mutual exclusion algorithms revisited, in: M. Herlihy (Ed.), Proc. 11th Ann. Symp. on Principles of Distributed Computing, Vancouver, BC, Canada, ACM Press, New york, August 1992, pp. 275-283. · Zbl 1370.68318
[11] M. Kwiatkowska, G. Norman, D. Parker, Prism: probabilistic symbolic model checker, in: Proc. of PAPM/PROBMIV 2001 Tools Session, September 2001. · Zbl 1047.68533
[12] McIver, A.K.; Morgan, C.C., Partial correctness for probabilistic programs, Theoret. comput. sci., 266, 1-2, 513-541, (2001) · Zbl 0992.68137
[13] C. Morgan, Proof rules for probabilistic loops, in: H. Jifeng, J. Cooke, P. Wallis (Eds.), Proc. BCS-FACS 7th Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996.
[14] C. Morgan, A. McIver, pGCL: formal reasoning for random algorithms, South African Comput. J. 22 (1999) 14-27.
[15] Morgan, C.; McIver, A.; Seidel, K., Probabilistic predicate transformers, ACM trans. programming languages systems, 18, 3, 325-353, (1996), See also [12]
[16] T. Nipkow, Hoare logics in Isabelle/HOL, in: H. Schwichtenberg, R. Steinbrüggen (Eds.), Proof and System-Reliability, Kluwer, Dordrecht, 2002, pp. 341-367.
[17] Shield, J.; Hayes, I.J.; Carrington, D.A., Using theory interpretation to mechanise the reals in a theorem prover, () · Zbl 0970.68146
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.