Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments

摘要

Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes. Unlike most of the existing works that focus on proving almost-sure termination or estimating the expected runtime, in this work we study the tail probabilities of runtimes—such as 'the execution takes more than 100 steps with probability at most 1%.'To this goal, we devise a theory of super- martingales that overapproximate higher moments of runtime. These higher moments, combined with a suitable concentration inequality, yield useful upper bounds of tail probabilities. Moreover, our vector-valued formulation enables automated template-based synthesis of those super-martingales. Our experiments suggest the method's practical use.