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

tacas-2019-papers
14:00 - 16:00: TACAS 2019 - Hybrid and Stochastic Systems at SUN I
Chair(s): Kim LarsenAalborg University
tacas-2019-papers14:00 - 14:30
Talk
Satoshi Kura, Natsuki Urabe, Ichiro HasuoNational Institute of Informatics
Link to publication
tacas-2019-papers14:30 - 15:00
Talk
Link to publication
tacas-2019-papers15:00 - 15:30
Talk
Milan CeskaBrno University of Technology , Nils JansenRWTH Aachen University, Sebastian JungesRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University
Link to publication
tacas-2019-papers15:30 - 16:00
Talk
Link to publication