论文标题
摊销的预期运行时间的演算
A Calculus for Amortized Expected Runtimes
论文作者
论文摘要
我们开发了一种最弱的前提式微积分dijkstra，用于推理具有访问动态内存的随机算法的预期运行时间 - $ \ textsf {aert} $ calculus。我们的演算是真正的定量，即，它可以操纵实现的函数，而不是布尔值的谓词。 在到达$ \ textsf {aert} $ calculus的途中，我们研究了$ \ textsf {ert} $ calculus，以推理Kaminski等人的预期运行时间。 [2018]通过功能扩展了处理动态内存的功能，从而实现了关于随机数据结构的组成和局部推理。该扩展名采用运行时分离逻辑，该逻辑已由Matheja [2020]预示，然后在Haslbeck [2021]中在Isabelle/Hol中实现。除了Haslbeck的结果外，我们进一步证明了So-Exted $ \ textsf {ert} $ Calculus在操作的马尔可夫决策过程模型上，具有无数分支的非确定性，提供直观的解释，提供证明规则，并提供具有逻辑性的逻辑性验证的逻辑性验证，以实现上限为预期的运行时间。最后，我们将所谓的潜在方法构建到$ \ textsf {ert} $ cyculus中，从而获得$ \ textsf {aert} $ calculus。 由于一个人需要能够处理电势的变化，这可能是负面的，因此$ \ textsf {aert} $微积分需要能够处理签名的随机变量。我们解决方案的一个特别令人愉悦的特征是，与例如Kozen [1985]，我们为我们的签名随机变量获得了一个循环规则，此外，与例如Kaminski和Katoen [2017]，$ \ textsf {aert} $微积分无需参与技术机械，跟踪随机变量的集成性。 最后，我们介绍了案例研究，包括对任何集合数据结构的随机删除 - 插入的正式分析[Brodal等。 1996]。
We develop a weakest-precondition-style calculus à 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].
