An Algorithm for the Formal Reduction of Differential Equations as Over-Approximations

Models of complex systems often consist of state variables with structurally similar dynamics that differ in the specific values of some parameters. Examples are multi-class epidemiological models, chemical reaction networks describing multiple components (e.g., binding sites) with equivalent functional behavior, and models of electric circuits with replicated designs. In these cases, the analysis may be expensive due to the model size. Here we consider models defined as systems of polynomial ordinary differential equations (ODEs) with positive solutions. We present an algorithm to reduce the computational cost by transforming the original ODE model into one for which we can compute an appropriate over-approximation on a smaller set of state variables. The algorithm is based on the theory of differential inequalities and consists of two steps. The first step computes a differential hull, which is an ODE system providing lower and upper bounds for each state variable. The hull is constructed such that variables with structurally similar dynamics but originally different parameters may now be represented by the same lower and upper bounds. Based on this, the second step exploits already developed notions of exact model reduction for ODEs to lump such variables. The algorithm is showcased on several case studies and its results are favourably compared against CORA, a well-known tool for reachability analysis of dynamical systems.