×

On the hardness of analyzing probabilistic programs. (English) Zbl 1417.68054

Summary: We study the hardness of deciding probabilistic termination as well as the hardness of approximating expected values (e.g. of program variables) and (co)variances for probabilistic programs.
Termination We distinguish two notions of probabilistic termination: Given a program \(P\) and an input \(\sigma \dots\) cm
1.
\(\dots\)does \(P\) terminate with probability 1 on input \(\sigma\)? (almost-sure termination)
2.
\(\dots\)is the expected time until \(P\) terminates on input \(\sigma \) finite? (positive almost-sure termination)
For both of these notions, we also consider their universal variant, i.e. given a program \(P\), does \(P\) terminate on all inputs? We show that deciding almost-sure termination as well as deciding its universal variant is \(\varPi^0_2\)-complete in the arithmetical hierarchy. Deciding positive almost-sure termination is shown to be \(\varSigma_2^0\)-complete, whereas its universal variant is \(\varPi_3^0\)-complete.
Expected values Given a probabilistic program \(P\) and a random variable \(f\) mapping program states to rationals, we show that computing lower and upper bounds on the expected value of \(f\) after executing \(P\) is \(\varSigma_1^0\)- and \(\varSigma_2^0\)-complete, respectively. Deciding whether the expected value equals a given rational value is shown to be \(\varPi^0_2\)-complete.
Covariances We show that computing upper and lower bounds on the covariance of two random variables is both \(\varSigma_2^0\)-complete. Deciding whether the covariance equals a given rational value is shown to be in \(\varDelta_3^0\). In addition, this problem is shown to be \(\varSigma^0_2\)-hard as well as \(\varPi^0_2\)-hard and thus a “proper” \(\varDelta_3^0\)-problem. All hardness results on covariances apply to variances as well.

MSC:

