Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 93 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 428: | Строка 428: | ||
''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели | ''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели | ||
больше состояний )'' | больше состояний )'' | ||
+ | |||
+ | ''' Достаточное условие корректности модели ''': | ||
+ | * <math>Act' \subseteq Act</math> | ||
+ | * <math>AP' \subseteq AP</math> | ||
+ | * <math>\exists \alpha:S \rightarrow S'</math> такая, что | ||
+ | ** <math>s_0' = \alpha(s_0)</math> | ||
+ | ** <math>\forall s_1, s_2 \in S ~:~ s_1 \overset{a}{\rightarrow} s_2 ~~ \Rightarrow ~~ \alpha(s_1) \overset{a}{\rightarrow}' \alpha(s_2)</math> | ||
+ | ** <math> \forall s \in S ~~ \Rightarrow ~~ L'(\alpha(s)) = L(s) \cap AP' </math> | ||
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === | === Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === |