多项式常微分方程中代数最强后置条件和最弱前置条件的完备算法

多项式常微分方程组通过多元多项式向量或向量场 $F$ 来描述。安全性断言 $\psi\rightarrow[F]\phi$ 意味着，每当初始状态属于子集 $\psi$（前置条件）时，系统的轨迹将位于状态空间的子集 $\phi$（后置条件）内。我们考虑 $\phi$ 和 $\psi$ 为代数簇，即多项式零点集的情况。特别地，指定后置条件的多项式可以被视为由 $\psi$ 隐含的系统守恒律。验证代数安全性断言的有效性是混合系统等领域中的一个基本问题。我们考虑了该问题的一个广义版本，并提供了一种算法：给定用户指定的多项式集合 $P$ 和代数前置条件 $\psi$，该算法能找到 $P$ 中由 $\psi$ 隐含的最大多项式子集（相对最强后置条件）。在 $\phi$ 的某些假设下，该算法也可用于找到包含在 $\phi$ 中的最大代数不变量以及 $\phi$ 的最弱代数前置条件。此外还考虑了其在连续半代数系统中的应用。通过文献中的几个案例研究展示了所提算法的有效性。