Inferring expected runtimes of probabilistic integer programs using expected sizes. (English) Zbl 1467.68066
Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12651, 250-269 (2021).
Summary: We present a novel modular approach to infer upper bounds on the expected runtimes of probabilistic integer programs automatically. To this end, it computes bounds on the runtimes of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.
For the entire collection see [Zbl 1466.68015].
For the entire collection see [Zbl 1466.68015].
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
| 90C10 | Integer programming |
| 90C15 | Stochastic programming |
References:
| [1] | Agrawal, S., Chatterjee, K., Novotný, P.: Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL) (2017), doi:10.1145/3158122 |
| [2] | Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161-203 (2011), doi:10.1007/s10817-010-9174-1 · Zbl 1213.68200 |
| [3] | Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142-159 (2012), doi:10.1016/j.tcs.2011.07.009 · Zbl 1236.68042 |
| [4] | Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3) (2013), doi:10.1145/2499937.2499943 · Zbl 1353.68045 |
| [5] | Albert, E., Bofill, M., Borralleras, C., Martin-Martin, E., Rubio, A.: Resource analysis driven by (conditional) termination proofs. Theory Pract. Log. Program. 19(5-6), 722-739 (2019), doi:10.1017/S1471068419000152 · Zbl 1434.68101 |
| [6] | Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Proc. SAS ’10. LNCS, vol. 6337, pp. 117-133 (2010), doi:10.1007/978-3-642-15769-1_8 · Zbl 1306.68017 |
| [7] | Ash, R.B., Doléans-Dade, C.A.: Probability and Measure Theory. Harcourt Academic Press, 2nd edn. (2000) · Zbl 0944.60004 |
| [8] | Avanzini, M., Moser, G.: A combination framework for complexity. In: Proc. RTA 13. LIPIcs, vol. 21, pp. 55-70 (2013), doi:10.4230/LIPIcs.RTA.2013.55 · Zbl 1356.68092 |
| [9] | Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean Complexity Tool. In: Proc. TACAS ’16. LNCS, vol. 9636, pp. 407-423 (2016), doi:10.1007/978-3-662-49674-9_24 |
| [10] | Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA) (2020), doi:10.1145/3428240 |
| [11] | Avanzini, M., Dal Lago, U., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185 (2020), doi:10.1016/j.scico.2019.102338 · Zbl 1507.68140 |
| [12] | Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4) (2014), doi:10.1145/2629488 · Zbl 1321.68296 |
| [13] | Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Proc. CAV ’17. LNCS, vol. 10427, pp. 601-620 (2017), doi:10.1007/978-3-319-63390-9_32 · Zbl 1494.68049 |
| [14] | Ben-Amram, A.M., Doménech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Proc. SAS ’19. LNCS, vol. 11822, pp. 459-480 (2019), doi:10.1007/978-3-030-32304-2_22 · Zbl 1539.68058 |
| [15] | Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proc. RTA ’05. LNCS, vol. 3467, pp. 323-337 (2005), doi:10.1007/978-3-540-32033-3_24 · Zbl 1078.68057 |
| [16] | Bournez, O., Garnier, F.: Proving positive almost sure termination under strategies. In: Proc. RTA ’06. LNCS, vol. 4098, pp. 357-371 (2006), doi:10.1007/11805618_27 · Zbl 1151.68441 |
| [17] | Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Proc. CAV ’05. LNCS, vol. 3576, pp. 491-504 (2005), doi:10.1007/11513988_48 · Zbl 1081.68611 |
| [18] | Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4) (2016), doi:10.1145/2866575 |
| [19] | Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44-67 (1977), doi:10.1145/321992.321996 · Zbl 0343.68014 |
| [20] | Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proc. PLDI ’15. pp. 467-478 (2015), doi:10.1145/2737924.2737955 |
| [21] | Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: CAV ’17. LNCS, vol. 10427, pp. 64-85 (2017), doi:10.1007/978-3-319-63390-9_4 · Zbl 1494.68051 |
| [22] | Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Proc. CAV ’13. LNCS, vol. 8044, pp. 511-526 (2013), doi:10.1007/978-3-642-39799-8_34 |
| [23] | Chatterjee, K., Novotný, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Proc. POPL ’17. pp. 145-160 (2017), doi:10.1145/3093333.3009873 · Zbl 1380.68114 |
| [24] | Chatterjee, K., Fu, H., Novotný, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40(2) (2018), doi:10.1145/3174800 · Zbl 1347.68075 |
| [25] | Chatterjee, K., Fu, H., Novotný, P.: Termination analysis of probabilistic programs with martingales. In: Barthe, G., Katoen, J., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 221—258. Cambridge University Press (2020), doi:10.1017/9781108770750.008 · Zbl 07311047 |
| [26] | Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: Proc. POPL ’15. pp. 489-501 (2015), doi:10.1145/2676726.2677001 · Zbl 1345.68104 |
| [27] | Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Proc. APLAS ’14. LNCS, vol. 8858, pp. 275-295 (2014), doi:10.1007/978-3-319-12736-1_15 · Zbl 1453.68047 |
| [28] | Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Proc. FM ’16. LNCS, vol. 9995, pp. 254-273 (2016), doi:10.1007/978-3-319-48989-6_16 |
| [29] | Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Proc. VMCAI ’19. LNCS, vol. 11388, pp. 468-490 (2019), doi:10.1007/978-3-030-11245-5_22 · Zbl 1522.68152 |
| [30] | Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3-31 (2017), doi:10.1007/s10817-016-9388-y · Zbl 1409.68255 |
| [31] | Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Proc. TACAS ’19. LNCS, vol. 11429, pp. 156-166 (2019), doi:10.1007/978-3-030-17502-3_10 |
| [32] | Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Proc. CADE ’19. LNAI, vol. 11716, pp. 269-286 (2019), doi:10.1007/978-3-030-29436-6_16 · Zbl 1535.68047 |
| [33] | Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: Induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL) (2020), doi:10.1145/3371105 |
| [34] | Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3) (2012), doi:10.1145/2362389.2362393 · Zbl 1284.68132 |
| [35] | Hoffmann, J., Shao, Z.: Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25 (2015), doi:10.1017/S0956796815000192 · Zbl 1420.68068 |
| [36] | Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: Proc. POPL ’17. pp. 359-373 (2017), doi:10.1145/3009837.3009842 · Zbl 1380.68123 |
| [37] | Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: Proc. APLAS ’18. LNCS, vol. 11275, pp. 181-201 (2018), doi:10.1007/978-3-030-02768-1_11 · Zbl 1519.68052 |
| [38] | Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang. 3(OOPSLA) (2019), doi:10.1145/3360555 |
| [39] | Jeannet, B., Miné, A.: Apron: A library of numerical abstract domains for static analysis. In: Proc. CAV ’09. pp. 661-667 (2009), doi:10.1007/978-3-642-02658-4_52 |
| [40] | Kallenberg, O.: Foundations of Modern Probability. Springer, New York (2002), doi:10.1007/978-1-4757-4015-8 · Zbl 0996.60001 |
| [41] | Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65 (2018), doi:10.1145/3208102 · Zbl 1426.68298 |
| [42] | Kaminski, B.L., Katoen, J., Matheja, C.: Expected runtime analyis by program verification. In: Barthe, G., Katoen, J., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 185—220. Cambridge University Press (2020), doi:10.1017/9781108770750.007 · Zbl 07311046 |
| [43] | KoAT: Web interface, binary, Docker image, and examples available at the web site https://aprove-developers.github.io/ExpectedUpperBounds/. The source code is available at https://github.com/aprove-developers/KoAT2-Releases/tree/probabilistic. |
| [44] | Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328-350 (1981), doi:10.1016/0022-0000(81)90036-2 · Zbl 0476.68019 |
| [45] | McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005), doi:10.1007/b138392 · Zbl 1069.68039 |
| [46] | McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL) (2018), doi:10.1145/3158121 |
| [47] | Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. CoRR abs/2010.06367 (2020), https://arxiv.org/abs/2010.06367 · Zbl 1467.68066 |
| [48] | Moosbrugger, M., Bartocci, E., Katoen, J., Kovács, L.: Automated termination analysis of polynomial probabilistic programs. In: Proc. ESOP ’21. LNCS (2021), to appear. · Zbl 1473.68053 |
| [49] | de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proc. TACAS ’08. LNCS, vol. 4963, pp. 337-340 (2008), doi:10.1007/978-3-540-78800-3_24 |
| [50] | Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: Proc. PLDI ’18. pp. 496-512 (2018), doi:10.1145/3192366.3192394, tool artifact and benchmarks available from https://channgo2203.github.io/zips/tool_benchmark.zip |
| [51] | Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning 51(1), 27-56 (2013), doi:10.1007/s10817-013-9277-6 · Zbl 1314.68174 |
| [52] | Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about recursive probabilistic programs. In: Proc. LICS ’16. pp. 672-681 (2016), doi:10.1145/2933575.2935317 · Zbl 1401.68048 |
| [53] | Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proc. VMCAI ’04. LNCS, vol. 2937, pp. 239-251 (2004), doi:10.1007/978-3-540-24622-0_20 · Zbl 1202.68109 |
| [54] | Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons (2005) · Zbl 1184.90170 |
| [55] | RaML (Resource Aware ML), https://www.raml.co/interface/ |
| [56] | Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Proc. SAS ’04. LNCS, vol. 3148, pp. 53-68 (2004), doi:10.1007/978-3-540-27864-1_7 · Zbl 1104.68023 |
| [57] | Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning 59(1), 3-45 (2017), doi:10.1007/s10817-016-9402-4 · Zbl 1409.68076 |
| [58] | Srikanth, A., Sahin, B., Harris, W.R.: Complexity verification using guided theorem enumeration. In: Proc. POPL ’17. pp. 639-652 (2017), doi:10.1145/3009837.3009864 · Zbl 1380.68284 |
| [59] | TPDB (Termination Problems Data Base), http://termination-portal.org/wiki/TPDB |
| [60] | Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. FOCS ’85. pp. 327-338 (1985), doi:10.1109/SFCS.1985.12 |
| [61] | Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating expected cost analysis with types. Proc. ACM Program. Lang. 4(ICFP) (2020), doi:10.1145/3408992 |
| [62] | Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: Proc. PLDI ’19. pp. 204-220 (2019), doi:10.1145/3314221.3314581 |
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.
