15:45-16:45 | A key question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is, that it terminates "almost surely". Proving that is a notoriously hard problem, it is Pi2-hard, to be precise. Whereas for ordinary programs a ranking (or variant) function suffices to prove certain termination, this is no longer the case for probabilistic programs. In this talk, I'll present a new proof rule that allows for proving almost-sure termination for a rich set of programs and give some simple, though counter-intuitive examples of almost-surely terminating programs. |