Modular Runtime Complexity Analysis of Probabilistic While Programs
Abstract
In this work we are concerned with the average case runtime complexity analysis of a prototypical imperative language in the spirit of Dijkstra’s Guarded Command Language. This language is endowed with primitives for sampling and probabilistic choice so that randomized algorithms can be expressed. Complexity analysis in this setting is particularly appealing as efficiency is one striking reason why randomized algorithms have been introduced and studied: in many cases, the most efficient algorithm for the problem at hand is randomized.
Our staring point in this work is the ert-calculus of Kaminski et al., which constitutes a sound and complete method for deriving expected runtimes of probabilistic programs. We combine this machinery with an avarage size analysis, so to make the overall procedure modular, in the sense that different program fragments can be analysed independently.
Categories
Complexity Analysis, Imperative Programming, Automation, Probabilistic