A Calculus for Amortized Expected Runtimes

Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We develop a weakest-precondition-style calculus \`a la Dijkstra for reasoning about amortized expected runtimes of randomized algorithms with access to dynamic memory - the $\textsf{aert}$ calculus. Our calculus is truly quantitative, i.e. instead of Boolean valued predicates, it manipulates real-valued functions. En route to the $\textsf{aert}$ calculus, we study the $\textsf{ert}$ calculus for reasoning about expected runtimes of Kaminski et al. [2018] extended by capabilities for handling dynamic memory, thus enabling compositional and local reasoning about randomized data structures. This extension employs runtime separation logic, which has been foreshadowed by Matheja [2020] and then implemented in Isabelle/HOL by Haslbeck [2021]. In addition to Haslbeck's results, we further prove soundness of the so-extended $\textsf{ert}$ calculus with respect to an operational Markov decision process model featuring countably-branching nondeterminism, provide intuitive explanations, and provide proof rules enabling separation logic-style verification for upper bounds on expected runtimes. Finally, we build the so-called potential method for amortized analysis into the $\textsf{ert}$ calculus, thus obtaining the $\textsf{aert}$ calculus. Since one needs to be able to handle changes in potential which can be negative, the $\textsf{aert}$ calculus needs to be capable of handling signed random variables. A particularly pleasing feature of our solution is that, unlike e.g. Kozen [1985], we obtain a loop rule for our signed random variables, and furthermore, unlike e.g. Kaminski and Katoen [2017], the $\textsf{aert}$ calculus makes do without the need for involved technical machinery keeping track of the integrability of the random variables. Finally, we present case studies, including a formal analysis of a randomized delete-insert-find-any set data structure [Brodal et al. 1996].
Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
Number of pages30
PublisherAssociation for Computing Machinery
Publication date2023
Article number67
DOIs
Publication statusPublished - 2023
Event50th ACM SIGPLAN Symposium on Principles of Programming Languages - Boston Park Plaza, Boston, United States
Duration: 15 Jan 202321 Jan 2023
Conference number: 50

Conference

Conference50th ACM SIGPLAN Symposium on Principles of Programming Languages
Number50
LocationBoston Park Plaza
Country/TerritoryUnited States
CityBoston
Period15/01/202321/01/2023

Fingerprint

Dive into the research topics of 'A Calculus for Amortized Expected Runtimes'. Together they form a unique fingerprint.

Cite this