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

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

Автор: Ломазова, Ирина Александровна

Шифр специальности: 05.13.17

Научная степень: Докторская

Год защиты: 2001

Место защиты: Переславль-Залесский

Количество страниц: 263 с. ил

Артикул: 336979

Автор: Ломазова, Ирина Александровна

Стоимость: 250 руб.

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

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.

Рекомендуемые диссертации данного раздела

28.06.2016

+ 100 бесплатных диссертаций

Дорогие друзья, в раздел "Бесплатные диссертации" добавлено 100 новых диссертаций. Желаем новых научных ...

15.02.2015

Добавлено 41611 диссертаций РГБ

В каталог сайта http://new-disser.ru добавлено новые диссертации РГБ 2013-2014 года. Желаем новых научных ...


Все новости

Время генерации: 0.221, запросов: 244