Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 694: | Строка 694: | ||
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. === | === Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. === | ||
- | При помощи конструкции never можно описать любой | + | При помощи конструкции never можно описать любой w-регулярный автомат над словами |
'''Выразительная мощность LTL''' | '''Выразительная мощность LTL''' | ||
Строка 707: | Строка 707: | ||
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного. | (p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного. | ||
- | <math>\exists </math> t | + | <math>\exists </math> t.t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p) |
LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы | LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы | ||
Строка 713: | Строка 713: | ||
'''Логика СTL*''' | '''Логика СTL*''' | ||
* Логика ветвящегося времени: | * Логика ветвящегося времени: | ||
- | ** использует кванторы ∀ и ∃ | + | ** использует кванторы ∀ и ∃ |
** использует F вместо <> и G вместо [] | ** использует F вместо <> и G вместо [] | ||
'''Логика СTL''' | '''Логика СTL''' | ||
- | Логика CTL – фрагмент логики CTL*, в котором | + | Логика CTL – фрагмент логики CTL*, в котором под управлением квантора пути (E или A) может находиться не более дного |
+ | оператора X или U | ||
'''Выразительные возможности CTL* и CTL''' | '''Выразительные возможности CTL* и CTL''' |