3347b0f54d9a3986.tex
1: \begin{abstract}
2:   We consider the problem of bounding mean first passage times and reachability probabilities
3:   for the class of population continuous-time Markov chains,  which capture stochastic interactions between groups of identical agents.
4:   The  quantitative analysis of such models
5:   is notoriously difficult since typically neither   state-based numerical
6:   approaches nor methods based on stochastic sampling give efficient and accurate results.
7:   Here, we propose a novel 
8:   approach that leverages techniques from martingale theory and stochastic processes to generate constraints on the statistical moments of first passage time distributions. These constraints induce a semi-definite program that can be used to compute exact bounds on reachability probabilities and mean first passage times without numerically solving the transient probability distribution of the process or sampling from it.
9: We showcase the method on some test examples and tailor it to  models exhibiting multimodality, a class of particularly challenging scenarios from biology.
10: \keywords{population continuous-time Markov chains \and semi-definite programming
11:   \and exit time distribution \and reachability probability \and Markov population models}
12: \end{abstract}
13: