We present a novel approach to investigating key behavioral properties of complex biological systems by first using automated techniques to learn a simplified Linear Hybrid Automaton model of the system under investigation, and then carrying out automatic reachability analysis on the resulting model. The specific biological system we consider is the neuronal Action Potential and the specific question of interest is bifurcation: the graded response of the neuron to stimulation of varying amplitude and duration. Reachability analysis in this case is performed using the d/dt analysis tool for hybrid systems. The results we so obtain reveal the precise conditions under which bifurcation manifests, when taking into consideration an infinite class of input stimuli of arbitrary shape, amplitude, and duration within given respective intervals. To the best of our knowledge, this represents the first time that formal (reachability) analysis has been applied to a computational model of excitable cells. The obvious advantage of symbolic reachability analysis over simulation-perhaps the only available analysis method when complex systems of coupled ODEs are used to model excitable-cell behavior, as has traditionally been the case-is that through the so-called reachable set computation, the system's reaction to an infinite set of possible inputs can be observed. Our results further demonstrate that Linear Hybrid Automata, as a formal language, is both expressive enough to capture interesting excitable-cell behavior, and abstract enough to render formal analysis possible.
In Proc. of ICBBE'08, the 2nd International Conference on Bioinformatics and Biomedical Engineering, Shanghai, China, May, 2008, IEEE.
*This work was supported by the NSF Faculty Early Career
Development Award CCR01-33583 and the NSF CCF05-23863 Award.