Анализ семантических свойств некоторых классов программ и сетей Петри

• Автор: Ломазова, Ирина Александровна
• Шифр специальности: 05.13.17
• Научная степень: Докторская
• Год защиты: 2001
• Место защиты: Переславль-Залесский
• Количество страниц: 263 с. : ил

1 Предварительные сведения

1.1 Мультимножества.

1.2 Квазиуиорядоченные мнокества.

1.3 Системы помеченных переходов.

1.4 Сети Петри

1.5 Сети Петри высокого уровня

2 Вложенные сети Петри двухуровневые системы

2.1 Сети Петри и моделирование мультиагентных систем .

2.2 Начальные примеры.

2.3 Структура сети

2.4 Поведение сети

2.5 Вложенные сети Петри как вполне структурированные системы переходов.
2.6 Анализ семантических свойств
3 Многоуровневые и рекурсивные вложенные сети Петри
3.1 Определение структуры и поведения.
3.2 Многоуровневые сети как вполне структурированные системы переходов
3.3 Алгоритмы анализа для многоуровневых сетей
3.4 Пример рекурсивной вложенной сети
3.5 Вложенные сети с автономными и локализованными элементами
3.6 Проблемы останова и поддержки активности переходов для рекурсивных сетей.0
4 Сравнение вложенных сетей с другими формальными мо
делями
4.1 Языковая выразительность вложенных сетей Петри
4.2 Вложенные сети Петри и алгебры процессов.
4.3 Вложенные сети Петри и другие классы сетей Петри
4.4 Вложенные сети Петри и Линейная логика.
5 Семантика и доказательство некоторых свойств сетей Петри
5.1 Каузальная семантика для элементарных сетей Петри . . .
5.2 Каузальная семантика для сетей позицийпереходов
5.3 Временная логика для доказательства свойств безопасности
5.4 Анализ поведения сетей высокого уровня
5.5 Анализ поведения модульных сетей Петри
6 Семантика и верификация последовательных программ
6.1 Хоаровская логика для функциональных программ
6.2 Функциональные программы и присваивание
6.3 Аксиоматическая семантика программ над абстрактными типами данных.
6.4 Процедурная реализация абстрактных типов данных
Заключение
Список литературы


С. В частности для С з, где . СОСТОИТ В проверке ДОСТИЖИМОСТИ ИЗ СОСТОЯНИИ . Для решения проблемы покрытия в случае вполне структурированных систем переходов используется метод насыщения i , , , основанный на свойстве стабилизации возрастающей последовательности верхних конусов см. Пусть 5, вполне структурированная система переходов. Напомним, что Л у Е 5 З. Е Л у л, где Л С . Через будем обозначать множество Е г непосредственных предшественников состояния . Соответственно для множества состояний X С полагаем X . Пусть С верхний конус. Рассмотрим последовательность С0 С С, С . С Су ii i i. Через обозначим предел этой последовательности, т. С. Решение проблемы покрытия для заданных СОСТОЯНИЙ И 5 состоит в проверке того, что 5 Е геГТ . Утверждение 1 Если С С верхний конус относительно вполне упорядочиваемого порядка , то С также является верхним конусом относительно . Доказательство. Покажем сначала, что если С верхний конус, то С также является верхним конусом. Действительно, пусть состояние С, т. С такое что 5 у и пусть г . По свойству совместимости найдется состояние г такое, что г г и г , т. Е и г 6 С. Это значит, что г 6 С. Поскольку объединение двух верхних конусов также является верхним конусом, применив индукцию, из доказанного получаем, что для любого г 0 множество С,, где С0 С, i С iС, также является верхним конусом. Пусть теперь Е С. Тогда для некоторого i 0, Е С,. Поскольку i верхний конус, из г следует г С, а значит игЕ РгсАЛС. Из приведенного выше утверждения и утверждения 1.