Редактирование: ВПнМ, 08 лекция (от 04 апреля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | '''Презентация:''' 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 = | ||
Строка 42: | Строка 39: | ||
* Стабильность: <> [] p | * Стабильность: <> [] p | ||
- | === | + | === Hfcghjcnhfyy`yyst gfnnthys ДЕД === |
- | * [] p --- всегда p --- | + | * [] p --- всегда p --- инфариант |
* <> p --- рано или поздно --- гарантия | * <> p --- рано или поздно --- гарантия | ||
* p -> <> q --- если p, то рано или поздно q --- гарантия отклика | * p -> <> q --- если p, то рано или поздно q --- гарантия отклика |