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

Версия 17:33, 26 сентября 2010

Презентация: 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-формул