Анализ корректности дискретных систем с асинхронными взаимодействиями

• Автор: Анишев, Петр Александрович
• Шифр специальности: 05.13.01
• Научная степень: Кандидатская
• Год защиты: 1984
• Место защиты: Новосибирск
• Количество страниц: 176 c. : ил

Оглавление
Введение

Глава I. Сети Петри и параллельные графсхемы алгоритмов

1.1. Сети Петри.

1.1.1. Определение основных понятий . ХЗ

1.1.2. Классы сетей Петри .

1.1.3. Расширения сетей Петри .

1.2. Параллельные г рафсхе.мы алгоритмов.

1.2.1. Определение основных понятий .

1.2.2. Корректность параллельных графсхем алгоритмов . . зх

1.2.3. Структурированные ПГСА

1.2.4. Методы проверки ПГСА на корректность
1.3. Переход, от ПГСА к сети Петри
1.3.1. Правила перехода
1.3.2. Анализ правил перехода
1.4. Постановка задачи проверки ПГСА на корректность . .
Выводы к главе I.
Глава П. Редукция сетей Петри
2.1. Постановка задачи редукции
2.1.1. Определение условий
2.1.2. Отличия от ранее введенных преобразований редукции 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. Конечность преобразований
2.3.3. Оценки слогаости .
2.3.4. Независимость
2.3.5. Локальность
2.3.6. Однозначность
2.3.7. Нерешенные вопросы редуцирования .
2.4. Классы редуцируемости сетей Петри Ю
2.4.1. Диаграмма вложения классов редуцируемости
2.4.2. Доказательство вложений .
2.5. Алгоритм и программа редукции .
Выводы к главе IIЮ
Глава Ш. Анализ сетей Петри.
у 3.1. Декомпозиция ис сетей
3.1.1. Определение понятий 1и
3.1.2. И условия.
3.1.3. Объединенный алгоритм проверки и ИЗ условий .
3.1.4. Сложность алгоритма и пути ее уменьшения .
3.2. Построение дерева достижимых маркирований и использование его для анализа сети
3.3. Требования, к алгоритмам анализа сетей Петри на
правильность
Выводы к главе Ш
Глава 1У. Применение методики к особенности программной реализации.
4.1. Применение разработанных методов к анализу некоторых систем взаимодействующих процессов
4.1.1. Проверка асинхронных интерпретаций параллельных
микропрограмм на детерминированность
4.1.2. Проверка некоторыхсвойств протоколов
4.1.3. Имитация процесса формирования и функционированияэкономических систем
4.2. Представление данных и характерные особенности
программы анализа ПГСА на корректность
Выводы к главе 1У.
Заключение
Литература


Разработка полиномиальных по сложности преобразований редукции ординарных сетей Петри и исследование вопросов;связанных с редуцируемостью,является другой важной задачей;решаемой в диссертации. Диссертация состоит из введения, четырех глав и заключения. В первой главе определяются понятия относящиеся к сетям Петри и параллельным граф-схемам алгоритмов; исследуется корректность структурированных ПГСА; обосновывается переход от граф-схемы • к ее модели г сети Петри, определяются правила такого перехода; доказывается теорема правильности сведения задачи проверки ПГСА на корректность к анализу соответствующей сети Петри на живость и безопасность. Во второй главе введены преобразования редукции ординарных сетей Петри,сохраняющие живость и безопасность сети. Определены условия применения указанных преобразований такие, как конечность, полиномиальная сложность, независимость, локальность, однозначность, массовость и полнота. Преобразования проанализированы на выполнение некоторых (наиболее важных для практики) условий. Введены классы редуцируемости ординарных сетей Петри, соотношения между этими классами систематизированы в виде диаграммы вложения. Дано краткое описание алгоритма редукции. Третья глава посвящена методам анализа различных классов сетей Петри. В алгоритме анализа выделено три этапа: редукция; декомпозиция; построение дерева достижимых маркирований. Сформулирован и исследован алгоритм анализа одного из классов (так называемых, сетей свободного выбора) сетей Петри. Рассмотрены вопросы анализа ординарных сетей с использованием дерева достижимости. Сформулированы требования к алгоритму анализа ординарных сетей Петри. В четвертой главе на примерах нескольких работ показано применение разработанной методики к анализу параллельных микропрограмм и проверке некоторых свойств протоколов. В задаче моделирования процесса функционирования экономической системы рассмотрена возможность использования ординарных сетей Петри для описания подсистем, поддерживающих исходный экономический потенциал. Кратко описаны представления данных и характерные особенности программы анализа ПГСА на корректность. В заключении перечислены результаты работы. Глава I. I.I. Сеть Петри - математическая модель, введенная А. Петри CJ в г, широко используется как в абстрактных областях теории вычислений, так и в прикладных С 3 : описание технологических процессов С 3 , параллельных программ ? J , синтез систем управления параллельными процессами С , 3 » верификация протоколов для сетей ЭВМ Cl 3 и т. Существует несколько формальных представлений сетей Петри, мы будем использовать графическое представление. I.I. I. Определение основных понятий. Г - множество переходов, X - бинарное отношение на PUT, соответствующее дугам двудольного графа с множеством вершин PUT ,i. XQ RxTUTxP. H(pi) равно значению функции маркирования в Z - ой позиции. Ориентированный граф называется сильно связным-v если для каждой пары вершин ( а. Л. и заканчивающийся в & . С множество сильно связных графов без петель и кратных дуг. Обозначим через OPN класс ординарных сетей. На чертеже позиции изображаются кружочками, а переходы черточками или квадратиками. Метки в позиции изображаются точками. М(р)-чиспо меток в позиции р, равноечислу точек. Обозначим через 'А множество входных вершин для множества вершин А , а через А* - множество выходных вершин для А . На рис. I.I изображена сеть Петри Ni - (Р, состоящая из четырех позиций и пяти переходов с вектором маркирования М0~ ( 1) О) . Ср*? Переход возбужден. Переходов имеющий входных позиций,считается возбужденным. В сети Л/у на рис. I.I. При срабатывании перехода от каждой его входной позидаи отнимается одна метка, а к каждой выходной позиции добавляется одна метка. Из множества возбужденных переходов сети может сработать любой единственнй переход, так для сети Ы1 множество возбужденных переходов есть { "a 1 ) 'кг. У сработать может либо , либо , либо "- . М , если существует последовательность срабатываний <6 ^ ‘ у приводящая из М в М . Переход ? М если существует маркирование М' , достижимое из М , при котором может сработать. Рис. Сеть . Рис. Рг Рз р4 ¦? Ч ч ¦? Рз ! Рис. Матрица смежностей сети Рис. Граф маркирований. N9.