x`=Ax+b
您可以在Z3中轻松编码微分方程,因为它只是一组n个线性(仿射)函数,超过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的解涉及指数(超越函数).对于具有可以表示为多项式的解的ODE类(通过a_ij常数,x_i变量和/或时间变量t),您将能够将(精确)解作为Z3中的多项式编码(参见例如, ,[1]).
然而,对于涉及超越性的一般解决方案,您有许多可能的选择,具体取决于您要完成的任务.一种选择是将超验主义建模为未解释的函数.在各种SMT-LIB基准测试中有一些工作可以做到这一点,但我对这些不太熟悉,所以希望其他人可以指出它们的链接.如果你想证明一些关于这种ODE解决方案的引理,这将是最有用的.像MetiTarski一些工具保持上下超越数(例如使用截断泰勒级数,这是多项式,并在Z3因此表示的)的约束近似的,但我不知道这在Z3的地位,但它看起来像可能会有一些支持莱昂纳多可以评论更多[6].
如果您正在进行可达性计算,那么您可能会超出目标集的范围,这可以通过ODE解决方案的更简单(更抽象)表示来完成.举例来说,可以应用该杂交技术[2]的变体和具有矩形动力学overapproximate线性动力学,例如,分区的状态空间的一个有趣的子集,则在每个分区中,之下和之上近似每个维度dotx_i = a_i1 X_1对于一些常数C和D,选择了一些常数C和D,+ a_i2 x_2 + ... + b_i与dothatx_i \,以确保原始(具体)x_i的每个解都包含在overapproximated(抽象)解决方案集合hatx_i中.从时间0设定的hatx_i的解决方案,t是在区间[C T + X_I(0),d T + X_I(0)],其中X -1(0)是X_I的在时间零初始条件,并且t是您想要计算到达设置的有限实时.您可以在所有维度上执行此操作.要计算C,D(可能会因每个分区和每个维度而异),根据您对健全性的关注程度,您可以简单地(数字地)最大化并最小化每个分区中的原始ODE dotx_i.
从您的其他帖子看,您似乎正在尝试模拟混合系统.模拟仍然会遇到试图表示超越性的问题,因为即使试图模拟一条轨迹(而不是模拟可能的轨迹集)也需要代表解决方案,这通常是超越的.据我所知,这仍然在模拟社区中以数字方式完成[参见,例如,3],但是有关于"保证"(声音)整合的工作,它提供了数值解与实际距离有多远的界限(解析) )解决方案[4,5].
[1]线性矢量场族的符号可达性计算.Gerardo Lafferriere,George J. Pappas和Sergio Yovine.Journal of Symbolic Computation,32(3):231 - 233,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]二十五年后的十九种可疑方法来计算矩阵的指数,Cleve Moler和Charles Van Loan,SIAM Review,Vol.45,No.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:有保证的Runge Kutta图书馆,Bouissou,O.,Martel,M.,科学计算,计算机算术和验证数字,2006,http://ieeexplore.ieee.org/xpls/abs_all.jsp？narumber = 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
| 归档时间： |
|
| 查看次数： |
516 次 |
| 最近记录： |