{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T10:06:10Z","timestamp":1764842770611,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031377082"},{"type":"electronic","value":"9783031377099"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Probabilistic recurrence relations (PRRs) are a standard formalism for describing the runtime of a randomized algorithm. Given a PRR and a time limit <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\kappa $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03ba<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, we consider the tail probability <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\Pr [T \\ge \\kappa ]$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>Pr<\/mml:mo>\n                    <mml:mo>[<\/mml:mo>\n                    <mml:mi>T<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mi>\u03ba<\/mml:mi>\n                    <mml:mo>]<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, i.e., the probability that the randomized runtime <jats:italic>T<\/jats:italic> of the PRR exceeds <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\kappa $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03ba<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Our focus is the formal analysis of tail bounds that aims at finding a tight asymptotic upper bound <jats:inline-formula><jats:alternatives><jats:tex-math>$$u \\ge \\Pr [T\\ge \\kappa ]$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>u<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mo>Pr<\/mml:mo>\n                    <mml:mo>[<\/mml:mo>\n                    <mml:mi>T<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mi>\u03ba<\/mml:mi>\n                    <mml:mo>]<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. To address this problem, the classical and most well-known approach is the cookbook method by Karp (JACM 1994), while other approaches are mostly limited to deriving tail bounds of specific PRRs via involved custom analysis.\n<\/jats:p><jats:p>In this work, we propose a novel approach for deriving the common exponentially-decreasing tail bounds for PRRs whose preprocessing time and random passed sizes observe discrete or (piecewise) uniform distribution and whose recursive call is either a single procedure call or a divide-and-conquer. We first establish a theoretical approach via Markov\u2019s inequality, and then instantiate the theoretical approach with a template-based algorithmic approach via a refined treatment of exponentiation. Experimental evaluation shows that our algorithmic approach is capable of deriving tail bounds that are (i) asymptotically tighter than Karp\u2019s method, (ii) match the best-known manually-derived asymptotic tail bound for QuickSelect, and (iii) is only slightly worse (with a <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\log \\log n$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>log<\/mml:mo>\n                    <mml:mo>log<\/mml:mo>\n                    <mml:mi>n<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> factor) than the manually-proven optimal asymptotic tail bound for QuickSort. Moreover, our algorithmic approach handles all examples (including realistic PRRs such as QuickSort, QuickSelect, DiameterComputation, etc.) in less than 0.1\u00a0s, showing that our approach is efficient in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-37709-9_2","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"16-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Automated Tail Bound Analysis for\u00a0Probabilistic Recurrence Relations"],"prefix":"10.1007","author":[{"given":"Yican","family":"Sun","sequence":"first","affiliation":[]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Achatz, M., McCallum, S., Weispfenning, V.: Deciding polynomial-exponential problems. In: Sendra, J.R., Gonz\u00e1lez-Vega, L. (eds.) Symbolic and Algebraic Computation, International Symposium, ISSAC 2008, Linz\/Hagenberg, Austria, July 20\u201323, 2008, Proceedings, pp. 215\u2013222. ACM (2008). https:\/\/doi.org\/10.1145\/1390768.1390799","DOI":"10.1145\/1390768.1390799"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J.P., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434333","DOI":"10.1145\/3434333"},{"key":"2_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"POPL","key":"2_CR4","doi-asserted-by":"publisher","first-page":"1957","DOI":"10.1145\/3571260","volume":"7","author":"K Batz","year":"2023","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.P., Matheja, C., Verscht, L.: A calculus for amortized expected runtimes. Proc. ACM Program. Lang. 7(POPL), 1957\u20131986 (2023). https:\/\/doi.org\/10.1145\/3571260","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"2_CR6","unstructured":"Billingsley, P.: Probability and Measure, 3rd edn. Wiley, New York (1995)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CAV, pp. 511\u2013526 (2013)","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"2_CR8","unstructured":"Chatterjee, K., Fu, H.: Termination of nondeterministic recursive probabilistic programs. CoRR abs\/1701.02944 (2017)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-63387-9_6","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2017","unstructured":"Chatterjee, K., Fu, H., Murhekar, A.: Automated recurrence analysis for almost-linear expected-runtime bounds. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 118\u2013139. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_6"},{"issue":"2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3174800","volume":"40","author":"K Chatterjee","year":"2018","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. TOPLAS 40(2), 7:1-7:45 (2018)","journal-title":"TOPLAS"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 55\u201378. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Stochastic invariants for probabilistic termination. In: POPL 2017, pp. 145\u2013160 (2017)","DOI":"10.1145\/3093333.3009873"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0304-3975(96)00261-7","volume":"181","author":"S Chaudhuri","year":"1997","unstructured":"Chaudhuri, S., Dubhashi, D.P.: Probabilistic recurrence relations revisited. Theoret. Comput. Sci. 181(1), 45\u201356 (1997)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR14","unstructured":"Goodman, N.D., Mansinghka, V.K., Roy, D., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: UAI 2008, pp. 220\u2013229. AUAI Press (2008)"},{"issue":"1","key":"2_CR15","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1239\/jap\/1032192549","volume":"35","author":"R Gr\u00fcbel","year":"1998","unstructured":"Gr\u00fcbel, R.: Hoare\u2019s selection algorithm: a Markov chain approach. Journal of Applied Probability 35(1), 36\u201345 (1998). http:\/\/www.jstor.org\/stable\/3215544","journal-title":"Journal of Applied Probability"},{"issue":"7","key":"2_CR16","first-page":"321","volume":"4","author":"CAR Hoare","year":"1961","unstructured":"Hoare, C.A.R.: Algorithm 64: quicksort. Commun. ACM 4(7), 321 (1961)","journal-title":"Commun. ACM"},{"issue":"7","key":"2_CR17","first-page":"321","volume":"4","author":"CAR Hoare","year":"1961","unstructured":"Hoare, C.A.R.: Algorithm 65: find. Commun. ACM 4(7), 321\u2013322 (1961)","journal-title":"Commun. ACM"},{"issue":"301","key":"2_CR18","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: APLAS, pp. 181\u2013201 (2018)","DOI":"10.1007\/978-3-030-02768-1_11"},{"issue":"5","key":"2_CR20","doi-asserted-by":"publisher","first-page":"30:1","DOI":"10.1145\/3208102","volume":"65","author":"BL Kaminski","year":"2018","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1-30:68 (2018). https:\/\/doi.org\/10.1145\/3208102","journal-title":"J. ACM"},{"issue":"6","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1145\/195613.195632","volume":"41","author":"RM Karp","year":"1994","unstructured":"Karp, R.M.: Probabilistic recurrence relations. J. ACM 41(6), 1136\u20131150 (1994)","journal-title":"J. ACM"},{"key":"2_CR22","unstructured":"Kleinberg, J.M., Tardos, \u00c9.: Algorithm Design. Addison-Wesley (2006)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-17465-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kura","year":"2019","unstructured":"Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 135\u2013153. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8"},{"key":"2_CR24","unstructured":"McConnell, J.J. (ed.): The Analysis of Algorithms: An Active Learning Approach. Jones & Bartlett Learning (2001)"},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1006\/jagm.1996.0055","volume":"21","author":"C McDiarmid","year":"1996","unstructured":"McDiarmid, C., Hayward, R.: Large deviations for quicksort. J. Algorithms 21(3), 476\u2013507 (1996)","journal-title":"J. Algorithms"},{"key":"2_CR26","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075","volume-title":"Randomized Algorithms","author":"R Motwani","year":"1995","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)"},{"key":"2_CR27","volume-title":"Real and Complex Analysis","author":"W Rudin","year":"1987","unstructured":"Rudin, W.: Real and Complex Analysis, 3rd edn. McGraw-Hill Inc, USA (1987)","edition":"3"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Smith, C., Hsu, J., Albarghouthi, A.: Trace abstraction modulo probability. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290352","DOI":"10.1145\/3290352"},{"key":"2_CR29","unstructured":"Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Automated tail bound analysis for probabilistic recurrence relations. CoRR (2023). http:\/\/arxiv.org\/abs\/2305.15104"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Harper, R.: Verified tail bounds for randomized programs. In: ITP, pp. 560\u2013578 (2018)","DOI":"10.1007\/978-3-319-94821-8_33"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: Central moment analysis for cost accumulators in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20\u201325, 2021, pp. 559\u2013573. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454062","DOI":"10.1145\/3453483.3454062"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: Freund, S.N., Yahav, E. (eds.) PLDI, pp. 1171\u20131186. ACM (2021)","DOI":"10.1145\/3410310"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Wilkie, A.J.: Schanuel\u2019s conjecture and the decidability of the real exponential field. In: Hart, B.T., Lachlan, A.H., Valeriote, M.A. (eds.) Algebraic Model Theory. NATO ASI Series, vol. 496 pp. 223\u2013230. Springer, Dordrecht (1997). https:\/\/doi.org\/10.1007\/978-94-015-8923-9_11","DOI":"10.1007\/978-94-015-8923-9_11"},{"key":"2_CR34","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"D Williams","year":"1991","unstructured":"Williams, D.: Probability with Martingales. Cambridge University Press, Cambridge (1991)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37709-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:35Z","timestamp":1689501695000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37709-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377082","9783031377099"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37709-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}