Может ли кто-нибудь помочь мне указать, какое будет лучшее кодирование следующего уравнения с использованием формулы первого порядка, чтобы дать его в качестве входных данных для решателя SMT ??
x`=Ax+b
Кодирование дифференциального уравнения первого порядка в виде формулы первого порядка
Ответы (1)
Вы можете легко закодировать дифференциальное уравнение в Z3, поскольку это всего лишь набор n линейных (аффинных) функций над n ^ 2 + n вещественными константами (n ^ 2 из a_ij, n из b_i) и 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
Вот ссылка на версию 2x2 в Z3Py: http://rise4fun.com/Z3Py/pl6P
Однако кодирование решения ОДУ будет затруднено, поскольку решение линейных ОДУ включает экспоненты (трансцендентные функции). Для класса ОДУ с решениями, которые могут быть представлены в виде полиномов (по константам a_ij, переменным x_i и/или временной переменной t), вы могли бы закодировать (точные) решения как полиномы в Z3 (см., например, , [1]).
Однако для общих решений, связанных с трансцендентными, у вас есть много возможных вариантов, в зависимости от того, чего вы пытаетесь достичь. Один из вариантов — это моделирование трансцендентального как неинтерпретируемой функции. В различных тестах SMT-LIB есть некоторые работы, которые делают это, но я не очень хорошо знаком с ними, поэтому, надеюсь, кто-то еще может указать на них ссылку. Это было бы очень полезно, если бы вы хотели доказать некоторые леммы о решениях таких ОДУ. Некоторые инструменты, такие как MetiTarski, поддерживают аппроксимацию трансцендентных величин сверху и снизу (используя, например, усеченные ряды Тейлора, которые являются многочленами и, следовательно, могут быть представлены в Z3), но я не знаю о статусе этого в Z3, но похоже, может быть некоторая поддержка, которую Леонардо мог бы прокомментировать больше [6].
Если вы выполняете вычисления достижимости, то вы можете переаппроксимировать множество досягаемости, что можно сделать с помощью более простых (более абстрактных) представлений решений ОДУ. Например, вы можете применить вариант метода гибридизации [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 в нулевое время, а t — это ограниченное реальное время, в течение которого вы хотите вычислить настройку охвата. Вы можете сделать это во всех измерениях. Чтобы вычислить C, D (которые, вероятно, будут различаться для каждого раздела и каждого измерения), в зависимости от того, насколько вы заботитесь о надежности, вы можете просто (численно) максимизировать и минимизировать исходный ODE dotx_i в каждом разделе.
Из других ваших сообщений похоже, что вы пытаетесь смоделировать гибридные системы. Моделирование по-прежнему будет страдать от проблем с попыткой представить трансцендентные, поскольку даже попытка смоделировать одну траекторию (вместо моделирования набора возможных траекторий) потребует представления решения, которое в целом является трансцендентным. Насколько мне известно, это все еще делается в сообществе моделирования численно [см., например, 3], но есть работа над «гарантированной» (надежной) интеграцией, которая устанавливает границы того, насколько далеко численное решение от фактического (аналитического). ) решение [4, 5].
[1] Вычисления символьной достижимости для семейств линейных векторных полей. Херардо Лафферриер, Джордж Дж. Паппас и Серхио Йовин. Journal of Symbolic Computation, 32(3):231-253, сентябрь 2001 г. http://www.seas.upenn.edu/~pappasg/papers/JSC01.pdf
[2] Э. Азарин, Т. Данг, А. Жирар, Методы гибридизации для анализа нелинейных систем, Acta Informatica, 43:7, 2007, 451-476, http://www.springerlink.com/content/q6755l613l856737/
[3] Девятнадцать сомнительных способов вычисления экспоненты матрицы, двадцать пять лет спустя, Клив Молер и Чарльз Ван Лоан, SIAM Review, Vol. 45, № 1 (март 2003 г.), стр. 3–49, http://www.jstor.org/stable/25054364
[4] Автоматическая гарантированная интеграция аналитических функций, Мартин С. Айерманн, БИТ ЧИСЛОВАЯ МАТЕМАТИКА, 1989, http://www.springerlink.com/content/q2k30rtx2h2n1815/
[5] GRKLib: гарантированная библиотека Рунге-Кутты, Буиссу, О., Мартель, М., Научные вычисления, компьютерная арифметика и проверенные числа, 2006 г., http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4402398
[6] Настоящие алгебраические стратегии для доказательств Метитарского, Грант Олни Пассмор, Лоуренс С. Полсон и Леонардо де Моура. Конференция по интеллектуальной компьютерной математике (CICM/AISC), 2012 г., http://research.microsoft.com/en-us/um/people/leonardo/CICM2012.pdf
person
Taylor T. Johnson
schedule
13.08.2012
Спасибо за такое подробное объяснение. Вы правильно заметили, что я пытаюсь смоделировать гибридную систему. Но на этом не заканчивается, моя цель состоит в том, чтобы проверить определенные свойства таких систем, которые, очевидно, должны учитывать все возможные траектории. Я сталкивался с такими методами, как аппроксимация аффинной динамики прямоугольной, но это в значительной степени ручной метод, и он не охватывает возможные решения ОДУ (пока не выбрано слишком много приблизительных моделей). Я ищу автоматический и звуковой метод для решений ODE, который, кроме того, может быть интегрирован с Z3.
- person hafizul asad; 13.08.2012
Если вам нужен полностью интегрированный метод, лучшим вариантом, вероятно, будет завышение экспоненты. Хотя это будет много работы. Вы можете узнать больше о том, как MetiTarski это делает. Вот еще одна цитата (с пояснением в стиле учебника) о том, как это было сделано в PVS: Подтвержденные вычисления действительных чисел: библиотека для интервальной арифметики, Daumas, M. and Lester, D. and Munoz, C., 2009. В качестве альтернативы, вы можете посмотреть на вызовы SpaceEx или PHAVer, которые являются автоматическими и поддерживают аффинную динамику. Затем вы можете проанализировать наборы охвата, которые они генерируют, в Z3.
- person Taylor T. Johnson; 13.08.2012
Я немного знаю о SpaceEx, который на самом деле является улучшенной версией PHAver. Как вы думаете, их можно вызывать из Z3??? или вы хотите сделать это в автономном режиме?
- person hafizul asad; 13.08.2012
Я также смотрю на методы, основанные на интервальной арифметике, такие как iSAT, VNODE-Lp. Что вы думаете по этому поводу??
- person hafizul asad; 13.08.2012
SpaceEx можно использовать для доказательства того, что свойство безопасности P (т. е. предикат в пространстве состояний) сохраняется, вычисляя множество достижимых состояний R (еще один предикат в пространстве состояний) и проверяя, является ли пересечение \neg P и R пустым. . SpaceEx может выводить набор достижимых состояний (или, чаще, набор достижимых состояний до некоторого времени T). Вы можете получить R от SpaceEx, разобрать его, а затем использовать как предикат в Z3. По сути, R будет некоторым линейным неравенством над непрерывными переменными (т. Е. Многоугольником или их объединением). Затем вы можете использовать Z3, чтобы проверить, пусто ли R \cap \neg P.
- person Taylor T. Johnson; 13.08.2012
Одна проблема, которая меня беспокоит, заключается в том, что свойство, которое я хочу проверить, основано на частоте, то есть я хочу показать, что все траектории имеют частоты с полосой пропускания. Теперь, поскольку SpaceEx дает завышенный набор досягаемости ... он может создавать паразитные частоты. ваш комментарий по этому поводу?
- person hafizul asad; 13.08.2012
В общем, вам понадобятся переоценки, иначе вы потеряете завершение или надежность, поскольку вы не можете вычислить точное множество досягаемости по причинам разрешимости. Поскольку вас интересуют свойства частоты, в этой статье описывается логика для свойств времени и частоты: ссылка. Это для проверки во время выполнения, поэтому я не видел никаких упоминаний о наборах охвата. Вы также можете воспользоваться инструментом Breach, который используется в статье: ссылка.
- person Taylor T. Johnson; 13.08.2012
давайте продолжим это обсуждение в чате
- person Taylor T. Johnson; 13.08.2012
