【问题标题】：Encoding of first order differential equation as First order formula将一阶微分方程编码为一阶公式
【发布时间】：2012-08-13 01:00:11
【问题描述】：

谁能帮我指出使用一阶公式对以下方程进行最佳编码，以便将其作为 SMT 求解器的输入？？

x`=Ax+b

【问题讨论】：

标签： z3 smt

【解决方案1】：

您可以在 Z3 中轻松编码微分方程，因为它只是一组 n^2 + n 个实常数（来自 a_ij 的 n^2，来自 b_i 的 n）和 n 个实变量（x_i）的线性（仿射）函数)。您可以直接在 Z3 中对其进行编码。

dotx_1 = a_11 * x_1 + a_12 * x_2 + a_13 * x_3 + ... + a_1n * x_n + b_1
dotx_2 = a_21 * x_1 + a_22 * x_2 + a_13 * x_3 + ... + a_2n * x_n + b_2
...
dotx_n = a_n1 * x_1 + a_n2 * x_2 + a_n3 * x_3 + ... + a_nn * x_n + b_n

这是 Z3Py 中的 2x2 版本的链接：http://rise4fun.com/Z3Py/pl6P

但是，编码 ODE 的解将很困难，因为线性 ODE 的解涉及指数（超越函数）。对于具有可表示为多项式（在 a_ij 常数、x_i 变量和/或时间变量 t 上）的解的 ODE 类，您将能够将（精确）解编码为 Z3 中的多项式（参见，例如, [1])。

但是，对于涉及先验的一般解决方案，您有许多可能的选择，具体取决于您要完成的任务。一种选择是将先验建模为未解释的函数。在各种 SMT-LIB 基准测试中有一些工作可以做到这一点，但我对这些不是很熟悉，所以希望其他人可以指出它们的链接。如果您想证明有关此类 ODE 解决方案的一些引理，这将是最有用的。像 MetiTarski 这样的一些工具维护超越数的上限和下限近似值（例如，使用截断的泰勒级数，它们是多项式，因此可以在 Z3 中表示），但我不知道 Z3 中的状态，但它看起来像可能会有一些支持，Leonardo 可以评论更多 [6]。

如果您正在进行可达性计算，那么您可能会过度近似范围集，这可以通过 ODE 解的更简单（更抽象）表示来完成。例如，您可以应用混合技术 [2] 的一种变体，并使用矩形动力学过度逼近线性动力学，例如，划分状态空间的一个有趣子集，然后在每个划分中，低于和过度逼近每个维度 dotx_i = a_i1 x_1 + a_i2 x_2 + ... + b_i 与 dothatx_i \in [C, D] 选择一些常数 C 和 D 以确保原始（具体）x_i 的每个解都包含在过度近似（抽象）解 hatx_i 的集合中。 hatx_i 从时间 0 到 t 的解集在区间 [C t + x_i(0), D t + x_i(0)] 内，其中 x_i(0) 是 x_i 在时间 0 的初始条件，t是您想要计算到达设置的有界实时。您可以在所有维度上执行此操作。要计算 C、D（可能会因每个分区和每个维度而异），取决于您对稳健性的关心程度，您可以简单地（在数值上）最大化和最小化每个分区中的原始 ODE dotx_i。

从您的其他帖子看来，您正在尝试模拟混合系统。模拟仍然会在尝试表示超验时遇到问题，因为即使尝试对一条轨迹进行建模（而不是对一组可能的轨迹进行建模）也需要表示解决方案，这通常是先验的。据我所知，这仍然在模拟社区中以数值方式完成[参见，例如，3]，但是有关于“保证”（声音）集成的工作，它提供了数值解与实际（解析) 解决方案 [4, 5]。

[1] 线性向量场族的符号可达性计算。 Gerardo Lafferriere、George J. Pappas 和 Sergio Yovine。符号计算杂志，32(3):231-253，2001 年 9 月。http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf

[2] E. Asarin、T. Dang、A. Girard，非线性系统分析的混合方法，Acta Informatica，43:7，2007，451-476，http://www.springerlink.com/content/q6755l613l856737/

[3] 计算矩阵指数的 19 种可疑方法，25 年后，Cleve Moler 和 Charles Van Loan，SIAM 评论，卷。 45，第 1 期（2003 年 3 月），第 3-49 页，http://www.jstor.org/stable/25054364

[4] 分析函数的自动、有保证的集成，Martin C. Eiermann，BIT NUMERICAL MATHEMATICS，1989，http://www.springerlink.com/content/q2k30rtx2h2n1815/

[5] GRKLib：有保障的龙格库塔图书馆，Bouissou, O., Martel, M.，科学计算、计算机算术和验证数值，2006 年，http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402398

[6] MetiTarski Proofs 的实数代数策略，Grant Olney Passmore，Lawrence C. Paulson 和 Leonardo de Moura。智能计算机数学会议（CICM/AISC），2012，http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf

【讨论】：

感谢您提供如此详细的解释。您正确地指出我正在尝试模拟混合系统。但这并没有结束，我的目的是验证此类系统的某些属性，这显然需要考虑所有可能的轨迹。我遇到过一些方法，比如用矩形近似仿射动力学，但它在很大程度上是一种手动方法，并没有紧密地包含 ODE 的可能解决方案（除非选择了太多近似模型）。我正在为 ODE 解决方案寻找一种自动且可靠的方法，此外还可以与 Z3 集成。
如果您想要一个完全集成的方法，那么您最好的选择可能是过度近似指数。不过，这将是很多工作。您可以查看更多有关 MetiTarski 如何做到这一点的信息。这是关于如何在 PVS 中完成此操作的另一个引用（带有类似教程的解释）：Verified Real Number Calculations: A Library for Interval Arithmetic, Daumas, M. and Lester, D. and Munoz, C., 2009。或者，您可以考虑调用 SpaceEx 或 PHAVer，它们是自动的并支持仿射动力学。然后，您可以将它们生成的到达集解析到 Z3 中。
我对 SpaceEx 有所了解，它实际上是 PHAver 的改进版本。您认为它们可以从 Z3 调用吗？还是您的意思是离线调用？
我也在研究基于区间算术的方法，如 iSAT、VNODE-Lp。你认为它的周边是什么？？
让我们continue this discussion in chat