Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 655: | Строка 655: | ||
=== Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. === | === Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. === | ||
- | ''Лекция 7, слайды 22-25 '' | ||
- | |||
'''Оператор <math>X</math> нужно использовать аккуратно:''' | '''Оператор <math>X</math> нужно использовать аккуратно:''' | ||
* с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния, | * с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния, |