EVENT

Project colloquium talk by Ichiro Hasuo : "Approximating Reachability Probabilities by (Super-)Martingales"

Date:

April 25 (Wed.)

Time:

16:00 - 17:00

Place:

ERATO MMSD Takebashi Site Common Room 3
http://group-mmm.org/eratommsd/access.html

Speaker:

Ichiro Hasuo (National Institute of Informatic)

Title:

Approximating Reachability Probabilities by (Super-)Martingales

Abstract:

Reachability is a fundamental problem in the analysis of probabilistic systems. It is well-known that reachability probabilities are efficiently computed for finite-state systems by linear programming. However, this LP method does not apply to systems that have infinitely many configurations, such as probabilistic programs and parametric systems. In such a case, we have to rely on a parametric witness (i.e. a function) for over- or under-approximating reachability probabilities. A well-studied class of such witnesses is that of supermartingales. In this talk I will talk about our recent results that refine existing supermartingale-based methods. The technical keys to those results are: choice of a suitable martingale concentration lemma for over-approximation; and a categorical axiomatization of supermartingales by coalgebras and corecursive algebras. The talk is based on my joint work with Natsuki Urabe, Masaki Hara, Bart Jacobs, Toru Takisaka and Yuichiro Oyabu.