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

 14:00 - 16:00: TACAS 2019 - Hybrid and Stochastic Systems at SUN I Chair(s): Kim LarsenAalborg University 14:00 - 14:30Talk Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher MomentsSatoshi Kura, Natsuki Urabe, Ichiro HasuoNational Institute of Informatics Link to publication 14:30 - 15:00Talk Computing the Expected Execution Time of Probabilistic Workflow Nets Link to publication 15:00 - 15:30Talk Shepherding Hordes of Markov ChainsMilan CeskaBrno University of Technology , Nils JansenRWTH Aachen University, Sebastian JungesRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University Link to publication 15:30 - 16:00Talk Optimal Time-Bounded Reachability Analysis for Concurrent Systems Link to publication