For probabilistic programs, there is some work for qualitative and quantitative analysis about expectation or mean, such as expected termination time, and expected cost analysis. However, another non-trivial issue is about tail bounds (i.e., upper bounds of tail probabilities), which can provide high-probability guarantees to extreme events. In this work, we focus on the problem of tail-bound cost analysis over nondeterministic probabilistic programs, which aims to automatically obtain the tail bound of resource usages over such programs. To achieve this goal, we present a novel approach, combined with a suitable concentration inequality, to derive the tail bound of accumulated cost until program termination. Our approach can handle both positive and negative costs. Moreover, our approach enables an automated template-based synthesis of supermartingales and leads to an efficient polynomial-time algorithm. To show the effectiveness of our approach, we present experimental results on various programs and make a comparison with state-of-the-art tools.
[1] GORDON A D, HENZINGER T A, NORI A V, et al. Probabilistic programming [C]// Future of Software Engineering Proceedings. New York: ACM, 2014: 167- 181.
[2] FOSTER N, KOZEN D, MAMOURSA K, et al. Probabilistic NetKAT [M]// Programming languages and systems. Berlin, Heidelberg: Springer, 2016: 282-309.
[3] SMOLKA S, KUMAR P, FOSTER N et al. Cantor meets Scott: Semantic foundations for probabilistic networks [C]//44th ACM SIGPLAN Symposium on Principles of Programming Languages. Paris: ACM, 2017: 557-571.
[4] KAHN D M. Undecidable problems for probabilistic network programming [C]//42nd International Symposium on Mathematical Foundations of Computer Science. Aalborg: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017: 68.
[5] ROY D, MANSINGHKA V, GOODMAN N, et al. A stochastic programming perspective on nonparametric Bayes [C]//25th International Conference on Machine Learning. Helsinki: ACM, 2008: 1-3.
[6] GORDON A D, AIZATULIN M, BORGSTROM J, et al. A model-learner pattern for Bayesian reasoning [C]//40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Rome: ACM, 2013: 403-416.
[7] ′ SCIBIOR A, GHAHRAMANI Z, GORDON A D. Practical probabilistic programming with monads [C]//2015 ACM SIGPLAN Symposium on Haskell. Vancouver: ACM, 2015: 165-176.
[8] CLARET G, RAJAMANI S K, NORI A V, et al. Bayesian inference using data flow analysis [C]//9th Joint Meeting on Foundations of Software Engineering. Saint Petersburg: ACM, 2013: 92-102.
[9] THRUN S. Probabilistic algorithms in robotics [J]. AI Magazine, 2000, 21(4): 93-109.
[10] THRUN S. Probabilistic robotics [J]. Communications of the ACM, 2002, 45(3): 52-57.
[11] JIANG X, COOPER G F. A Bayesian spatio-temporal method for disease outbreak detection [J]. Journal of the American Medical Informatics Association, 2010, 17(4): 462-471.
[12] BARTHE G, K?PF B, OLMEDO F, et al. Probabilistic relational reasoning for differential privacy [J]. ACM Transactions on Programming Languages and Systems, 2013, 35(3): 9.
[13] MANFREDI G, JESTIN Y. An introduction to ACAS Xu and the challenges ahead [C]//2016 IEEE/AIAA 35th Digital Avionics Systems Conference. Sacramento: IEEE, 2016: 1-9.
[14] CHAKAROV A, SANKARANARAYANAN S. Probabilistic program analysis with martingales [M]// Computer aided verification. Berlin, Heidelberg: Springer, 2013: 511-526.
[15] WANG D, HOFFMANN J, REPS T. PMAF: An algebraic framework for static analysis of probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 513-528.
[16] NGO V C, CARBONNEAUX Q, HOFFMANN J. Bounded expectations: Resource analysis for probabilistic programs [C]//39th ACM SIGPLAN Conference on Programming Language Design and Implementation. Philadelphia: ACM, 2018: 496-512.
[17] AGRAWAL S, CHATTERJEE K, NOVOTN′ Y P. Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 1-32.
[18] CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [C]//43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. St. Petersburg, FL: ACM, 2016: 327–342.
[19] CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [M]//Computer aided verification. Cham: Springer, 2016: 3-22.
[20] ESPARZA J, GAISER A, KIEFER S. Proving termination of probabilistic programs using patterns [M]//Computer aided verification. Cham: Springer, 2012: 123-138.
[21] KAMINSKI B L, KATOEN J-P, MATHEJA C, et al. Weakest precondition reasoning for expected runtimes of probabilistic programs [M]//Programming languages and systems. Berlin, Heidelberg: Springer, 2016: 364-389.
[22] KAMINSKI B L, KATOEN J-P, MATHEJA C. On the hardness of analyzing probabilistic programs [J]. Acta Informatica, 2019, 56(3): 255-285.
[23] COUSOT P, COUSOT R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints [C]//4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Los Angeles: ACM, 1977: 238-252.[24] RUBINSTEIN R Y, KROESE D P. Simulation and the Monte Carlo method [M]. Hoboken: John Wiley & Sons, 2016.
[25] BATZ K, KAMINSKI B L, KATOEN J, et al. How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times [M]//Programming languages and systems. Cham: Springer, 2018: 186-213.
[26] WANG P, FU H, GOHARSHADY A K, et al. Cost analysis of nondeterministic probabilistic programs [C]//40th ACM SIGPLAN Conference on Programming Language Design and Implementation. Phoenix, AZ: ACM,2019: 204-220.
[27] KURA S, URABE N, HASUO I. Tail probabilities for randomized program runtimes via martingales for higher moments [M]//Tools and algorithms for the construction and analysis of systems. Cham: Springer, 2019: 135-153.
[28] WANG D, HOFFMANN J, REPS T. Tail bound analysis for probabilistic programs via central moments [J/OL]. (2020-01-28). https://arxiv.org/abs/2001.10150.
[29] WILLIAMS D. Probability with martingales [M]. Cambridge: Cambridge University Press, 1991.
[30] CHATTERJEE K, FU H, NOVOTN′ Y P, et al. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs [J]. ACM Transactions on Programming Languages and Systems, 2018, 40(2): 7.
[31] CHATTERJEE K, FU H, GOHARSHADY A K. Termination analysis of probabilistic programs through positivstellensatz’s [EB/OL]. (2016-04-25). http://arxiv.org/abs/1604.07169.
[32] MEYN S, TWEEDIE R. Markov chains and stochastic stability [M]. London: Springer, 1993.
[33] FIORITI L M F, HERMANNS H. Probabilistic termination: Soundness, completeness, and compositionality [C]//42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Mumbai: ACM, 2015: 489-501.
[34] WANG P, FU H, CHATTERJEE K, et al. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time [J]. Proceedings of the ACM on Programming Languages, 2020, 4(POPL): 25.
[35] NAKAMOTO S. Bitcoin: A peer-to-peer electronic cash system [EB/OL].
[2020-09-24]. https://bitcoin.org/bitcoin.pdf.
[36] DE VRIES A. Bitcoin’s growing energy problem [J]. Joule, 2018, 2(5): 801-805.
[37] ABATE A, KATOEN J, LYGEROS J, et al. Approximate model checking of stochastic hybrid systems [J]. European Journal of Control, 2010, 16(6): 624-641.
[38] FU H, CHATTERJEE K. Termination of nondeterministic probabilistic programs [M]//Verification, model checking, and abstract interpretation. Cham: Springer, 2019: 468-490.
[39] HOEFFDING W. Probability inequalities for sums of bounded random variables [M]//The collected works of Wassily Hoeffding. New York: Springer, 1994: 409- 426.
[40] CHATTERJEE K, FU H, GOHARSHADY A K, et al. Computational approaches for stochastic shortest path on succinct MDPs [C]//Proceedings of the 27th International Joint Conference on Artificial Intelligence. Stockholm: AAAI Press, 2018: 4700-4707.
[41] FENG Y, ZHANG L, JANSEN D N, et al. Finding polynomial loop invariants for probabilistic programs [M]//Automated technology for verification and analysis. Cham: Springer, 2017: 400-416.
[42] FARKAS J. A fourier-f′ele mechanikai elv alkalmaz′asai [J]. Mathematikai′es Term′eszettudom′anyi ′ Ertesit¨o, 1894, 12: 457-472 (in Hungarian).
[43] BARTHE G, ESPITAU T, GR′ EGOIRE B, et al. Proving expected sensitivity of probabilistic programs [J]. Proceedings of the ACM on Programming Languages, 2018, 2(POPL): 57.
[44] LETAN T, R′ EGIS-GIANAS Y, CHIFFLIER P, et al. Modular verification of programs with effects and effect handlers in Coq [M]//Formal methods. Cham: Springer, 2018: 338-354.
