Algorithm for verification of probabilistic reachability in hybrid systems, with application to biological models

Hybrid systems combine continuous and discrete evolution. They provide a powerful theoretical framework for modelling and formal verification of real-world systems (e.g., biological systems and cyber-physical systems). We investigate the problem of bounded reachability in hybrid systems with random initial parameters, i.e., computing the probability that the model reaches an unsafe region of its state space within a finite number of steps. In particular, we present an algorithm which given a model of a system with random initial parameters (bounded or unbounded) can compute an interval of an arbitrarily small length containing the exact value of such probability. We have applied the implemented algorithm to the verification of biological models such as the Insulin-Glucose Regulatory System and Starvation Model