68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Arons, T., Pnueli, A., Zuck, L.D.: Parameterized Verification by Probabilistic Abstraction. In: FoSSaCS, LNCS, vol. 2620, pp. 87-102. Springer (2003) · Zbl 1029.68104
[2] Ash, R.B., Doleans-Dade, C.: Probability and Measure Theory. Academic Press, Cambridge (2000) · Zbl 0944.60004
[3] Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst. 35(3), 9 (2013) · Zbl 1321.68182 · doi:10.1145/2492061
[4] Bläser, M., Manthey, B.: Smoothed complexity theory. TOCT 7(2), 6:1-6:21 (2015) · Zbl 1347.68155 · doi:10.1145/2656210
[5] Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proceedings of 16th International Conference on Term Rewriting and Applications, RTA 2005, Nara, Japan, April 19-21, 2005,LNCS, vol. 3467, pp. 323-337. Springer (2005) · Zbl 1078.68057
[6] Bournez, O., Hoyrup, M.: Rewriting logic and probabilities. In: RTA, LNCS, vol. 2706, pp. 61-75. Springer (2003) · Zbl 1038.68063
[7] Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, LNCS, vol. 8044, pp. 511-526. Springer (2013)
[8] Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz’s. In: CAV (1), LNCS, vol. 9779, pp. 3-22. Springer (2016) · Zbl 1411.68025
[9] Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: POPL, pp. 327-342. ACM (2016) · Zbl 1347.68075
[10] Davis, M.D.: Computability and Unsolvability. McGraw-Hill Series in Information Processing and Computers. McGraw-Hill, New York (1958)
[11] Davis, M.D.: Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science. Academic Press, Cambridge (1994)
[12] Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976) · Zbl 0368.68005
[13] Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: CAV, LNCS, vol. 7358, pp. 123-138. Springer (2012)
[14] Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL 2015, pp. 489-501. ACM (2015) · Zbl 1345.68104
[15] Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: ESOP, LNCS, vol. 9632, pp. 282-309. Springer (2016) · Zbl 1335.68027
[16] Gill, J.: Computational complexity of probabilistic turing machines. SIAM J. Comput. 6(4), 675-695 (1977) · Zbl 0366.02024 · doi:10.1137/0206049
[17] Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: Future of Software Engineering (FOSE), pp. 167-181. ACM (2014)
[18] Gretz, F., Katoen, J.P., McIver, A.: Operational versus Weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110-132 (2014) · doi:10.1016/j.peva.2013.11.004
[19] Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent programs. TOPLAS 5(3), 356-380 (1983) · Zbl 0511.68009 · doi:10.1145/2166.357214
[20] Jansen, N., Kaminski, B.L., Katoen, J.P., Olmedo, F., Gretz, F., McIver, A.: Conditioning in probabilistic programming. ENTCS 319, 199-216 (2015) · Zbl 1351.68066
[21] Kaminski, B.L., Katoen, J.P.: On the hardness of almost – sure termination. In: Proceedings of MFCS 2015, Part I, LNCS, vol. 9234, pp. 307-318. Springer (2015) · Zbl 1465.68097
[22] Kaminski, B.L., Katoen, J.P., Matheja, C.: Inferring covariances for probabilistic programs. In: QEST 2016, pp. 191-206 (2016) · Zbl 1377.68070
[23] Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. (2016). arXiv:1601.01001 · Zbl 1335.68058
[24] Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run-times of probabilistic programs. In: ESOP, LNCS, vol. 9632, pp. 364-389. Springer (2016) · Zbl 1335.68058
[25] Katoen, J., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: SAS, LNCS, vol. 6337, pp. 390-406. Springer (2010) · Zbl 1239.68020
[26] Kleene, S.C.: Recursive predicates and quantifiers. Trans. AMS 53(1), 41-73 (1943) · Zbl 0063.03259 · doi:10.1090/S0002-9947-1943-0007371-8
[27] Klenke, A.: Probability Theory: A Comprehensive Course. Springer, Berlin (2013) · Zbl 1141.60001
[28] Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328-350 (1981) · Zbl 0476.68019 · doi:10.1016/0022-0000(81)90036-2
[29] Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162-178 (1985) · Zbl 0575.03013 · doi:10.1016/0022-0000(85)90012-1
[30] dal Lago, U., Grellois, C.: Probabilistic termination by monadic affine sized typing. In: ESOP, LNCS, vol. 10201, pp. 393-419. Springer (2017) · Zbl 1485.68045
[31] McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, Berlin (2004) · Zbl 1069.68039
[32] McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. In: POPL [to appear] (2018)
[33] Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Refinement Workshop, Workshops in Computing, p. 7. Springer Verlag (1996)
[34] Murawski, A., Ouaknine, J.: On probabilistic program equivalence and refinement. In: CONCUR, LNCS, vol. 3653, pp. 156-170. Springer (2005) · Zbl 1134.68351
[35] Odifreddi, P.: Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers. Elsevier, Amsterdam (1992) · Zbl 0744.03044
[36] Odifreddi, P.: Classical Recursion Theory, vol. II. Elsevier, Amsterdam (1999) · Zbl 0931.03057
[37] Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Boston (1994) · Zbl 0833.68049
[38] Post, E.L.: Recursively enumerable sets of positive integers and their decision problems. Bull. AMS 50(5), 284-316 (1944) · Zbl 0063.06328 · doi:10.1090/S0002-9904-1944-08111-1
[39] Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (2005) · Zbl 1184.90170
[40] Rogers, H.: Theory of Recursive Functions and Effective Computability, vol. 5. McGraw-Hill, New York (1967) · Zbl 0183.01401
[41] Sharir, M., Pnueli, A., Hart, S.: Verification of probabilistic programs. SIAM J. Comput. 13(2), 292-314 (1984). https://doi.org/10.1137/0213021 · Zbl 0533.68012 · doi:10.1137/0213021
[42] Sneyers, J., de Schreye, D.: Probabilistic termination of CHRiSM Programs. In: LOPSTR, LNCS, vol. 7225, pp. 221-236. Springer (2011) · Zbl 1377.68067
[43] Tiomkin, M.L.: Probabilistic termination versus fair termination. TCS 66(3), 333-340 (1989) · Zbl 0679.68028 · doi:10.1016/0304-3975(89)90158-8
[44] Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2011) · doi:10.1145/2049706.2049708
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.