Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 403: | Строка 403: | ||
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. === | === Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. === | ||
- | Представим трассу в форме интерпретации I: <math>I(tr) = | + | Представим трассу в форме интерпретации I: <math>I(tr) = <\mathbb{N}, \leqslant, \xi></math> |
* <math>\mathbb{N}</math> - множество натуральных чисел | * <math>\mathbb{N}</math> - множество натуральных чисел | ||
* <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math> | * <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math> | ||
Строка 409: | Строка 409: | ||
Рассмотрим трассы tr и tr' такие, что | Рассмотрим трассы tr и tr' такие, что | ||
- | * <math>I(tr) = | + | * <math>I(tr) = <\mathbb{N}, \leqslant, \xi>, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math> |
- | * <math>I(tr') = | + | * <math>I(tr') = <\mathbb{N}, \leqslant, \xi'>, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> |
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \prec tr'</math>), если | Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \prec tr'</math>), если |