Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 91 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 719: | Строка 719: | ||
Логика CTL – фрагмент логики CTL*, в котором кванторы могут встречаться только парами, причём в паре должны обязательно находиться один временной и один пространственный кванторы. Например: AG EF(p), A(p U q). | Логика CTL – фрагмент логики CTL*, в котором кванторы могут встречаться только парами, причём в паре должны обязательно находиться один временной и один пространственный кванторы. Например: AG EF(p), A(p U q). | ||
- | |||
- | '''Выразительные возможности CTL* и CTL''' | ||
- | * CTL* и CTL описывают подмножества w-регулярных автоматов над деревьями | ||
- | ** автоматы над деревьями более выразительны, чем автоматы над словами (CTL-формула выполнима на дереве трасс, а не на одной трассе); | ||
- | * CTL и LTL являются подмножествами CTL*; | ||
- | * CTL и LTL не сравнимы по выразительной мощности (пересекаются, но не включают); | ||
- | * на LTL можно описать свойства, не выразимые на CTL: | ||
- | ** CTL не позволяет описать свойства вида []<>(p), | ||
- | ** при помощи []<>(p) в LTL задаются ограничения справедливости; | ||
- | * на CTL можно описать свойства, не выразимые на LTL: | ||
- | ** на LTL нельзя описать свойства вида AGEF(p), | ||
- | ** AGEF(p) используется для описания свойства reset: из любого состояния | ||
- | система может перейти в нормальное | ||
== Верификация программ на моделях == | == Верификация программ на моделях == |