Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

CHATTERJEE, Krishnendu, Hongfei FU, Petr NOVOTNÝ a Rouzbeh HASHEMINEZHAD. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS (TOPLAS). NEW YORK: ACM, 2018, roč. 40, č. 2, 45 s. ISSN 0164-0925. Dostupné z: https://dx.doi.org/10.1145/3174800.

Základní údaje

Originální název

Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs

Autoři

CHATTERJEE, Krishnendu, Hongfei FU, Petr NOVOTNÝ a Rouzbeh HASHEMINEZHAD

Vydání

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS (TOPLAS), NEW YORK, ACM, 2018, 0164-0925

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.800

DOI

http://dx.doi.org/10.1145/3174800

UT WoS

000434634500003

Klíčová slova anglicky

Probabilistic programs; termination; ranking supermartingale; concentration

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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 (Apps) with both angelic and demonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Apps over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) can be decided in polynomial time for Apps with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for Apps with angelic non-determinism. Moreover, the NP-hardness result holds already for Apps without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show that the expectation problem over LRApp can be solved in 2EXPTIME and is PSPACE-hard even for Apps 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 Apps with at most demonic non-determinism.