Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 91 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 452: | Строка 452: | ||
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. === | === Абстракция. Абстракция графов программ. Отношение слабой симуляции. === | ||
- | Лекция 10, слайды 8 - 11 | ||
- | Программа PG' ''корректно моделирует'' программу PG тогда и только тогда, когда система переходов TS(PG') корректно моделирует систему переходов TS(PG). | ||
- | |||
- | Будем говорить, что PG' моделирует PG, если | ||
- | * в PG' присутствуют переменные, соответствующие наблюдаемым переменным PG | ||
- | * все действия PG, влияющие на наблюдаемые переменные, отражены в модели <i>(наблюдаемые операторы)</i> | ||
- | * модель корректно воспроизводит возможные последовательности изменения значений наблюдаемых переменных, присутствующих в PG | ||
- | |||
- | '''Отношение слабой симуляции''' не сохраняет количество шагов между состояниями. В связи с этим, не сохраняются свойства, не инвариантные к | ||
- | прореживанию (LTL: оператор neXt). | ||
== Логика LTL, автоматы Бюхи == | == Логика LTL, автоматы Бюхи == |