Write a Blog >>

We consider termination of probabilistic programs with real-valued variables. The relevant probabilistic termination questions are as follows: (1) qualitative questions that ask whether (a) the program terminates with probability 1 (almost-sure termination), (b) the expected termination time is finite (finite termination); (2) quantitative questions that ask to (a) approximate the expected termination time (expectation problem),
(b) approximate the probability to terminate in a given number of steps (probabilistic problem), (c) compute a bound $B$ such that the probability to terminate after $B$ steps decreases exponentially (concentration problem). The notion of ranking supermartingales is a powerful approach to establish termination for probablistic programs. In this work we consider algorithmic questions related probabilistic termination, and since our focus is algorithms we consider the simplest class of ranking supermartingales, namely linear ranking supermartingales. We consider the class of affine probabilistic programs (APPs) for which linear ranking supermartingales exist and refer the subclass as LRAPPs.

Our main results for LRAPPs are as follows: First, we show that the qualitative problems (i) can be answered for probabilistic programs with demonic nondeterminism in polynomial time, (ii) are NP-hard for programs with angelic nondeterminism, and (iii) can be solved in PSPACE for probabilistic programs with both angelic and demonic nondeterminism. Second, we show that the concentration problem can be solved in the same complexity as for the qualitative problems. Finally, we establish complexity results for the expectation and probabilistic problems. For both the problems we show PSPACE-hardness even for deterministic programs, and that the problems for probabilistic programs with both types of nondeterminism can be solved in 2EXPTIME. We present experimental results to show the effectiveness of our approach to answer the qualitative and quantitative questions on probabilistic programs with demonic nondeterminism.

Thu 21 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 2: Probabilistic and statistical analysisResearch Papers at Grand Bay South
Chair(s): Aditya Nori Microsoft Research, UK
10:30
25m
Talk
Prophet: Automatic Patch Generation via Learning from Successful Patches
Research Papers
Fan Long MIT CSAIL, Martin C. Rinard Massachusetts Institute of Technology, USA
Media Attached
10:55
25m
Talk
Estimating types in binaries using predictive modeling
Research Papers
Omer Katz Technion, Israel Institute of Technology, Ran El-Yaniv Technion, Israel Institute of Technology, Eran Yahav Technion
Media Attached File Attached
11:20
25m
Talk
Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs
Research Papers
Krishnendu Chatterjee IST Austria, Hongfei Fu IST Austria, Rouzbeh Hasheminezhad Sharif University, Petr Novotný IST Austria
Media Attached
11:45
25m
Talk
Transforming Spreadsheet Data Types using Examples
Research Papers
Rishabh Singh Microsoft Research, Sumit Gulwani Microsoft Research
Media Attached