将一阶微分方程编码为一阶公式 [英] Encoding of first order differential equation as First order formula

问题描述

x`=Ax+b

推荐答案

您可以在 Z3 中轻松地对微分方程进行编码，因为它只是 n^2 + n 个实常数 (n^2 来自 a_ij，n 来自 b_i) 和 n 个实变量 (x_i).您可以直接在 Z3 中对其进行编码.

You can encode the differential equation easily in Z3 as it is just a set of n linear (affine) functions over n^2 + n real constants (n^2 from a_ij, n from b_i) and n real variables (x_i). You can encode this directly in 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

Here's a link for a 2x2 version of this in Z3Py: http://rise4fun.com/Z3Py/pl6P

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

However, encoding the solution of the ODEs will be difficult, as the solution of linear ODEs involve exponentials (transcendental functions). For the class of ODEs with solutions that can be represented as polynomials (over the a_ij constants, x_i variables, and/or a time variable t), you would be able to encode the (exact) solutions as polynomials in Z3 (see, e.g., [1]).

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

For the general solutions that involve transcendentals however, you have many possible options, depending on what you are trying to accomplish. One option is modeling the transcendentals as uninterpreted functions. There is some work in various SMT-LIB benchmarks that do this, but I am not so familiar with these, so hopefully someone else can point out a link to them. This would be most useful if you wanted to prove some lemmas about the solutions of such ODEs. Some tools like MetiTarski maintain upper and lower bound approximations of transcendentals (using, e.g., truncated Taylor series, which are polynomials, and hence representable in Z3), but I'm not aware of the status of this in Z3, but it looks like there may be some support that Leonardo could comment on more [6].

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

If you are doing reachability computations, then you could overapproximate the reach set, which can be done with simpler (more abstract) representations of the solutions of the ODEs. For instance, you could apply a variant of the hybridization technique [2] and overapproximate the linear dynamics with rectangular dynamics, e.g., partition an interesting subset of the state space, then in each partition, under and over approximate each dimension dotx_i = a_i1 x_1 + a_i2 x_2 + ... + b_i with dothatx_i \in [C, D] for some constants C and D chosen to ensure every solution of the original (concrete) x_i is contained in the set of overapproximated (abstract) solutions hatx_i. The set of solutions of hatx_i from time 0 to t is in the interval [C t + x_i(0), D t + x_i(0)], where x_i(0) is the initial condition of x_i at time zero, and t is the bounded real time you want to compute the reach set up-to. You can do this over all dimensions. To compute the C, D (which will likely vary for each partition and each dimension), depending on how much you care about soundness, you can simply (numerically) maximize and minimize the original ODE dotx_i in each partition.

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

From your other posts, it looks like you are trying to simulate hybrid systems. Simulation will still suffer the problems in trying to represent transcendentals, as even trying to model one trajectory (instead of modeling the set of possible trajectories) will require representing the solution, which is in general transcendental. To my knowledge, this is still done in the simulation community numerically [see, e.g., 3], but there is work on "guaranteed" (sound) integration, which provides bounds on how far off the numerical solution is from the actual (analytic) solution [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

[1] Symbolic reachability computations for families of linear vector fields. Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Journal of Symbolic Computation, 32(3):231-253, September 2001. http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf

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

[2] E. Asarin, T. Dang, A. Girard, Hybridization methods for the analysis of nonlinear systems, Acta Informatica, 43:7, 2007, 451-476, http://www.springerlink.com/content/q6755l613l856737/

[3] 计算矩阵指数的 19 种可疑方法，二十五年后，Cleve Moler 和 Charles Van Loan，SIAM 评论，卷.45, No. 1 (Mar., 2003), pp. 3-49, http://www.jstor.org/stable/25054364

[3] Nineteen Dubious Ways to Compute the Exponential of a Matrix, Twenty-Five Years Later, Cleve Moler and Charles Van Loan, SIAM Review, Vol. 45, No. 1 (Mar., 2003), pp. 3-49, http://www.jstor.org/stable/25054364

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

[4] Automatic, guaranteed integration of analytic functions, Martin C. Eiermann, BIT NUMERICAL MATHEMATICS, 1989, http://www.springerlink.com/content/q2k30rtx2h2n1815/

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

[5] GRKLib: a Guaranteed Runge Kutta Library, Bouissou, O., Martel, M., Scientific Computing, Computer Arithmetic and Validated Numerics, 2006, http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402398

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

[6] Real Algebraic Strategies for MetiTarski Proofs, Grant Olney Passmore, Lawrence C. Paulson, and Leonardo de Moura. Conference on Intelligent Computer Mathematics (CICM/AISC), 2012, http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf

这篇关于将一阶微分方程编码为一阶公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！