An algorithm for reachability computations on hybrid automata models of protein signaling networks

Hybrid automata theory is an ideal mathematical framework for modeling biological protein signaling mechanisms. Reachability analysis of these models is essential, because the set of points backward reachable from a biologically feasible equilibrium contains all initial protein concentrations from which that steady state can be attained. This is useful for determining experimentally verifiable properties of the system under study. This paper proposes an algorithm for computing discrete abstractions of a class of hybrid automata with piecewise affine continuous dynamics, defined completely in terms of symbolic variables and parameters. These discrete abstractions are utilized to compute symbolic parametric backward reachable sets from the equilibria of the hybrid automata. The algorithm has been implemented and used to compute reachable sets for the biologically observed equilibria of multiple cell Delta-Notch protein signaling networks.