Некоторые методы ресурсного анализа сетей Петри

• Автор: Башкин, Владимир Анатольевич
• Шифр специальности: 05.13.17
• Научная степень: Докторская
• Год защиты: 2014
• Место защиты: Ярославль
• Количество страниц: 268 с. : ил.

Содержание
Введение

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

1.1. Множества и отношения

1.2. Эквивалентность поведений

1.3. Сети Петри

1.4. Ресурсы в сетях Петри

Глава 2. Некоторые методы поиска бисимуляционно-эквивалентных ресурсов

2.1. Бисимуляция в ограниченных сетях

2.2. Ограниченное подобие ресурсов

2.3. Расслоенное подобие ресурсов

2.4. Подобие обобщенных ресурсов
2.5. Адаптивное управление процессами на основе подобия ресурсов .
Глава 3. Некоторые методы анализа сетей с одномерным ресурсом
3.1. Одномерные полулинейные множества
3.2. Односчетчиковые контуры
3.3. Алгоритмы анализа
3.4. Правильная организованность
3.5. Потоки работ с ресурсом
Глава 4. Модели с активными и обобщёнными ресурсами
4.1. Сети активных ресурсов
4.2. Модульные АР-сети
4.3. Модифицированные АР-сети
4.4. Автоматы, управляемые ресурсами

4.5. Клеточные сети с бесконечномерным ресурсом
Заключение
Благодарности
Литература

Введение
Актуальность темы исследования. В последние десятилетия большой и устойчивый интерес проявляется к математическим средствам моделирования и анализа сложных параллельных и распределенных систем, к которым относятся, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы и алгоритмы, протоколы взаимодействия (коммуникационные, верифицирующие), модели технологических и бизнес-процессов. При разработке подобных систем, как правило, высок риск возникновения ошибки на стадии проектирования и чрезвычайно высока цена проявления ошибки на стадии эксплуатации. Все это обуславливает интерес к формальным математическим средствам анализа и верификации, позволяющим дать ответы на вопросы о свойствах модели, например, о наличии конфликтов, тупиков или неограниченных состояний (переполнений).
Одним из наиболее популярных формализмов для моделирования и анализа параллельных и распределенных систем являются сети Петри. Понятие сети Петри было введено в 1962 году Карлом-Адамом Петри. С тех пор теория сетей Петри сильно разрослась и продолжает активно развиваться. Причиной популярности сетей Петри является математическая строгость, простота и наглядность описания параллелизма, а также удобное графическое представление модели.
Среди отечественных исследований по сетям Петри и спецификации и анализу распределенных систем отметим работы Н. А. Анисимова, О. Л. Бандман, И. Б. Вирбицкайте, В. В. Воеводина, Н. В. Евтушенко, В. А. Захарова, Ю. Г. Карпова, В. Е. Котова, И. А. Ломазовой, В. А. Непомнящего, Р. И. Подловченко, Р. Л. Смелянского, В. А. Соколова, Л. Н. Столярова, Л. А. Черкасовой.
Сети Петри позволяют с достаточной степенью детализации моделировать вычислительные процессы, процессы управления в распределенных системах и протоколы взаимодействия. В них имеются простые конструкции для описания структур параллелизма: последовательная композиция, выбор, параллельное
Рассмотрим шаг ,V| Д jj. Тогда существует шаг s2 Д такой что (/р є R, и, следовательно, существует шаг 52 -> 'Д такой что (.у], s'2) є У?2, то есть (jj, ,v() є R2 ° Ri. Аналогично можно показать, что отношение Н2 о Rx обладает свойством переноса в обратном направлении. Таким образом, R2 ° Ri — бисимуляция.
Свойство 4: Поскольку свойства 2 и 3 могут быть обобщены для объединения (композиции) бесконечного числа множеств, а
R = (R U R~1)* = Id(S) U (Л U /С1) U (/? U /Г1)2 U ■ • ■ U (R U R~l)k U ...,
то очевидно, что R — бисимуляция.
Свойство 6 является очевидным следствием свойства 3, а свойство 7 — следствием свойств 3 и 4. □
Бисимуляция — достаточно тонкая эквивалентность на множестве состояний, адекватно отражающая свойства системы в семантике ветвящегося времени. Однако, в силу своей универсальности, для многих классов систем отношение бисимуляции неразрешимо, то есть не существует алгоритма, отвечающего на вопрос, являются ли данные два состояния бисимулярными или нет.
Бисимуляционная эквивалентность изучалась для различных классов формальных моделей [56, 63, 105, 136, 139-142, 145, 173, 194, 196]. Был получен ряд результатов по ее разрешимости. В частности, бисимуляция разрешима для всех классов систем с конечным числом состояний (конечных автоматов), так как в них для проверки бисимулярности достаточно просто перебрать множество состояний. Бисимуляция разрешима также для таких классов моделей с бесконечным множеством состояний, как:
- базовые параллельные процессы (ВРР, Basic Parallel Processes) [105, 106, 137],
- базовые алгебры процессов (ВРА, Basic Process Algebra) [63, 107],