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

Текущая версия

Презентация: http://savenkov.lvk.cs.msu.su/mc/lect8.pdf
Диктофонная запись: 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-формул