MODELING AND SYMBOLIC ANALYSIS OF BIOLOGICAL PROTEIN SIGNALING NETWORKS USING HYBRID AUTOMATA A DISSERTATION SUBMITTED TO THE DEPARTMENT OF AERONAUTICS AND ASTRONAUTICS AND THE COMMITTEE ON GRADUATE STUDIES OF STANFORD UNIVERSITY IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY Ronojoy Ghosh December 2005 UMI Number: 3197434 Copyright 2006 by Ghosh, Ronojoy All rights reserved. INFORMATION TO USERS The quality of this reproduction is dependent upon the quality of the copy submitted. Broken or indistinct print, colored or poor quality illustrations and photographs, print bleed-through, substandard margins, and improper alignment can adversely affect reproduction. In the unlikely event that the author did not send a complete manuscript and there are missing pages, these will be noted.
Also, if unauthorized copyright material had to be removed, a note will indicate the deletion. ® UMI UMI Microform 3197434 Copyright 2006 by ProQuest Information and Learning Company. All rights reserved. This microform edition is protected against unauthorized copying under Title 17, United States Code.
ProQuest Information and Learning Company 300 North Zeeb Road P. Box 1346 Ann Arbor, MI 48106-1346 (©) Copyright by Ronojoy Ghosh 2006 All Rights Reserved ii I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. CL, (Claire Tomlin) Principal Adviser I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. / (Stephen Rock) ⁄ I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy.
Ele flip (David Dill) I certify that I have read this dissertation and that, in my opinion, it is fully adequate in scope and quality as a dissertation for the degree of Doctor of Philosophy. 2M,PU LX 4 retired Axelrod) ( Approved for the University Committee on Graduate Studies. ili Abstract Recent advances in quantitative biology have created a tremendous opportunity to apply dynamical systems modeling to biological phenomena, and to validate these models using experimental data. Using simulation and analysis, there is immense scope to discover non-intuitive design principles behind biological processes, and successfully predict the effects of changing key variables.
Systems biology, defined as the integration of mathematical analysis with experimental biology, has the potential to revolutionize the way biology is done. Cellular protein signaling networks exhibit complex combinations of both discrete and continuous behaviors. The dynamics that govern the spatial and temporal in- crease or decrease of protein concentrations inside cells are continuous differential equations, while the activation or deactivation of these continuous dynamics are trig- gered by discrete switches that involve regulating species concentrations reaching given thresholds. This thesis proposes a hybrid automata framework for modeling such processes; hybrid automata theory being a hierarchical mathematical system that uses differen- tial equations to model continuous dynamics, and discrete event-driven switches to model the governing equations in different modes of operation.
In particular, the the- sis proposes hybrid models of two interesting intercellular signaling pathways active during embryonic development: the lateral inhibitory Delta-Notch pathway respon- sible for pattern formation in the embryonic skin of Xenopus laevis, and the Planar Cell Polarity (PCP) signaling pathway in Drosophila melanogaster wings. These models are validated against experimentally observed steady state protein concen- tration patterns. iv A fundamental objective of this work is to analytically compute constraints on the kinetic parameters of the model, for particular biologically observed or interesting steady states to exist. The constraints are computed symbolically, i.
without having to numerically instantiate the parameters. This is a great advantage in the context of biological processes, where exact numerical parameters cannot often be identified from experimental data, but a range of values, or relative values for the parameters can be obtained. The particular structure of the hybrid automata models developed in this work make symbolic constraint generation computationally tractable. Another key objective is the computation of initial conditions, or initial protein concentrations, that converge to a particular steady state.
The initial conditions can be interpreted as initial biases in the distribution of signaling species that lead to a biologically interesting steady state. This is posed as a backward reachable set com- putation problem. An abstraction procedure is presented that converts the hybrid automaton into a discrete transition system using symbolic solutions to the differen- tial equations and Lie derivatives to compute transitions between discrete states. The backward reachability problem is then computed on the discrete abstraction, which makes the analysis tractable for large state spaces.
The reachability computation is implemented using MATLAB and the quantifier elimination tool QEPCAD and is demonstrated for multiple cell Delta-Notch signaling networks with up to eighteen continuous variables. Since the computed reachable sets are large, it is difficult to directly interpret them in a biologically meaningful way. To solve this problem, a query algorithm is developed and presented that can be used to test whether a particular protein distri- bution is guaranteed to converge to a steady state of interest. The use of the query algorithm is demonstrated for the Delta-Notch hybrid model.
The thesis concludes with a description of the implementation of the analysis tools on a publicly available systems biology software platform known as Bio-SPICE. A further example, lactose metabolism inside a cell, is described as an illustration of the methods developed in this work; and reachable sets are computed for this model using the tools integrated with Bio-SPICE. Acknowledgments I would like to thank my principal adviser, Professor Claire Tomlin, for her guidance and support during my graduate career at Stanford University. Her insight, teaching skills, mentorship, and unwavering enthusiasm made this work possible.
I would also like to thank Professor David Dill for introducing me to formal verification, which enabled me to approach control theoretic analysis from a different perspective, and for his insightful comments on my research. I gratefully acknowledge the research collaboration with Professor Jeffrey Axelrod, who gave me an opportunity to observe the wonderful world of experimental biology, and for his useful comments that helped refine this thesis. I would like to thank Professor Stephen Rock, for his valuable comments on my dissertation research and for encouraging me to write this thesis in a style accessible to both engineers and biologists. It is a pleasure to acknowledge my research collaborations with Dr.
Ashish Ti- wari and Dr. Patrick Lincoln, at SRI International. The experience I gained working with them on implementing symbolic abstraction and verification algorithms proved invaluable when I was attempting to design and implement my own analysis algo- rithms. I would like to thank Dr.
Adam Halasz and Professor Vijay Kumar at the University of Pennsylvania, for our research collaborations on the lactose metabolism model. My sincere thanks go to Professors Harley McAdams and Lucy Shapiro, for sustaining my research interest in systems biology during the crucial early years of my graduate career. The discussions we had on mathematical modeling of genetic networks provided valuable insight into the biologist’s view of the problem. I would also like to thank Professor Hasan Suhail, my undergraduate adviser at the Indian vi Institute of Technology, Kharagpur, for initiating my interest in computational biol- ogy.
In addition, I would like to thank Keith Amonlirdviman, Gokhan Inalhan, Alexan- dre Bayen, Jung Soon Jang, Inseok Hwang, Meeko Oishi, Rodney Teo, Ian Mitchell, Hamsa Balakrishnan, Robin Raffard, Gabe Hoffmann, Steven Waslander, Kaushik Roy, Peter Brende, Sriram Shankaran, Jianghai Hu, and Dusan Stipanovic for their collaborations, informal conversations, and for making the hybrid systems laboratory an exciting and stimulating place to work. I would like to gratefully acknowledge the financial support of DARPA, and thank Dr. Eric Eisenstadt and Dr. Sri Kumar for their encouragement and interest in my research.
I would also like to thank Stanford University for the School of Engineering Fellowship and the Interstate Electronics Corporation Fellowship. I would like to thank my friends, Daniel Levner in partic- ular, for their encouragement and for adding color to life outside of work. Lastly, I would especially like to thank my wife, Sheila, and my parents for their constant support and encouragement without which my graduate career would not have been possible. vii Contents Abstract iv Acknowledgments vi 1 Introduction 1.2 Glossary of Biological Terms.
eae 1l 2 Protein Signaling 13 2.2 Lateral Inhibition Through Delta-Notch Signaling .3 Planar Cell Polarity Signaling .4 Motivation for Hybrid Model. ee ee 18 3 Hybrid Automata 20 3.1 Hybrid Automata and Transition Systems. 20 4 Delta-Notch Signaling 4.1 Delta-Notch Lateral Inhibition.1 Previous Work: Mathematical Models .2 Hybrid Automaton with Piecewise Linear Switch .2 Equilibrium Analysis and Constraint Generation.3 Simulation Results for a Planar Array of£Cells.3 Hybrid Automaton with Signum Switch.2 Equilibrium Analysis and Constraint Generation. Simulation Results for 1 and 2 Dimensional Networks of Cells 4.4 Comparison with Nonlinear ODE Model .1 Reachability: Mathematical Definitions .4 Reachable Set Computation Results.1 One Cell Delta-Notch Automaton.2 Two Cell Delta-Notch Automaton.3 Four Cell Delta-Notch Automaton.5 Query-Based Interpretation .1 Structure of Computed Reachable Sets .2 Example: Four Cell Delta-Notch Automaton .3 Query Based Interpretation Algorithm .4 Query Results for Four Cell Delta-Notch Automaton .6 Proposed Biological Experiments.
0000 eae 87 Planar Cell Polarity Signaling 6. Q Q ng và và va 6.2 Hybrid Automaton Model Development.3 Equilibrium Analysis and Parameter Constraints.4 Simulation Results and Experimental Validation.1 Integration with Bio-SPICE Systems Biology Software Platform .2 Lactose Metabolism within a Bacterial Cel.21 Hybrid Model Development and Simplification.2 Reachability Analysis Results. 8 Future Work A Definition of Lactose Metabolism Hybrid Model Bibliography List of Tables 4.1 Equilibria of the single cell automaton Hone cell,PWA.2 Existence conditions for equilibrium points of Hạns se PWA- - - - - + - 33 4.3 Unsatisfiable constraint list for possible equilibrium-containing modes of Hiwo-cell, PW A- SS .4 Existence conditions for equilibrium points of Honecell.5 Existence conditions for equilibrium points of Hiwoccy (the composi- tion of two single-cell hybrid automata).1 Steady state protein concentrations in four cell Delta-Notch network.1 Equilibria of the single cell automaton Hpgp. Of the 256 equilibria, only the important ones are listed.2 Existence conditions for equilibria of Hpcp.1 Parameter values for lactose metabolism hybrid automaton.2 Equilibria of reduced order lactose metabolism hybrid automaton Aljgeg.115 xi List of Figures 2.1 Xenopus embryo labeled by a-tubulin, a marker for ciliated cell pre- cursors seen as black dOfS.2 Drosophila adult wing epithelium.
The figure of a magnified portion of the wing below shows the hexagonal shape of the cells and the hairs pointing in a similar direction.3 Planar cell polarity signaling network between two adjacent cells in Drosophila pupal wing. 1v nà và k va 17 2.4 Piecewise linear switching function.5 Sigmoidal switching function.1 Continuous state space with geometrical representations of polynomial modal invariants of a two dimensional hybrid automaton.1 (a) Hexagonal close-packed layout scheme for cells in two dimensional arrays. (b) Influence diagram for Delta-Notch protein signaling network.2 Transition diagram for a single cell hybrid automaton with piecewise linear switch, ©. ung và g v v và VN va 31 4.3 Hybrid automaton for a 3 x 3 array, modeling a nine cell network.4 Equilibrium mode map for single cell automaton with piecewise linear switching function.
kg kg kg kg kg k va 34 4.5 Effect on equilibria of two cell automaton Hs se¡ pwA With changes in switch slope m. Note the disappearance of the two equilibria at (1,0) and (0,1) when mm < au TH xặ:cừýáa .6 Steady state protein concentration distribution in a planar array of cells for hybrid model.7 Steady state protein concentration distribution in a planar array of cells for nonlinear model with sigmoid switch, .8 Steady state protein concentrations for hybrid model with shallow lin- ear switch.9 Steady state protein concentrations for nonlinear model with shallow sigmoid switch,. ng va g v kg va 42 4.10 Phase portrait for a single cell hybrid automaton.11 Pruned transition diagrams for Delta-Notch hybrid automata.