| Systems Biology strives to hasten our understanding of the fundamental principles of life by adopting a global systems-level approach for the analysis of cellular function and behavior. Hybrid Automata are an ideal framework for capturing the chemical kinetics of interacting biochemicals. Our goal in this thesis is to aid Systems Biology research by improving the current understanding of hybrid automata.; We first provide new constructions that prove that the "open" HPCD subclass is closer to decidability and undecidability than was previously thought. However, the low dimensionality constraint that must be met for this class to be decidable makes it unsuitable for modeling chemical reactions. Our quest for semi-decidable subclasses leads us to define the "semi-algebraic" subclass. This is the most expressive hybrid automaton subclass amenable to rigorous symbolic temporal reasoning. We begin with the bounded reachability problem, and then show how the dense-time temporal logic TCTL can be model-checked by exploiting techniques from real algebraic geometry, primarily real quantifier elimination. We also prove the undecidability of reachability in the real Turing Machine formalism. We then develop efficient approximation strategies for semi-algebraic hybrid systems by extending bisimulation partitioning, rectangular grid-based approximation, polytopal approximation and time discretization. We identify well-behaved subclasses and develop new optimizations. We then develop a uniform algebraic framework for modeling biochemical and metabolic networks. We extend the flux balance analysis based approach for equilibrium characterization. We present some preliminary results using a prototypical tool Tolque. It is a symbolic algebraic dense time model-checker for semi-algebraic hybrid automata, which uses Qepcad for quantifier elimination.; The techniques developed in this thesis present a mathematically well-grounded platform for powerful symbolic reasoning over biochemical networks and other semi-algebraic hybrid automata. It is hoped that the by building upon this thesis, along with the development of computationally efficient quantifier elimination algorithms and the integration of different computer algebra tools, scientific software systems will emerge that fundamentally transform the way biochemical networks (and other hybrid automata) are investigated and understood. |
