一句话：提出 aert 演算，以最弱前置条件风格定量推理随机算法在动态内存下的摊还期望运行时间。
论文研究带动态内存的随机算法，如何以最弱前置条件风格定量推理其摊还期望运行时间，提出 aert 演算。方法上，先把 Kaminski 等人的 ert 演算扩展到动态内存，借助运行时分离逻辑实现对随机数据结构的组合式局部推理，并证明该扩展相对于带可数分支非确定性的 MDP 操作模型可靠；随后将势能法以概率望远镜求和形式融入 ert，得到 aert 演算。该演算能处理有符号随机变量，给出循环规则，并避免显式跟踪可积性。案例研究包括 Brodal 等人的随机 delete-insert-find-any 集合，证明每次操作具有常数期望运行时间，而确定性算法无法做到。
We develop a weakest-precondition-style calculus à la Dijkstra for reasoning about amortized expected runtimes of randomized algorithms with access to dynamic memory — the aert calculus. Our calculus is truly quantitative, i.e. instead of Boolean valued predicates, it manipulates real-valued functions. En route to the aert calculus, we study the 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 ert calculus with respect to an operational Markov decision process model featuring countably-branching nondeterminism, provide extensive 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 ert calculus, thus obtaining the aert calculus. Soundness of the aert calculus is obtained from the soundness of the ert calculus and some probabilistic form of telescoping. Since one needs to be able to handle changes in potential which can in principle be both positive or negative, the aert calculus needs to be — essentially — capable of handling certain 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 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], which yields a constant expected runtime per operation, whereas no deterministic algorithm can achieve this.
@article{paperbot2112,
title = {A Calculus for Amortized Expected Runtimes},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Lena Verscht},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571260}
}