This dissertation proposes a hybrid automata framework for modeling two intercellular protein signaling pathways active during development: the lateral inhibitory Delta-Notch pathway responsible for pattern formation in the skin of Xenopus laevis, and the Planar Cell Polarity (PCP) signaling pathway in Drosophila melanogaster wings. A fundamental objective of this work is to analytically compute constraints on the kinetic parameters of the model, for biologically interesting steady states to exist. The constraints are computed symbolically, without numerically instantiating the parameters, which is an advantage in modeling biological processes, where exact numerical parameters cannot often be identified from experimental data. Another key objective is the computation of initial protein concentrations that lead to a particular steady state. This is posed as a backward reachable set computation problem. An abstraction procedure is presented that converts the hybrid automaton into a discrete transition system, on which reachability is computed. The large size of the computed reachable sets make it difficult to directly interpret them in a biologically meaningful way. A query algorithm is developed that can test whether a particular protein distribution is guaranteed to converge to a specific steady state. Both the reachability and the query algorithm are demonstrated for the Delta-Notch hybrid model. The dissertation concludes with a description of the implementation of the analysis tools on a publicly available systems biology software platform known as Bio-SPICE; and a further example, lactose metabolism inside a cell, is analyzed.
展开▼
