Теоретико-категорное исследование эквивалентностей параллельных моделей с реальным временем

• Автор: Грибовская, Наталия Сергеевна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Новосибирск
• Количество страниц: 142 с.

1. Известные результаты

1.1. Сравнительная характеристика безвременных моделей

1.1.1. Модели параллельных процессов

1.1.2. Сравнительная характеристика приведенных моделей

1.2. Анализ эквивалентностей методами теории категорий

1.2.1. Открытые морфизмы

1.2.2. Теоретикокятегорпая характеризация эквивалентностей . .

2. Трассовые эквивалентности для временных моделей

2.1. Интерливинговая трассовая эквивалентность

2.1.1. Модель временных систем переходов

2.1.2. Категория временных систем переходов СТТБ.

2.1.3. Тготкрьтье морфизмы.
2.1.4. Теоретикокатегорная характеризация эквивалентности .
2.1.5. Разрешимость для конечного подкласса.
2.2. Частичноупорядоченная эквивалентность Пратта
2.2.1. Модель временных структур событий
2.2.2. Категория временных структур событий СТЕвр.
2.2.3. ТР открытые морфизмы.
2.2.4. Теорстикокатегорная характеризация эквивалентности .
2.2.5. Разрешимость для конечного подкласса.
2.3. Частичноупорядоченная трассовая эквивалентность
2.3.1. Категория временных структур событий СТЕЕа.
2.3.2. ТР3Ьоткрытые морфизмы.
2.3.3. Теоретнкокатегорная характеризация эквивалентности .
2.3.4. Разрешимость для конечного подкласса.
3. Тестовые эквивалентности для временных моделей
3.1. Интерливинговая тестовая эквивалентность.
3.1.1. Категория временных систем переходов СТТвиаг
3.1.2. открытые морфизмы.
3.1.3. Теоретикокатегорная характеризация эквивалентности .
3.1.4. Разрешимость для дискретного подкласса
3.2. Частичноупорядоченная тестовая эквивалентность
3.2.1. Категория временных структур событий СТ5
3.2.2. ТТоткрытые морфизмы.
3.2.3. Теоретикокатсчрная характеризация эквивалепстности . .
3.2.4. Разрешимость для дискретного подкласса
4. Бисимуляционные эквивалентности для временных моделей
4.1. Игтерливинговая слабая бисимуляция по Милнеру и Сангиорги . .
4.1.1. Категория временных систем переходов СТТЯмЫз
4.1.2. Рцдоткрытые морфизмы
4.1.3. Теоретикокатегорная характеризация эквивалентности .
4.1.4. Разрешимость для конечного подкласса
4.2. Частичноупорядоченная сильная сохраняющая историю бисимуляция
4.2.1. ТРоткрытые морфизмы
4.2.2. Теоретикокатегорная характеризация эквивалентности . . .
4.2.3. Разрешимость дтя конечного подкласса
Заключение
Литература


Системы переходов и морфизмы между ними формируют категорию Т, в которой композиция двух морфизмов 7, А То i п о7, А Т Тч определена как о о1 о а, А о А То , тождественный морфизм на системе переходов Т это пара 5,,, где тождественная функция на множестве состояний 5, . Заметим, что композиция функций в левой части является всюду определенной функцией, а композиция в правой части частично определенной функцией. В одной из своих ранних работ по Милнер определил модель деревьев синхронизации как модель параллельных процессов и объяснил значение языка в терминах операций над этими деревьями. Определение 1. I л для некоторой строки действий а . Таким образом, мы получили категорию деревьев синхронизации , как полную подкатегорию категории Т. Операция развертки системы переходов в дерево синхронизации появилась как правое обратное отображение к функции включения Т. Заметим, что строка может быт рассмотрена как дерево синхронизации с одной единственной ветвью. Сети Петри можно рассматривать как некоторое обобщение систем переходов. Определение 1. Е Чв 0 функция постусловий. Маркировка сети Петри формализует понятие глобального состояния и определяет выполненные условия. При выполнении события маркировка изменяется. Таким образом выполнение события е из маркировки М приводит к маркировке Л Л М тогда и только тогда, когда ргее С Л С М М М . Два события е и е сети Петри называются параллельными, если ргее П 0. Определение 1. Пусть даны две сети Петри В, , ,, ,,,. Е Ег частично определенная функция, удовлетворяющая следующим уыовиям 0 , 0 ргее ргсе и 0 . V . Отметим, что в работе Нильсен и Винскель доказали, что эта категория коуниверсальна.