Редактирование: ВПнМ, 08 лекция (от 04 апреля)

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

'''Презентация:''' http://savenkov.lvk.cs.msu.su/mc/lect8.pdf<br />
'''Диктофонная запись:''' http://esyr.org/lections/audio/verification_2008_summer/verification_08_04_04.ogg

= Темпоральные формулы, LTL =

Что было на пред. лекции: при помощи автомата Бюхи удобно описать повдение молдели. Если мы будем этот автомат будем параллельно композировать с нашей моделью, то будем проверять, выполняется св-во или нет. Однако, многин св-ва задавать при помощи автоматов неудобно. Например, на ваш запрос будет дан отклик. Какая ситуация и была раньше. Поэтому нужен более удобный способ. Таким способом явл. темп. логика.

Свойств бывает два вида: безопасности (не будет плохого) и живучести (когда-то случится хорошее). Любое св-во безопасности можно сформ. на сост. программы. можно сформулировать условие и если оно удовл., то всё хорошо. Для форм. и проверки св-в автоматы Б. и темп. логика не нужны. Нужно просто генеирровать сост. программы и проверять, удовл. сост. или нет. Будут проблемы с размеромЮ, но их можно решить. Но есть и др. св-ва. Есть св-ва живучести, которые задаются посл. сост. Автоматами задавать их неудобно. Для проверки св-в надо показать, что какое-то поведение либо неизбежно, либо невозможно. И нам надо проверять св-во на беск. проходах. Алгоритмы другие, способ другой. Поскольку св-ва вложные, товсе св-ва описываются на LTL.

Пример св-ва безопасности: ...

Пример поведения системы: есть два рпоцесса, две перем p и q. ... Мы можем взять систему переходов и постр. композицию. Чтобы проверить св-во, мы применим автомат к пространству сост. Мы увидим, что наше свойство нарушается в двух сост. системы. Какбы ни шло ..., мы придём в одно из двух этих сост. Св-во наруш.

Свойство живучести: как тольько p стало истинным, через конечное число шагов q станет истинным. Нарушение свойства: после того, как p истиинно, q никогда не станет истинным.

То есть, если все возможные трассы нашей системы будут допускаемы для данного автомата, наше св-во нарушается.

== Примеры св-в живучести: ==
* p всегда истинно
* p в конце концов станет истинным
* p всегда в конце конфов станет ложным ещё раз
* p всегда ведёт к отрицпнию q
* p всегда ведёт к тому, что q станет истинным
Если то св-во, которое было в примере, описать чере АБ просто, то эти уже нетривиально, Для их описания исп. темп. логика.

== LTL ==
* Явный, лаконич., непротивореч. спосоьб опис. требований
* Был создан философами для описания темп. связей.

Мы описываем св-ва, которые описываются на трассах. Есть логики, которые описываются на деревьях. Ещё есть логики, которые отлич. по временным отношениям. Ещё есть простр-временные логики.

Семантика LTL опред. на автоматах Б. Это значит, что каждому утв. LTL соотв. класс проходов автоматов Бюхи. Соотв., язык авт. Бюхи позв. это свойство распознавать.

=== Операторы ===

=== Выполнимость формул ===

== Паттерны ==

=== Цмкличность и стабильность ===
* Цикличность: [] <> p
* Стабильность: <> [] p

=== Распространные паттерны LTL===
* [] p --- всегда p --- инвариант
* <> p --- рано или поздно --- гарантия
* p -> <> q --- если p, то рано или поздно q --- гарантия отклика
* p -> q U r --- если p, то q, затем r --- приоритет
* <> p -> <> q --- если когда-то p, то когда-то q --- корелляция

=== Эквивалентные формулы ===

=== Примеры свойств живучести ===
* p всегда истинно --- [] p
* p в конце концов станет истинным --- <> [] !p
* p всегда в конце конфов станет ложным ещё раз --- [] <> !p
* p всегда ведёт к отрицпнию q --- [] (p -> !q)
* p всегда ведёт к тому, что q станет истинным --- [](p -> <> q)
Тут тонкий момент, потому что когда гооврим что что-то ведёт к чему-то, то мы можем иметь разные вещи в виду.

=== Описание требований ===
( "p приводит к q"
** p -> q --- мы применяем это к только к первому состоянию. Не подходит.
** [] p -> q --- spin это воспримет это как ([] p) -> q. Не подходит.
** [] (p -> q) --- Логическая имплю буде проверяться на всех сост., не задана причинно-след. связь. Не подходит.
** [] (p -> <> q) --- e;t kexit? yj tcnm ghj,ktvf. Если q станет истинным в том же сост., что и p, то не факт, что связь будет. Хочется зафиксировать, что меджу p и q прошёл промежуток времени. Не подходит
** [] (p -> X(<> q)) --- уже лучше, но подходит если p всегда ложно. Скорее всего, не подходит.
** [] (p -> X(<> q)) &7 (<> p) --- скорее всего, это и имели в виду

=== Правильная интерпретация LTL-формул ===

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_08_%D0%BB%D0%B5%D0%BA%D1%86%D0%B8%D1%8F_%28%D0%BE%D1%82_04_%D0%B0%D0%BF%D1%80%D0%B5%D0%BB%D1%8F%29

Редактирование: ВПнМ, 08 лекция (от 04 апреля)

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 42: / Строка 42: @@
 * Стабильность: <> [] p
-=== Распространённые паттерны LTL===
+=== Распространные паттерны LTL===
 * [] p --- всегда p --- инвариант
 * <> p --- рано или поздно --- гарантия