Algorithmic Reduction of Biochemical Reaction Networks

The dynamics of species concentrations of chemical reaction networks are given by autonomous first-order ordinary differential equations. Singular perturbation methods allow the computation of approximate reduced systems that make explicit several time scales with corresponding invariant manifolds. This thesis presents:

1. An algorithmic approach for the computation of such reductions on solid analytical grounds. Required scalings are derived using tropical geometry. The existence of invariant manifolds is subject to certain hyperbolicity conditions. These conditions are reduced to Hurwitz criteria and discrete combinatorial conditions on degrees, which are technically solved using SMT over nonlinear real and linear integer arithmetic, respectively. The approach is implemented in Python and applied to a large body of known biochemical models.
2. ODEbase, a repository of biochemical models that has been created to provide real-world input data in a form that is suitable for symbolic computation software. ODEbase has been populated with semi-automatic conversions of several hundred SBML models from the BioModels database and is available to everyone at https://odebase.org.
3. A calculus for model-driven computation of disjunctive normal forms of real constraints from conjunctions of such disjunctive normal forms, which is required for the tropicalization in 1. The calculus technically once more builds on SMT solving, here over linear real arithmetic. Compared to existing software like Redlog, its implementation generally shows significant speedups, and a number of otherwise infeasible computations finish within seconds.