Reasoning about probabilistic sequential programs. (English) Zbl 1121.68028
Summary: A complete and decidable Hoare-style calculus for iteration-free probabilistic sequential programs is presented using a state logic with truth-functional propositional (not arithmetical) connectives.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B48 | Probability and inductive logic |
| 03B70 | Logic in computer science |
References:
| [1] | Abadi, M.; Halpern, J. Y., Decidability and expressiveness for first-order logics of probability, Information and Computation, 112, 1, 1-36 (1994) · Zbl 0799.03017 |
| [2] | Ambainis, A.; Mosca, M.; Tapp, A.; de Wolf, R., Private quantum channels, (FOCS’00: Proceedings of the 41st Annual Symposium on Foundations of Computer Science (2000), IEEE Computer Society), 547 |
| [3] | Baltazar, P.; Chadha, R.; Mateus, P.; Sernadas, A., Towards model-checking quantum security protocols, (Dini, P.; etal., Proceedings of the First Workshop on Quantum Security: QSec’07 (2007), IEEE Press), e-page 0014. Joint e-proceedings with Quantum, Nano, and Micro Technologies: ICQNM ’07 · Zbl 1273.03104 |
| [4] | Basu, S.; Pollack, R.; Marie-Françoise, R., Algorithms in Real Algebraic Geometry (2003), Springer Verlag · Zbl 1031.14028 |
| [5] | Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, Journal of Computer and System Sciences, 18, 251-264 (1986) · Zbl 0634.03031 |
| [6] | Caleiro, C.; Mateus, P.; Sernadas, A.; Sernadas, C., Quantum institutions, (Futatsugi, K.; Jouannaud, J.-P.; Meseguer, J., Algebra, Meaning, and Computation — Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday. Algebra, Meaning, and Computation — Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 4060 (2006), Springer Verlag), 50-64 · Zbl 1132.03354 |
| [7] | 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 · Zbl 1273.03104 |
| [8] | Chadha, R.; Mateus, P.; Sernadas, A., Reasoning about states of probabilistic sequential programs, (Ésik, Z., Computer Science Logic 2006 (CSL06). Computer Science Logic 2006 (CSL06), Lecture Notes in Computer Science, vol. 4207 (2006), Springer-Verlag), 240-255 · Zbl 1225.68112 |
| [9] | R. Chadha, P. Mateus, A. Sernadas, C. Sernadas, Extending classical logic for reasoning about quantum systems, CLC, Department of Mathematics, Instituto Superior Técnico, 2005. Invited submission to the Handbook of Quantum Logic. Preprint; R. Chadha, P. Mateus, A. Sernadas, C. Sernadas, Extending classical logic for reasoning about quantum systems, CLC, Department of Mathematics, Instituto Superior Técnico, 2005. Invited submission to the Handbook of Quantum Logic. Preprint · Zbl 1273.03172 |
| [10] | 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) · Zbl 1066.68081 |
| [11] | Fagin, R.; Halpern, J. Y.; Megiddo, N., A logic for reasoning about probabilities, Information and Computation, 87, 1-2, 78-128 (1990) · Zbl 0811.03014 |
| [12] | Feldman, Y. A., A decidable propositional dynamic logic with explicit probabilities, Information and Control, 63, 1-2, 11-38 (1984) · Zbl 0592.68031 |
| [13] | Feldman, Y. A.; Harel, D., A probabilistic dynamic logic, Journal of Computer and System Sciences, 28, 193-215 (1984) · Zbl 0537.68036 |
| [14] | Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects of Computing, 6, 512-535 (1995) · Zbl 0820.68113 |
| [15] | Hoare, C., An axiomatic basis for computer programming, Communications of the ACM, 12, 576-583 (1969) · Zbl 0179.23105 |
| [16] | Hodges, W., Model Theory (1993), Cambridge University Press · Zbl 0789.03031 |
| [17] | M. Huth, M. Kwiatkowska, Quantitative analysis and model checking, in: 12th Annual IEEE Symposium on Logic in Computer Science, LICS’97, 1997, pp. 111-122; M. Huth, M. Kwiatkowska, Quantitative analysis and model checking, in: 12th Annual IEEE Symposium on Logic in Computer Science, LICS’97, 1997, pp. 111-122 |
| [18] | C. Jones, Probabilistic non-determinism, Ph.D. Thesis, U. Edinburgh, 1990; C. Jones, Probabilistic non-determinism, Ph.D. Thesis, U. Edinburgh, 1990 |
| [19] | Jones, C.; Plotkin, G. D., A probabilistic powerdomain of evaluations, (Proceedings of the Fourth Annual Symposium on Logic in Computer Science (1989), IEEE Computer Society), 186-195 · Zbl 0716.06003 |
| [20] | Kozen, D., Semantics of probabilistic programs, Journal of Computer System Science, 22, 328-350 (1981) · Zbl 0476.68019 |
| [21] | Kozen, D., A probabilistic PDL, Journal of Computer System Science, 30, 162-178 (1985) · Zbl 0575.03013 |
| [22] | J.A. Makowsky, M.L. Tiomkin, Probabilistic propositional dynamic logic, 1980. Manuscript; J.A. Makowsky, M.L. Tiomkin, Probabilistic propositional dynamic logic, 1980. Manuscript · Zbl 0732.03022 |
| [23] | Mateus, P.; Sernadas, A., Weakly complete axiomatization of exogenous quantum propositional logic, Information and Computation, 204, 5, 771-794 (2006) · Zbl 1116.03021 |
| [24] | Mateus, P.; Sernadas, A.; Sernadas, C., Exogenous semantics approach to enriching logics, (Sica, G., Essays on the Foundations of Mathematics and Logic. Essays on the Foundations of Mathematics and Logic, Advanced Studies in Mathematics and Logic, vol. 1 (2005), Polimetrica), 165-194 · Zbl 1151.03324 |
| [25] | Morgan, C.; McIver, A.; Seidel, K., Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, 18, 3, 325-353 (1996) |
| [26] | Moshier, M. A.; Jung, A., A logic for probabilities in semantics, (Computer Science Logic. Computer Science Logic, Lecture Notes in Computer Science, vol. 2471 (2002), Springer Verlag), 216-231 · Zbl 1020.68050 |
| [27] | Narasimha, M.; Cleaveland, R.; Iyer, P., Probabilistic temporal logics via the modal mu-calculus, (Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, FOSSACS 99. Foundations of Software Science and Computation Structures. Foundations of Software Science and Computation Structures, FOSSACS 99, Lecture Notes in Computer Science, vol. 1578 (1999), Springer Verlag), 288-305 · Zbl 0933.03029 |
| [28] | Nilsson, N. J., Probabilistic logic, Artificial Intelligence, 28, 1, 71-87 (1986) · Zbl 0589.03007 |
| [29] | Nilsson, N. J., Probabilistic logic revisited, Artificial Intelligence, 59, 1-2, 39-42 (1993) · Zbl 1507.68015 |
| [30] | Parikh, R.; Mahoney, A., A theory of probabilistic programs, (Proceedings of the Carnegie Mellon Workshop on Logic of Programs. Proceedings of the Carnegie Mellon Workshop on Logic of Programs, Lecture Notes in Computer Science, vol. 64 (1983), Springer Verlag), 396-402 · Zbl 0558.68010 |
| [31] | L.H. Ramshaw, Formalizing the analysis of algorithms, Ph.D. Thesis, Stanford University, 1979; L.H. Ramshaw, Formalizing the analysis of algorithms, Ph.D. Thesis, Stanford University, 1979 |
| [32] | J.H. Reif, Logics for probabilistic programming (extended abstract), in: STOC’80: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, 1980, pp. 8-13; J.H. Reif, Logics for probabilistic programming (extended abstract), in: STOC’80: Proceedings of the Twelfth Annual ACM Symposium on Theory of Computing, 1980, pp. 8-13 |
| [33] | 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) · Zbl 1271.68004 |
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.
