Algebra, Coalgebra, and Minimization in Polynomial Differential Equations

We consider reasoning and minimization in systems of polynomial ordinary differential equations (ODES). The ring of multivariate polynomials is employed as a syntax for denoting system behaviours. We endow polynomials with a transition system structure based on the concept of Lie derivative, thus inducing a notion of L-bisimulation. Two states (variables) are proven L-bisimilar if and only if they correspond to the same solution in the odes system. We then characterize L-bisimilarity algebraically, in terms of certain ideals in the polynomial ring that are invariant under Lie-derivation. This characterization allows us to develop a complete algorithm, based on building an ascending chain of ideals, for computing the largest L-bisimulation containing all valid identities that are instances of a user-specified template. A specific largest L-bisimulation can be used to build a reduced system of odes, equivalent to the original one, but minimal among all those obtainable by linear aggregation of the original equations.