[Apologies for multiple copies]

Dear all,

Let me advertise our next ERATO MMSD project colloquium talk by Ichiro Hasuo on 25th April, 16:00-. Please find the title and the abstract below. You are all invited.

Sincerely, -- Natsuki Urabe urabenatsuki@is.s.u-tokyo.ac.jp The University of Tokyo, ERATO MMSD

----- Wed 25 April 2018, 16:00–17:00

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

Ichiro Hasuo (National Institute of Informatics http://www.nii.ac.jp/), 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.