ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 14:00 - 14:30 at SUN I - Hybrid and Stochastic Systems Chair(s): Kim Larsen

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 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change