We describe the design of a quantifier elimination framework for the complex numbers in the language of ordered rings supplemented with symbols for the imaginary unit, real parts, imaginary parts, and conjugates. Technically, we use a reduction to real quantifier elimination followed by a heuristic reinterpretation of the results within our complex framework. We present computational examples using a prototypical implementation of our approach in our Python-based open-source system Logic1.

Model reduction of fast-slow chemical reaction networks based on the quasi-steady state approximation fails when the fast subsystem has first integrals. We call these first integrals approximate conservation laws. In order to define fast subsystems and identify approximate conservation laws, we use ideas from tropical geometry. We prove that any approximate conservation law evolves more slowly than all the species involved in it and therefore represents a supplementary slow variable in an extended system. By elimination of some variables of the extended system, we obtain networks without approximate conservation laws, which can be reduced by standard singular perturbation methods. The field of applications of approximate conservation laws covers the quasi-equilibrium approximation, which is well known in biochemistry. We discuss reductions of slow-fast as well as multiple timescale systems. Networks with multiple timescales have hierarchical relaxation. At a given timescale, our multiple timescale reduction method defines three subsystems composed of (i) slaved fast variables satisfying algebraic equations, (ii) slow driving variables satisfying reduced ordinary differential equations, and (iii) quenched much slower variables that are constant. The algebraic equations satisfied by fast variables define chains of nested normally hyperbolic invariant manifolds. In such chains, faster manifolds are of higher dimension and contain the slower manifolds. Our reduction methods are introduced algorithmically for networks with monomial reaction rates and linear, monomial, or polynomial approximate conservation laws. We propose symbolic algorithms to reshape and rescale the networks such that geometric singular perturbation theory can be applied to them, test the applicability of the theory, and finally reduce the networks. As a proof of concept, we apply this method to a model of the TGF-beta signaling pathway.

For polynomial ODE models, we introduce and discuss the concepts of exact and approximate conservation laws, which are the first integrals of the full and truncated sets of ODEs. For fast-slow systems, truncated ODEs describe the fast dynamics. We define compatibility classes as subsets of the state space, obtained by equating the conservation laws to constants. A set of conservation laws is complete when the corresponding compatibility classes contain a finite number of steady states. Complete sets of conservation laws can be used for model order reduction and for studying the multistationarity of the model. We provide algorithmic methods for computing linear, monomial, and polynomial conservation laws of polynomial ODE models and for testing their completeness. The resulting conservation laws and their completeness are either independent or dependent on the parameters. In the latter case, we provide parametric case distinctions. In particular, we propose a new method to compute polynomial conservation laws by comprehensive Gro"\bner systems and syzygies.

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers. L’archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d’enseignement et de recherche français ou étrangers, des laboratoires publics ou privés. F5: A REDUCE Package for Signature-based Gröbner Basis Computation Alexander Demin, Hamid Rahkooy, Thomas Sturm

Recently, symbolic computation and computer algebra systems have been successfully applied in systems biology, especially in chemical reaction network theory. One advantage of symbolic computation is its potential for qualitative answers to biological questions. Qualitative methods analyze dynamical input systems as formal objects, in contrast to investigating only part of the state space, as is the case with numerical simulation. However, symbolic computation tools and libraries have a different set of requirements for their input data than their numerical counterparts. A common format used in mathematical modeling of biological processes is SBML. We illustrate that the use of SBML data in symbolic computation requires significant pre-processing, incorporating external biological and mathematical expertise. ODEbase provides high quality symbolic computation input data derived from established existing biomodels, covering in particular the BioModels database.

We discuss the effective computation of geometric singularities of implicit ordinary differential equations over the real numbers using methods from logic. Via the Vessiot theory of differential equations, geometric singularities can be characterised as points where the behaviour of a certain linear system of equations changes. These points can be discovered using a specifically adapted parametric generalisation of Gaussian elimination combined with heuristic simplification techniques and real quantifier elimination methods. We demonstrate the relevance and applicability of our approach with computational experiments using a prototypical implementation inReduce.

We present a symbolic algorithmic approach that allows to compute invariant manifolds and corresponding reduced systems for differential equations modeling biological networks which comprise chemical reaction networks for cellular biochemistry, and compartmental models for pharmacology, epidemiology and ecology. Multiple time scales of a given network are obtained by scaling, based on tropical geometry. Our reduction is mathematically justified within a singular perturbation setting. The existence of invariant manifolds is subject to hyperbolicity conditions, for which we propose an algorithmic test based on Hurwitz criteria. We finally obtain a sequence of nested invariant manifolds and respective reduced systems on those manifolds. Our theoretical results are generally accompanied by rigorous algorithmic descriptions suitable for direct implementation based on existing off-the-shelf software systems, specifically symbolic computation libraries and Satisfiability Modulo Theories solvers. We present computational examples taken from the well-known BioModels database using our own prototypical implementations.

We consider the problem of binomiality of the steady state ideals of biochemical reaction networks. We are interested in finding polynomial conditions on the parameters such that the steady state ideal of a chemical reaction network is binomial under every specialisation of the parameters if the conditions on the parameters hold. We approach the binomiality problem using Comprehensive Gröbner systems. Considering rate constants as parameters, we compute comprehensive Gröbner systems for various reactions. In particular, we make automatic computations on n-site phosphorylations and biomodels from the Biomodels repository using the grobcov library of the computer algebra system Singular.

