Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 675: | Строка 675: | ||
* Свойство f, инвариантное к прореживанию, либо истинно для всех трасс из <math>E(\psi)</math>, либо ни для одной из них: | * Свойство f, инвариантное к прореживанию, либо истинно для всех трасс из <math>E(\psi)</math>, либо ни для одной из них: | ||
** <math>\psi \models f ~ \Rightarrow ~ \forall v \in E(\psi), v \models f </math> | ** <math>\psi \models f ~ \Rightarrow ~ \forall v \in E(\psi), v \models f </math> | ||
- | * истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы меняют свои значения; | + | * истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы |
- | * Теорема: все формулы LTL без оператора <math>X</math> инвариантны к прореживанию. | + | меняют свои значения; |
- | + | * Теорема: все формулы LTL без оператора <math>X</math> инвариантны к | |
+ | прореживанию. | ||
=== Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin. === | === Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin. === |