Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-Notch protein signalling

Hybrid automata are an eminently suitable modelling framework for biological protein regulatory networks, as the protein concentration dynamics inside each biological cell are modelled using linear differential equations; inputs activate or deactivate these continuous dynamics through discrete switches, which themselves are controlled by protein concentrations reaching given thresholds. This paper proposes an iterative refinement algorithm for computing discrete abstractions of a class of hybrid automata with piecewise affine continuous dynamics and forced discrete transitions, defined completely in terms of symbolic variables and parameters. Furthermore, these discrete abstractions are utilised to compute symbolic parametric backward reachable sets from the equilibria of the hybrid automata, that are guaranteed to be exact or conservative under-approximations. The algorithm is then implemented using MATLAB and QEPCAD, to compute reachable sets for the biologically observed equilibria of the multiple cell Delta-Notch protein signalling automaton with symbolic parameters. The results are analysed to show that novel, non-intuitive, and biologically interesting properties can be deduced from the reachability computation, thus demonstrating the utility of the algorithm.