1

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

x`=Ax+b
4

1 回答 1

7

您可以在 Z3 中轻松编码微分方程，因为它只是 n^2 + n 个实常数（a_ij 中的 n^2，b_i 中的 n）和 n 个实变量 (x_i) 上的一组 n 个线性（仿射）函数。您可以直接在 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 中的状态，但它看起来像可能会有一些支持，莱昂纳多可以评论更多 [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 种可疑方法，二十五年后，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

于 2012-08-13T14:22:22.040 回答