Algorithmic Algebraic Model Checking: Hybrid Automata & Systems Biology

Candidate: Venkatesh Pranesh Mysore

Advisor: Bhubaneswar Mishra

Systems Biology strives to hasten our understanding of
the fundamental principles of life by adopting a systems-level
approach for the analysis of cellular function and
behavior. One popular framework for capturing the
chemical kinetics of interacting biochemicals is Hybrid Automata.
Our goal in this thesis is to aid Systems Biology research by
improving the current understanding of hybrid automata, by developing
techniques for symbolic rather than numerical analysis of the
dynamics of biochemical networks modeled as hybrid automata, and by
honing the theory to two classes of problems: kinetic mass action based
simulation in genetic regulatory & signal transduction pathways, and
pseudo-equilibrium simulation in metabolic networks.

We first provide new constructions that prove that the
"open" Hierarchical Piecewise Constant Derivative (HPCD) subclass is
closer to the decidability and undecidability frontiers than
was previously understood. After concluding that the HPCD-like classes
are 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 Timed Computation Tree 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 Blum-Shub-Smale Turing Machine
formalism. We then develop efficient approximation strategies
by extending bisimulation partitioning, rectangular
grid-based approximation, polytopal approximation and time
discretization. We then develop a uniform
algebraic framework for modeling biochemical and metabolic
networks, also extending flux balance analysis. 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 "Algorithmic Algebraic Model Checking" techniques developed
in this thesis present a theoretically-grounded mathematically-sound
platform for powerful symbolic temporal reasoning over biochemical networks and
other semi-algebraic hybrid automata. It is our hope that by building upon
this thesis, along with the development of computationally efficient
parallelizable 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 analyzed.