Proving Almost-Sure Termination by Omega-Regular Decomposition
Almost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. Our approach automatically decomposes the runs of the probabilistic program into a finite union of ω-regular subsets and then proves almost-sure termination of each subset based on the notion of localized ranking supermartingales. Compared to the lexicographic methods and the compositional methods, our approach does not require a lexicographic order over the ranking supermartingales as well as the so-called unaffecting condition. Thus it has high generality. We present the algorithm of our approach and prove its soundness, as well as its relative completeness. We show that our approach can be applied to some hard cases and the evaluation on the benchmarks of previous works shows the significant efficiency of our approach.
Fri 19 JunDisplayed time zone: Pacific Time (US & Canada) change
05:00 - 06:00 | Probabilistic ProgrammingPLDI Research Papers at PLDI Research Papers live stream Chair(s): Sasa Misailovic University of Illinois at Urbana-Champaign | ||
05:00 20mTalk | Proving Almost-Sure Termination by Omega-Regular Decomposition PLDI Research Papers | ||
05:20 20mTalk | λPSI: Exact Inference for Higher-Order Probabilistic Programs PLDI Research Papers Timon Gehr ETH Zurich, Switzerland, Samuel Steffen ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland | ||
05:40 20mTalk | Reactive Probabilistic Programming PLDI Research Papers Guillaume Baudart IBM Research, Louis Mandel IBM Research, Eric Atkinson Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Marc Pouzet École normale supérieure, Michael Carbin Massachusetts Institute of Technology, USA DOI Pre-print Media Attached |