Partial correctness for probabilistic demonic programs. (English) Zbl 0992.68137
Summary: Recent work in sequential program semantics has produced both an operational [J. He, K. Seidel and A. McIver, Sci. Comput. Program. 28, No. 2-3, 171-192 (1997; Zbl 0877.68014)] and an axiomatic [C. C. Morgan, A. McIver and K. Seidel, ACM Trans. Programming Languages Systems 18, No. 3, 325-353 (1996); K. Seidel, C. C. Morgan, A. K. McIver, Tech Report PRG-TR-6-96, Programming Research group, February 1996)] treatment of total correctness for probabilistic demonic programs, extending Kozen’s original work [D. Kozen, J. Comput. System Sci. 22, 328-350(1981; Zbl 0476.68019)] by adding demonic nondeterminism. For practical applications (e.g. combining loop invariants with termination constraints) it is important to retain the traditional distinction between partial and total correctness. C. Jones (Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University, Edinburgh, UK, 1990) defines probabilistic partial correctness for probabilistic, but again not demonic programs. In this paper we combine all the above, giving an operational and axiomatic framework for both partial and total correctness of probabilistic and demonic sequential programs; among other things, that provides the theory to support our earlier – and practical – publication on probabilistic demonic loops [C. C. Morgan, in: Jifeng et al. (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996)].
MSC:
| 68Q55 | Semantics in the theory of computing |
Software:
UNITYReferences:
| [1] | S. Abramsky, A. Jung, Domain theory, in: Dov M. Gabbay S. Abramsky, T.S. Maibaum (Eds.), Handbook of Logic and Computer Science, Vol. 3, Oxford, Clarendon Press, 1994, p. 1-168.; S. Abramsky, A. Jung, Domain theory, in: Dov M. Gabbay S. Abramsky, T.S. Maibaum (Eds.), Handbook of Logic and Computer Science, Vol. 3, Oxford, Clarendon Press, 1994, p. 1-168. |
| [2] | Chandy, K. M.; Misra, J., Parallel Program Design: A Foundation (1988), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0717.68034 |
| [3] | Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013 |
| [4] | Edalat, A., Domain theory and integration, Theoret. Comput. Sci., 151, 163-193 (1995) · Zbl 0872.28006 |
| [5] | Edalat, A.; Negri, S., The generalised Riemann integral on locally compact spaces, Topology Appl., 89, 121-150 (1998) · Zbl 0927.28002 |
| [6] | Escardo, M. H., Pcf extended with real numbers, Theoret. Comput. Sci., 162, 79-115 (1996) · Zbl 0871.68034 |
| [7] | Feldman, Y. A.; Harel, D., A probabilistic dynamic logic, J. Comput. System Sci., 28, 193-215 (1984) · Zbl 0537.68036 |
| [8] | Grimmett, G.; Welsh, D., Probability: an Introduction (1986), Clarendon Press: Clarendon Press Oxford · Zbl 0606.60002 |
| [9] | He, J.; Seidel, K.; McIver, A. K., Probabilistic models for the guarded command language, Sci. Comput. Programming, 28, 2,3, 171-192 (1997) · Zbl 0877.68014 |
| [10] | Hesselink, W. H., Programs, Recursion and Unbounded Choice, Number 27 in Cambridge Tracts in Theoretical Computer Science (1992), Cambridge University Press: Cambridge University Press Cambridge, UK · Zbl 0759.68057 |
| [11] | C. Jones, Probabilistic nondeterminism. Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University Edinburgh, UK, 1990.; C. Jones, Probabilistic nondeterminism. Monograph ECS-LFCS-90-105, Ph.D. Thesis, Edinburgh University Edinburgh, UK, 1990. |
| [12] | A. Jung, private communication, 1997.; A. Jung, private communication, 1997. |
| [13] | Kozen, D., Semantics of probabilistic programs, J. Comput. System Sci., 22, 328-350 (1981) · Zbl 0476.68019 |
| [14] | D. Kozen, A probabilistic PDL, in: Proc. 15th ACM Symp. on Theory of Computing, ACM, New York, 1983.; D. Kozen, A probabilistic PDL, in: Proc. 15th ACM Symp. on Theory of Computing, ACM, New York, 1983. |
| [15] | A.K. McIver, C.C. Morgan, Demonic, angelic and unbounded choices in probabilistic programs, Tech. Report PRG-TR-5-96, Programming Research Group, March 1996. See PPT athttp [23]; A.K. McIver, C.C. Morgan, Demonic, angelic and unbounded choices in probabilistic programs, Tech. Report PRG-TR-5-96, Programming Research Group, March 1996. See PPT athttp [23] · Zbl 0971.68027 |
| [16] | A.K. McIver, C.C. Morgan, Partial correctness for probabilistic programs. Tech. Report, Programming Research Group, 1996. See PCFPP athttp [23]; A.K. McIver, C.C. Morgan, Partial correctness for probabilistic programs. Tech. Report, Programming Research Group, 1996. See PCFPP athttp [23] · Zbl 0992.68137 |
| [17] | C.C. Morgan, Proof rules for probabilistic loops, in: H. Jifeng, J. Cooke, P. Wallis (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996. http://www.springer.co.uk/ewic/workshops/7RW.; C.C. Morgan, Proof rules for probabilistic loops, in: H. Jifeng, J. Cooke, P. Wallis (Eds.), Proc. BCS-FACS Seventh Refinement Workshop, Workshops in Computing, Springer, Berlin, 1996. http://www.springer.co.uk/ewic/workshops/7RW. |
| [18] | C.C. Morgan, A.K. McIver, Unifying wpwlp[23]; C.C. Morgan, A.K. McIver, Unifying wpwlp[23] · Zbl 0875.68625 |
| [19] | C.C. Morgan, A.K. McIver, J.W. Sanders, Probably Hoare? Hoare probably! 1999.; C.C. Morgan, A.K. McIver, J.W. Sanders, Probably Hoare? Hoare probably! 1999. |
| [20] | Morgan, C. C.; McIver, A. K.; Seidel, K., Probabilistic predicate transformers, ACM Trans. Programming Languages Systems, 18, 3, 325-353 (1996) |
| [21] | Nelson, G., A generalization of Dijkstra’s calculus, ACM Trans. Programming Languages Systems, 11, 4, 517-561 (1989) |
| [22] | PSG (Probabilistic Systems Group) Collected Reports. http://www.comlab.ox.ac.uk/oucl/groups/probs/bibliography.html.; PSG (Probabilistic Systems Group) Collected Reports. http://www.comlab.ox.ac.uk/oucl/groups/probs/bibliography.html. |
| [23] | J.R. Rao, Building on the UNITY experience: compositionality, fairness and probability in parallelism, Ph.D. Thesis, University of Texas at Austin, Austin, TX, 1992.; J.R. Rao, Building on the UNITY experience: compositionality, fairness and probability in parallelism, Ph.D. Thesis, University of Texas at Austin, Austin, TX, 1992. |
| [24] | R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, 1995.; R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, 1995. |
| [25] | K. Seidel, C.C. Morgan, A.K. McIver, An introduction to probabilistic predicate transformers, Tech. Report PRG-TR-6-96, Programming Research Group, February 1996, Also available via http [23]; K. Seidel, C.C. Morgan, A.K. McIver, An introduction to probabilistic predicate transformers, Tech. Report PRG-TR-6-96, Programming Research Group, February 1996, Also available via http [23] |
| [26] | Smolka, S. A.; Gupta, G.; Bhaskar, S., On randomization in sequential and distributed systems, ACM Comput. Surveys, 26, 1, 7-86 (1994) |
| [27] | Trustrum, K., Linear Programming, Library of Mathematics (1971), Routledge & Kegan Paul: Routledge & Kegan Paul London · Zbl 0239.90028 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
