ERATO MMSD Takebashi Site Common Room 3
http://group-mmm.org/
Ichiro Hasuo (National Institute of Informatics),
Approximating Reachability Probabilities by (Super-)Martingales
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.