一句话：本文用线性 ranking supermartingale 合成，对仿射概率程序的终止性定性与定量问题给出算法及复杂度界。
本文研究带实值变量的概率程序终止问题，包括定性问题（几乎必然终止、期望终止时间有限）和定量问题（近似期望终止时间、计算尾部指数衰减的步数界）。方法上，作者基于 ranking supermartingale，重点研究仿射概率程序（App）中线性 ranking supermartingale 的算法合成，并处理天使与恶魔非确定性。主要结果：对至多含恶魔非确定性的 App，子类 LRA_pp 的成员判定可在多项式时间完成；含天使非确定性时则是 NP-hard 且属于 PSPACE，且 NP-hard 在无概率与恶魔非确定性时已成立。集中问题与成员问题复杂度相同；期望问题可在 2EXPTIME 求解，并对确定性程序已是 PSPACE-hard。实验表明方法对至多含恶魔非确定性的 App 有效。
In this article, we consider the termination problem of probabilistic programs with real-valued variables. The questions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); and quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability not to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales, which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (A pps ) with both angelic and demonic non-determinism. An important subclass of A pps is LRA pp which is defined as the class of all A pps over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRA pp (i) can be decided in polynomial time for A pps with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for A pps with angelic non-determinism. Moreover, the NP-hardness result holds already for A pps without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRA pp can be solved in the same complexity as for the membership problem of LRA pp . Finally, we show that the expectation problem over LRA pp can be solved in 2EXPTIME and is PSPACE-hard even for A pps without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over A pps with at most demonic non-determinism.
DOI 原文 ·
@article{paperbot321,
title = {Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs},
author = {Krishnendu Chatterjee and Hongfei Fu and Petr Novotný and Rouzbeh Hasheminezhad},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {2},
year = {2018},
doi = {10.1145/3174800}
}