Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments
Programs with probabilistic branching and random assignments attract a lot of attention as a programming-language foundation of randomized algorithms. A number of analysis methods have been proposed for such programs, notable among which is a family of martingale-based methods for termination analysis. Most of these methods study either the qualitative question of almost-sure reachability, approximating reachability probabilities, or approximating the expected runtimes. In this paper we extend the realm of martingale-based methods to \emph{tail probabilities}, that is, the probability with which a program does not terminate within a given deadline. For programs with probabilistic branching, nondeterministic branching, and assignments from (potentially continuous) distributions, we devise a martingale-based method for overapproximating tail probabilities—which allows one e.g.\ to say ``the program’s execution takes more than 100 steps with probability at most 1%.'' Our method features the following: 1) an extension of martingales to higher moments (we do so systematically so that it enables template-based automatic synthesis); and 2) use of a suitable concentration inequality which we prove to be optimal. We implement the proposed method using linear and polynomial templates, and LP- and SDP-solvers, respectively. Our experiments suggest the method’s scalability as well as the quality of the obtained upper bounds.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments TACAS Link to publication | ||
14:30 30mTalk | Computing the Expected Execution Time of Probabilistic Workflow Nets TACAS Link to publication | ||
15:00 30mTalk | Shepherding Hordes of Markov Chains TACAS Milan Ceska Brno University of Technology , Nils Jansen RWTH Aachen University, Sebastian Junges RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University Link to publication | ||
15:30 30mTalk | Optimal Time-Bounded Reachability Analysis for Concurrent Systems TACAS Link to publication |