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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 14:00 - 16:00 Hybrid and Stochastic SystemsTACAS at SUN I Chair(s): Kim Larsen Aalborg University 14:0030mTalk Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher MomentsTACASSatoshi Kura , Natsuki Urabe , Ichiro Hasuo National Institute of Informatics Link to publication 14:3030mTalk Computing the Expected Execution Time of Probabilistic Workflow NetsTACAS Link to publication 15:0030mTalk Shepherding Hordes of Markov ChainsTACASMilan 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:3030mTalk Optimal Time-Bounded Reachability Analysis for Concurrent SystemsTACAS Link to publication