1

誰かが、SMTソルバーへの入力として与えるために、一次式を使用して次の方程式の最良のエンコードが何であるかを指摘するのを手伝ってもらえますか？

x`=Ax+b
4

1 に答える 1

7

微分方程式は、n^2 + n 実定数 (a_ij から n^2、b_i から n) および n 実変数 (x_i) に対する n 線形 (アフィン) 関数のセットであるため、Z3 で簡単にエンコードできます。これを 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])。

ただし、超越を含む一般的なソリューションの場合、達成しようとしていることに応じて、多くの可能なオプションがあります。1 つのオプションは、超越を未解釈の関数としてモデル化することです。これを行うさまざまな SMT-LIB ベンチマークでいくつかの作業がありますが、私はこれらにあまり詳しくないので、他の誰かがそれらへのリンクを指摘できることを願っています。これは、そのような ODE の解に関する補題を証明したい場合に最も役立ちます。MetiTarski のようないくつかのツールは、超越の上限と下限の近似を維持します (たとえば、多項式であり、したがって Z3 で表現可能な切り捨てられたテイラー級数を使用します)、Z3 でのこの状態を認識していませんが、次のようになります。レオナルドがさらにコメントできるいくつかのサポートがあるかもしれません [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) は、時間ゼロにおける x_i の初期条件です。t は、リーチ設定を計算する制限付きリアルタイムです。これは、すべての次元で実行できます。C、D (パーティションごと、次元ごとに異なる可能性があります) を計算するには、健全性をどの程度気にするかに応じて、各パーティションの元の ODE dotx_i を単純に (数値的に) 最大化および最小化できます。

他の投稿から、ハイブリッド システムをシミュレートしようとしているように見えます。1 つの軌道をモデル化しようとしても (可能な軌道のセットをモデル化する代わりに)、一般に超越的な解を表す必要があるため、シミュレーションは超越を表現しようとする際に依然として問題に悩まされます。私の知る限り、これはまだシミュレーション コミュニティで数値的に行われています [たとえば、3 を参照]。 ) ソリューション [4, 5]。

[1] 線形ベクトル フィールドのファミリに対する記号到達可能性の計算。ジェラルド・ラフェリエール、ジョージ・J・パパス、セルジオ・ヨヴィン。Journal of Symbolic Computation、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 Review、Vol. 45、No. 1 (2003 年 3 月)、pp. 3-49、http: //www.jstor.org/stable/25054364

[4] 分析関数の自動保証統合、Martin C. Eiermann、BIT NUMERICAL MATHEMATICS、1989、http://www.springerlink.com/content/q2k30rtx2h2n1815/

[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 Proofs の Real Algebraic Strategies、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 に答える