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 -bisimulation. Two states (variables) are proven -bisimilar if and only if they correspond to the same solution in the ODEs system. We then characterize -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 -bisimulation containing all valid identities that are instances of a user-specified template. A specific largest -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.