一句话：用Lie导数上的L-双模拟刻画多项式ODE的解等价，并给出最小化约简算法。
本文研究多项式常微分方程（ODE）系统的推理与最小化问题。作者以多元多项式环作为描述系统行为的语法，并基于Lie导数为其赋予迁移系统结构，由此定义L-双模拟：两个状态（变量）L-双模拟当且仅当它们在ODE系统中对应相同解。随后，文章用多项式环中在Lie求导下不变的一些理想对L-双模拟进行代数刻画。基于此，提出一个完备算法，通过构造理想升链来计算包含用户指定模板所有有效恒等式实例的最大L-双模拟。该最大L-双模拟可用于构建约简ODE系统，它在原方程的所有线性聚合可得系统中是最小的，且与原系统等价。文中还给出一种计算代价更低的近似约简与线性化技术。全文为FOSSACS 2017论文的扩展修订版。
We consider reasoning and minimization in systems of polynomial ordinary differential equations (ode's). The ring of multivariate polynomials is employed as a syntax for denoting system behaviours. We endow this set with a transition system structure based on the concept of Lie-derivative, thus inducing a notion of L-bisimulation. We prove that two states (variables) are L-bisimilar if and only if they correspond to the same solution in the ode's 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 ode's, equivalent to the original one, but minimal among all those obtainable by linear aggregation of the original equations. A computationally less demanding approximate reduction and linearization technique is also proposed.Comment: 27 pages, extended and revised version of FOSSACS 2017 paper
@article{paperbot826,
title = {Algebra, coalgebra, and minimization in polynomial differential equations},
author = {Michele Boreale},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:14)2019}
}