In 2020, the 22nd CASC conference was planned to be held in Linz, Austria, at Johannes Kepler University (JKU). Due to the Covid-19 pandemic it had to be held as an online conference, hosted by the team at JKU. Although we were saddened not to be able to meet in Linz this year, we were grateful to the commitment of the organisers and participants that allowed CASC to go ahead successfully. This special issue contains selected work that was presented at this online event.

Motivated by problems arising with the symbolic analysis of steady state ideals in Chemical Reaction Network Theory, we consider the problem of testing whether the points in a complex or real variety with non-zero coordinates form a coset of a multiplicative group. That property corresponds to Shifted Toricity, a recent generalization of toricity of the corresponding polynomial ideal. The key idea is to take a geometric view on varieties rather than an algebraic view on ideals. Recently, corresponding coset tests have been proposed for complex and for real varieties. The former combine numerous techniques from commutative algorithmic algebra with Gröbner bases as the central algorithmic tool. The latter are based on interpreted first-order logic in real closed fields with real quantifier elimination techniques on the algorithmic side. Here we take a new logic approach to both theories, complex and real, and beyond. Besides alternative algorithms, our approach provides a unified view on theories of fields and helps to understand the relevance and interconnection of the rich existing literature in the area, which has been focusing on complex numbers, while from a scientific point of view the (positive) real numbers are clearly the relevant domain in chemical reaction network theory. We apply prototypical implementations of our new approach to a set of 129 models from the BioModels repository.

Motivated by problems from Chemical Reaction Network Theory, we investigate whether steady state ideals of reversible reaction networks are generated by binomials. We take an algebraic approach considering, besides concentrations of species, also rate constants as indeterminates. This leads us to the concept of unconditional binomiality, meaning binomiality for all values of the rate constants. This concept is different from conditional binomiality that applies when rate constant values or relations among rate constants are given. We start by representing the generators of a steady state ideal as sums of binomials, which yields a corresponding coefficient matrix. On these grounds, we propose an efficient algorithm for detecting unconditional binomiality. That algorithm uses exclusively elementary column and row operations on the coefficient matrix. We prove asymptotic worst case upper bounds on the time complexity of our algorithm. Furthermore, we experimentally compare its performance with other existing methods.

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Dataset supporting the paper: Russell Bradford, James H. Davenport, Matthew England, Hassan Errami, Vladimir Gerdt, Dima Grigoriev, Charles Hoyt, Marek Košta, Ovidiu Radulescu, Thomas Sturm, and Andreas Weber. Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks. To appear in the Journal of Symbolic Computation. We provide all the accompanying material for the main computations, split up into sections as presented in the paper. For Sections 3 and 9 the computations are introduced by a plain text ReadMe. For Sections 4 and 6 they are introduced by a Maple (also available ad pdf printout).

We consider the problem of testing whether the points in a complex or real variety with non-zero coordinates form a multiplicative group or, more generally, a coset of a multiplicative group. For the coset case, we study the notion of shifted toric varieties which generalizes the notion of toric varieties. This requires a geometric view on the varieties rather than an algebraic view on the ideals. We present algorithms and computations on 129 models from the BioModels repository testing for group and coset structures over both the complex numbers and the real numbers. Our methods over the complex numbers are based on Gröbner basis techniques and binomiality tests. Over the real numbers we use first-order characterizations and employ real quantifier elimination. In combination with suitable prime decompositions and restrictions to subspaces it turns out that almost all models show coset structure. Beyond our practical computations, we give upper bounds on the asymptotic worst-case complexity of the corresponding problems by proposing single exponential algorithms that test complex or real varieties for toricity or shifted toricity. In the positive case, these algorithms produce generating binomials. In addition, we propose an asymptotically fast algorithm for testing membership in a binomial variety over the algebraic closure of the rational numbers.

We consider feasibility of linear integer problems in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer problems is decidable, many state-of-the-art implementations neglect termination in favor of efficiency. We present the calculus CutSat++ that is sound, terminating, complete, and leaves enough space for model assumptions and simplification rules in order to be efficient in practice. CutSat++ combines model-driven reasoning and quantifier elimination to the feasibility of linear integer problems.

The international interdisciplinary SYMBIONT project ranges from mathematics via computer science to systems biology, with a balanced team of researchers from those fields. At the present stage the project has a clear focus on fundamental research on mathematical methods, and prototypes in software. Results are systematically benchmarked against models from computational biology databases. We summarize the motivation and aims for the project, and report on existing results by the consortium and first activities. The project website can be found at www.symbiont-project.org.

We report on a prototypical tool for Satisfiability Modulo Theory solving for quantifier-free formulas in Non-linear Real Arithmetic or, more precisely, real closed fields, which uses a computer algebra system as the main component. This is complemented with two heuristic techniques, also stemming from computer algebra, viz. interval constraint propagation and subtropical satisfiability. Our key idea is to make optimal use of existing knowledge and work in the symbolic computation community, reusing available methods and implementations to the most possible extent. Experimental results show that our approach is surprisingly efficient in practice.