Abstract
A complete and decidable propositional logic for reasoning about states of probabilistic sequential programs is presented. The state logic is then used to obtain a sound Hoare-style calculus for basic probabilistic sequential programs. The Hoare calculus presented herein is the first probabilistic Hoare calculus with a complete and decidable state logic that has truth-functional propositional (not arithmetical) connectives. The models of the state logic are obtained exogenously by attaching sub-probability measures to valuations over memory cells. In order to achieve complete and recursive axiomatization of the state logic, the probabilities are taken in arbitrary real closed fields.
Supported by FCT and FEDER through POCI via CLC QuantLog POCI/MAT/ 55796/2004 Project. Additional support for Rohit Chadha came from FCT and FEDER grant SFRH/BPD/26137/2005.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Halpern, J.Y.: Decidability and expressiveness for first-order logics of probability. Information and Computation 112(1), 1–36 (1994)
Ambainis, A., Mosca, M., Tapp, A., de Wolf, R.: Private quantum channels. In: FOCS 2000: Proceedings of the 41st Annual Symposium on Foundations of Computer Science, p. 547. IEEE Computer Society Press, Los Alamitos (2000)
Basu, S., Pollack, R., Marie-Françoise, R.: Algorithms in Real Algebraic Geometry. Springer, Heidelberg (2003)
Chadha, R., Mateus, P., Sernadas, A.: Reasoning about quantum imperative programs. Electronic Notes in Theoretical Computer Science 158, 19–40 (2006) (Invited talk at the Twenty-Second Conference on the Mathematical Foundations of Programming Semantics)
Chadha, R., Mateus, P., Sernadas, A., Sernadas, C.: Extending classical logic for reasoning about quantum systems. CLC, Department of Mathematics, Instituto Superior Técnico (preprint, 2005) (Invited submission to the Handbook of Quantum Logic)
den Hartog, J.I., de Vink, E.P.: Verifying probabilistic programs using a hoare like logic. International Journal of Foundations of Computer Science 13(3), 315–340 (2002)
Fagin, R., Halpern, J.Y., Megiddo, N.: A logic for reasoning about probabilities. Information and Computation 87(1-2), 78–128 (1990)
Feldman, Y.A.: A decidable propositional dynamic logic with explicit probabilities. Information and Control 63(1/2), 11–38 (1984)
Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. Journal of Computer and System Sciences 28, 193–215 (1984)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1995)
Hoare, C.: An axiomatic basis for computer programming. Communications of the ACM 12, 576–583 (1969)
Hodges, W.: Model Theory. Cambridge University Press, Cambridge (1993)
Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997), pp. 111–122 (1997)
Jones, C.: Probabilistic Non-determinism. PhD thesis, U. Edinburgh (1990)
Jones, C., Plotkin, G.D.: A probabilistic powerdomain of evaluations. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 186–195. IEEE Computer Society Press, Los Alamitos (1989)
Kozen, D.: Semantics of probabilistic programs. Journal of Computer System Science 22, 328–350 (1981)
Kozen, D.: A probabilistic PDL. Journal of Computer System Science 30, 162–178 (1985)
Makowsky, J.A., Tiomkin, M.L.: Probabilistic propositional dynamic logic (manuscript, 1980)
Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Information and Computation (to appear)
Mateus, P., Sernadas, A., Sernadas, C.: Exogenous semantics approach to enriching logics. In: Essays on the Foundations of Mathematics and Logic. Advanced Studies in Mathematics and Logic, vol. 1, pp. 165–194. Polimetrica (2005)
Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)
Moshier, M.A., Jung, A.: A logic for probabilities in semantics. In: Bradfield, J.C. (ed.) CSL 2002. LNCS, vol. 2471, pp. 216–231. Springer, Heidelberg (2002)
Narasimha, M., Cleaveland, W.R., Iyer, P.: Probabilistic temporal logics via the modal mu-calculus. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 288–305. Springer, Heidelberg (1999)
Nilsson, N.J.: Probabilistic logic. Artificial Intelligence 28(1), 71–87 (1986)
Nilsson, N.J.: Probabilistic logic revisited. Artificial Intelligence 59(1-2), 39–42 (1993)
Parikh, R., Mahoney, A.: A theory of probabilistic programs. In: Proceedings of the Carnegie Mellon Workshop on Logic of Programs. LNCS, vol. 64, pp. 396–402. Springer, Heidelberg (1983)
Ramshaw, L.H.: Formalizing the analysis of algorithms. PhD thesis, Stanford University (1979)
Reif, J.H.: Logics for probabilistic programming (extended abstract). In: STOC 1980: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, pp. 8–13 (1980)
Tix, R., Keimel, K., Plotkin, G.D.: Semantic domains for combining probability and non-determinism. Electronic Notes in Theoretical Computer Science 129, 1–104 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chadha, R., Mateus, P., Sernadas, A. (2006). Reasoning About States of Probabilistic Sequential Programs. In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_16
Download citation
DOI: https://doi.org/10.1007/11874683_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)