Algorithmic reduction of biological networks with multiple time scales (Q2051597)

The article presents an algorithmic approach to the reduction of biological reaction networks. Reduction of reaction networks has been widely studied in the literature, however, the main distinction of this article is the algorithmic viewpoint using SMT solving combined with different methods ranging from singular perturbation to Gröbner bases. The article starts with the usual scaling of polynomial vector fields (describing reaction networks) in two time scales and give an algorithm to compute such a scaling. Then it follows with another main algorithm that uses tropical equilibration condition in order to give a tropicalisation of the scaled system as a union of polyhedra. A SMT solver is used during the tropicalisation algorithm. The next section of the article generalises the scaling in two time scales, presented in the previous section, into several time scales, following Cardin and Teixeira's work on multiple time scaling. Such a time scaling leads to a chain of nested subvarieties of the positive orthant, which is the set of solutions of a nested reduced system. A condition called hyperbolically attractiveness has been introduced on the latter chain such that if that condition holds, the chain convergies to the solutions of the system. Generalising Hurwitz' criterion, effective logic-based methods for characterising and verifying hyperbolically attractive chains has been given. Consequently, an algorithm for verifying hyperbolically attractiveness, which employs SMT solving, has been presented. The article then follows an algebraic method to further simplify the reduced system obtained via multiple time scaling in the previous section. Gröbner bases as the standard tool has been used at the core of the simplification algorithm. A back-transformation method is then described, which transformes the reduced system into the so-called back-transformed reduced system, with reverted scaling, but preserving same truncation and partitioning. All the above algorithms have been combined into a final algorithm, whose input is the ODE associated to a reaction network, and whose output is scaling into several times scales, in the form of the back-transformed reduced system. The algorithm runs tropicalisation, scaling, reduction, simplification and back-transforming consequently. The authors have developed two prototype softwares, one in Python and another one in Maple, implementing all the above algorithms. Extensive experiments have been done and many examples have been illustrated on biological systems from the biomodels repository, a repository of real world biological models. Remarks on the complexity of the methods, that show the effectiveness of the algorithms presented, have been described at the end of the paper.