Hybrid Automata in Systems Biology: How Far Can We Go?

We consider the reachability problem on semi-algebraic hybrid automata. In particular, we deal with the effective cost that has to be afforded to solve reachability through first-order satisfiability.The analysis we perform with some existing tools shows that even simple examples cannot be efficiently solved. We need approximations to reduce the number of variables in our formulae: this is the main source of time computation growth. We study standard approximation methods based on Taylor polynomials and ad-hoc strategies to solve the problem and we show their effectiveness on the repressilator case study.