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