автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.17, диссертация на тему:Бисимуляция ресурсов в сетях Петри

На правах рукописи

Башкин Владимир Анатольевич БИСИМУЛЯЦИЯ РЕСУРСОВ В СЕТЯХ ПЕТРИ

Специальность 05.13.17 - Теоретические основы информатики

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

Ярославль - 2003

Работа выполнена в Ярославском государственном университете им. П.Г. Демидова.

Научный руководитель

доктор физико-математических наук, с.н.с., Ломазова Ирина Александровна

Официальные оппоненты:

доктор физико-математических наук, профессор, Бондаренко Владимир Александрович

кандидат физико-математических наук, доцент, Захаров Владимир Анатольевич

Ведущая организация

Институт систем информатики им. А.П. Ершова СО РАН

Защита состоится « У» ^кв/^лХ 2003 г. в ^-^час. на заседании диссертационного совета К 212.002.04 при Ярославском государственном университете им. П.Г. Демидова по адресу: 150000, г. Ярославль, ул. Советская 14.

С диссертацией можно ознакомиться в научной библиотеке Ярославского государственного университета им. П.Г. Демидова.

Автореферат разослан « /?» 2003 г.

Учёный секретарь диссертационного совета

Глызин С.Д.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность проблемы. В последние десятилетия большой и устойчивый интерес проявляется к математическим средствам моделирования и анализа сложных параллельных и распределенных систем, к которым относятся, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы и алгоритмы, протоколы взаимодействия (коммуникационные, верифицирующие), модели технологических и бизнес-процессов. При разработке подобных систем, как правило, высок риск возникновения ошибки на стадии проектирования и чрезвычайно высока цена проявления ошибки на стадии эксплуатации. Все это обуславливает интерес к формальным математическим средствам анализа и верификации, позволяющим дать ответы на вопросы о свойствах модели, например, о наличии тупиков или неограниченных состояний (переполнений).

Одним из наиболее популярных формализмов для моделирования и анализа параллельных систем являются сети Петри. Понятие сети Петри было введено в 1962 году Карлом Петри. С тех пор теория сетей Петри сильно разрослась и продолжает активно развиваться. Причиной популярности сетей Петри является простота и наглядность описания параллелизма, а также удобное графическое представление модели. К тому же за время исследований было накоплено большое количество теоретических результатов и практического опыта в области спецификации и анализа параллельных и распределенных систем с помощью этого формализма.

Среди отечественных исследований по сетям Петри и спецификации и анализу распределенных систем отметим работы H.A. Анисимова, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой.

Сети Петри позволяют с достаточной степенью детализации моделировать вычислительные процессы, процессы управления в распределенных системах и протоколы взаимодействия. В них имеются простые конструкции для описания структур параллелизма: последовательная композиция, выбор, параллельное слияние. Сети Петри представляют собой модель с бесконечным числом состояний, при этом они менее выразительны, чем универсальные вычислительные системы типа машин Тьюринга, что позволяет решать для них многие за-

дачи анализа поведенческих свойств В частности, для обыкновенных сетей Петри разрешимы проблемы достижимости, останова, живости, ограниченности, покрытия.

При исследовании поведенческих свойств параллельных и распределенных систем ключевым является понятие эквивалентности поведений. Существуют различные подходы к определению поведения системы. Один из них использует понятие языка, порождаемого системой. Такой язык состоит из множества цепочек имен действий, производимых системой. Языковая семантика удобна для анализа последовательных систем, поскольку языки однозначно описывают их «

поведение. Языковая эквивалентность позволяет также сравнивать поведение параллельных систем, однако с ее помощью нельзя уловить некоторые особенности функционирования параллельных и распределенных систем, в частности, обнаруживать тупиковые состояния (дедлоки).

Для сравнения поведения параллельных систем Д. Парком и Р. Милнером в начале 80-х гг. было введено понятие бисимуляционной эквивалентности. Бисимуляционная эквивалентность стала фундаментальным понятием в теории параллельных и распределенных систем. Бисимуляция обладает четкой математической трактовкой и более тонко отслеживает ветвления в дереве срабатываний системы по сравнению с языковой эквивалентностью. Два состояния системы считаются бисимуляционно эквивалентными, если внешний наблюдатель, который видит только метки срабатываний переходов, по наблюдаемому поведению системы не может определить, с которого из этих двух состояний она начала работу.

Бисимуляционная эквивалентность изучалась для различных классов формальных систем, как с конечным, так и с бесконечным множеством состояний. В случае сетей Петри текущее состояние задается с помощью разметки — мультимножества фишек (маркеров) в позициях сети. Соответственно две разметки сети Петри называются бисимуляционно эквивалентными (бисимулярными), если выбор любой из них в качестве начальной дает одно и то же наблюдаемое поведение ^

сети.

В 1993 г. П. Жанкар доказал, что бисимуляционная эквивалентность разметок для обыкновенной помеченной сети Петри неразрешима. Бисимуляция разметок разрешима лишь для сильно ограниченных подклассов сетей Петри, например, для бисимулярно-

детерминированных сетей и для сетей с не более чем одной неограниченной позицией.

Несмотря на неразрешимость бисимуляции, поиск эквивалентных с точки зрения бисимулярности структур в сети Петри остается актуальной задачей с точки зрения приложений. В первую очередь это объясняется потребностями бисимуляционной редукции сетей Петри. Под бисимуляционной редукцией данной сети понимается сокращение ее размера при сохранении поведенческих свойств (в смысле бисимулярности). Дело в том, что большинство алгоритмов анализа сетей Петри имеют экспоненциальную сложность, поэтому любое предварительное сокращение размера модели может существенно облегчить ее дальнейший анализ.

В 1992 году Ф. Шнобелен и С. Аутон ввели понятие бисимуляции позиций. Бисимуляция позиций — это отношение эквивалентности на конечном множестве позиций сети, аддитивное замыкание которого является подмножеством бисимуляции разметок, замкнутым относительно достижимости. Бисимулярность двух позиций означает, в частности, что в любой разметке перенос фишки из первой позиции во вторую не меняет наблюдаемого поведения сети. Бисимуляция позиций обыкновенных сетей Петри разрешима, причем с полиномиальной сложностью.

Бисимуляция позиций задает "хорошо структурированное" подмножество бисимуляции разметок. В данном случае "хорошая структурированность" означает, во-первых, возможность представить любую входящую в полученное отношение пару разметок как сумму пар позиций (разметок, содержащих ровно одну фишку), и, во-вторых, замкнутость полученного отношения относительно срабатываний переходов.

В 1998 г. в работах Н.С. Сидоровой было введено и исследовано более слабое отношение на множестве позиций сети Петри — корректное слияние — отличающееся от бисимуляции позиций отсутствием требования замкнутости относительно срабатывания переходов. Такое ослабление позволяет отражать более тонкие эквивалентности на множестве разметок, однако корректное слияние позиций неразрешимо.

Общей особенностью проводившихся ранее исследований является то, что при определении подмножества бисимуляции разметок сети Петри в качестве базиса используются отношения на множестве пози-

ций сети (бисимуляция позиций и корректное слияние позиций). В первую очередь это обусловлено тем, что множество позиций сети Петри конечно, м все отношения на нем можно эффективно перечислить. Следовательно, различные свойства таких отношений (в частности, бисимуляционные) можно проверить непосредственно перебором. Однако у такого подхода есть и свои недостатки.

Отношения на множестве позиций не позволяют выразить некоторые естественные эквивалентности в сетях Петри. Например, через бисимуляцию позиций и корректное слияние позиций не выражаются следующие бисимулярности:

1. Бисимулярность любого количества фишек в тупиковой позиции (позиции, у которой нет исходящих дуг) пустому множеству фишек.

2. Бисимулярность любого ненулевого количества фишек любому ненулевому количеству фишек в позиции простого цикла (подграфа, состоящего из одной позиции и одного перехода, соединенных двумя противоположно направленными дугами).

3. Бисимулярность двух множеств фишек различной мощности.

В то же время все приведенные выше структуры могут быть выявлены эмпирически, путем анализа графовой структуры сети Петри. Данное наблюдение позволяет предположить, что бисимуляция позиций задает не всё разрешимое подмножество бисимуляции разметок. В связи с этим возникает задача нахождения более общего способа построения разрешимых подмножеств отношения бисимуляции разметок.

Разметку сети Петри можно рассматривать как мультимножество ее позиций, отмеченных фишками. Фишки в разметке сети часто содержательно трактуются как некоторые ресурсы, необходимые для выполнения того или иного действия, или, получающиеся в результате выполнения некоторого действия. Содержательно эквивалентность ресурсов в системе означает, что в любой разметке ресурс можно заменить на эквивалентный ему, и наблюдаемое поведение сети при этом не изменится. Таким образом, мультимножество позиций сети Петри можно рассматривать не только как разметку целиком, но и как некоторый ресурс, который может входить в другие разметки.

Исследование эквивалентностей на множестве ресурсов сети представляет теоретический и практический интерес, по крайней мере, с двух точек зрения:

нахождение эквивалентных ресурсов может подсказать разработчикам системы более эффективные способы ее реализации;

эквивалентности ресурсов, как и эквивалентности разметок, можно использовать для редукции сети. Цель работы состоит в точном определении и исследовании отношения эквивалентности ресурсов в сетях Петри, которое соответствовало бы содержательному понятию возможности заменить одни ресурсы на другие так, чтобы наблюдаемое поведение системы не менялось с точки зрения бисимуляционной эквивалентности. Основное внимание при этом уделяется проблеме разрешимости определяемого отношения и алгоритмам нахождения бисимуляционно эквивалентных ресурсов для заданной сети Петри.

Для достижения указанной цели решаются следующие задачи:

1. Исследование свойств и структуры отношения подобия ресурсов и других отношений эквивалентности на множестве ресурсов обыкновенной сети Петри, сохраняющих наблюдаемое поведение системы. Исследование разрешимости этих отношений и построение соответствующих алгоритмов.

2. Исследование бисимуляции ресурсов в сетях Петри с невидимыми переходами (когда срабатывание некоторых переходов не видно наблюдателю) и построение соответствующих алгоритмов.

3. Определение и исследование бисимуляции ресурсов для сетей с индивидуальными фишками - сетей Петри высокого уровня и вложенных сетей Петри.

4. Разработка алгоритмов редукции сети Петри на основе бисимуляционной эквивалентности ресурсов.

Методы исследования основываются на использовании аппарата теории сетей Петри, понятий и методов алгебраической теории параллельных процессов, теории множеств и теории отношений. Научная новизна работы.

1. Введено понятие ресурса сети Петри. Определено отношение подобия ресурсов, сохраняющее бисимулярность разметок, исследованы его свойства. В частности, доказано, что подобие ресурсов обладает конечным базисом относительно аддитивного транзитивного замыкания и в то же время неразрешимо.

2. Определено отношение условного подобия ресурсов, исследованы его свойства. Доказано, что множество пар подобных ресурсов

полулинейно, причем в качестве базиса разложения могут использоваться пары условно подобных ресурсов.

3. Определено отношение бисимуляции ресурсов, исследованы его свойства и взаимосвязь с подобием ресурсов. Показано, что бисимуляция ресурсов является сужением подобия ресурсов. Построен алгоритм проверки того, является ли данное отношение на множестве ресурсов бисимуляцией. Получен алгоритм построения для заданной обыкновенной сети Петри отношения бисимуляции на множестве ресурсов размера не больше заданного, т.е. построения отношения, аппроксимирующего максимальную бисимуляцию ресурсов.

4. Отношения подобия и бисимуляции ресурсов также определены и исследованы для следующих классов сетей Петри:

• сети Петри с невидимыми переходами;

• сети Петри высокого уровня;

• вложенные сети Петри.

Для насыщенных сетей Петри с невидимыми переходами и сетей Петри высокого уровня построены алгоритмы аппроксимации максимальной бисимуляции ресурсов, а для вложенных сетей Петри - бисимуляции ресурсов специального вида (системных ресурсов).

5. Сформулированы правила построения редуцирующих преобразований обыкновенных сетей Петри на основе подобия ресурсов.

Практическая ценность работы. Полученные результаты имеют в основном теоретический характер. Тем не менее, они могут быть использованы при решении практических задач, а именно, выявление подобных ресурсов может быть полезным для верификации и оптимизации системы, а также для редукции построенной сети. В частности, представленные методы редукции могут быть использованы в компиляторах языков параллельного программирования на стадии оптимизации кода или в системах анализа и верификации, использующих метод проверки на моделях для предварительной редукции модели.

Участие в проектах. Во время работы над диссертацией автор участвовал в следующих научных проектах:

1. Методы моделирования, анализа и верификации распределенных систем. РФФИ, грант 99-01-00309-а.

2. Разработка новых методов и средств моделирования и анализа процессов обработки информации в распределенных системах. РФФИ, фант 03-01-00804-а.

Апробация работы. Результаты диссертации докладывались на XXII Конференции молодых ученых механико-математического факультета МГУ (Москва, 2000), на Международной конференции "Concurrency Specification and Programming" (Берлин, 2002), на IV Научно-практической конференции студентов, аспирантов и молодых ученых Ярославской области (Ярославль, 2003), на Международной конференции "Parallel Computing Technologies" (Нижний Новгород, 2003), на семинаре "Моделирование и анализ информационных систем" кафедры теоретической информатики Ярославского государственного университета (2000-2003).

Публикация результатов работы. По теме диссертации опубликовано 10 научных работ.

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы из 65 наименований. Общий объем работы 145 страниц. Работа содержит 44 рисунка.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

Во введении обосновывается актуальность работы, приводится краткий обзор основных результатов и проблем в исследуемой области, формулируется цель диссертации, характеризуется ее научная новизна, дается краткий обзор работы.

Первая глава носит вводный характер. В ней кратко приводятся понятия, определения, обозначения и результаты, используемые в диссертации.

В разделе 1.1 определяются операции и отношения на множествах, мультимножествах и последовательностях.

В разделе 1.2 приводятся понятия и определения теории систем помеченных переходов и теории бисимуляционной эквивалентности.

Рассматривается понятие языка системы помеченных переходов. На примере показывается, почему языковой эквивалентности недостаточно для корректного отражения поведения системы в семантике ветвящегося времени.

Приводятся два эквивалентных определения бисимуляции — через свойство переноса и через бисимуляционные игры. Рассматриваются основные свойства бисимуляции, дается краткий обзор результатов в области разрешимости бисимуляции, полученных для различных классов формальных систем моделирования параллелизма.

В разделе 1.3 приводятся основные понятия, определения и обозначения теории сетей Петри.

Помеченной сетью Петри называется набор N = (Р, Т, F, Act, I), где Р - конечное множество позиций; Т - конечное множество переходов, РглТ=0\ F: (РхТ) и (ТхР) -> Nat - функция инцидентности; Act -конечное множество меток срабатываний; /: Т Act - помечающая функция. Графически сеть Петри изображается как двудольный ориентированный граф с кратными дугами, в котором множества Р и Т задают вершины, а функция F - дуги.

Разметкой (маркировкой) сети N называется функция М: Р -> Nat, сопоставляющая каждой позиции сети некоторое натуральное число (или ноль). При разметке М в каждую позицию р помещается М(р) маркеров (фишек). Разметка задает текущее состояние моделируемой системы.

Для перехода t е Т через't и Г обозначаются мультимножества его входных и выходных позиций: VpeP *f(p) =oef F(p, f), f(p) =det F(t, p).

Переход f e T готов к срабатыванию при разметке М, если выполняется 't с М. Готовый к срабатыванию переход t может сработать, порождая новую разметку М' =def M-'t+ f. Такое

t

срабатывание обозначается как М —>• М'.

Также в первой главе рассматривается понятие бисимуляции разметок в сетях Петри, приводится результат П. Жанкара о неразрешимости бисимуляции разметок в помеченных сетях Петри.

Вторая глава посвящена исследованию сохраняющих бисимулярность отношений на множестве ресурсов обыкновенной сети Петри.

В разделе 2.1 исследуются некоторые специальные бинарные отношения на множестве мультимножеств и способы их конечного представления.

Для элементов бинарного отношения (пар мультимножеств) их сумма определяется как при покоординатном сложении. Под аддитивным замыканием отношения далее понимается замыкание относительно такого сложения. Аддитивно-транзитивное замыкание (далее АТ-замыкание) отношения есть его замыкание относительно сложения и транзитивности. Обозначения ВА, Вт, В*1 используются для аддитивного, транзитивного и аддитивного транзитивного замыканий бинарного отношения В на множестве мультимножеств.

Вводится понятие а-базиса данного отношения (где а е {А, Т, АТ}). Отношение В' называется а -базисом отношения В, если выполняется (В)а = В". Базис В' называется минимальным а-базисом отношения В, если не существует В" с В', такого, что (Б')а = В™.

Лемма 2.2.

1. Все минимальные а-базисы отношения В либо конечны, либо бесконечны.

2. Если у отношения В существует конечный а-базис, то все минимальные а-базисы В конечны.

3. Если у отношения В существует бесконечный минимальный а-базис, то все а-базисы В бесконечны.

Теорема 2.2. Если отношение рефлексивно и симметрично, то все его минимальные АТ-базисы конечны.

Это утверждение (хотя и в несколько другой формулировке и в терминах конгруэнтностей в коммутативных полугруппах) было доказано впервые Л. Редей (1965 г.), а позднее независимо Й. Хиршфельдом (1994 г.). В диссертации приводится новое доказательство, которое представляется более удачным, поскольку конструктивно описывает структуру элементов конечного базиса.

В диссертации приводятся примеры отношений на мультимножествах, показывающие, что все условия теоремы являются необходимыми, а именно:

1. Отношение эквивалентности с бесконечными минимальными А-базисами и с бесконечными минимальными Т-базисами.

2. Симметричное отношение с бесконечными минимальными АТ-базисами.

3. Рефлексивное отношение с бесконечными минимальными АТ-базисами.

Несмотря на конечность всех минимальных АТ-базисов, число таких базисов для данного отношения может быть бесконечно. Приводится пример отношения с бесконечным числом минимальных базисов.

Далее в диссертации рассматривается конечный базис специального вида, названный основным базисом отношения. Основной базис строится как множество элементов отношения 6АТ минимальных относительно специально определяемого для этого частичного порядка.

Доказано, что любое симметричное бинарное отношение имеет ровно один основной базис. Исследованы свойства основного базиса.

Приводится полиномиальный алгоритм 2.1, который по произвольной паре мупьтимножеств проверяет, принадлежит ли эта пара АТ-замыканию данного основного базиса. Приводится также полиномиальный алгоритм 2.2, позволяющий преобразовать произвольный конечный АТ-базис данного отношения в основной базис.

В разделе 2.2 вводятся и исследуются понятия ресурса и подобия ресурсов обыкновенной сети Петри.

Ресурс сети Петри определяется как мультимножество над множеством позиций сети Петри.

Формально определение ресурса не отличается от определения разметки сети Петри. Каждая разметка является ресурсом и каждый ресурс является разметкой. Мы различаем эти понятия из-за их различной интерпретации. Ресурсы являются частями разметок (в некотором смысле неделимыми), обеспечивающими то или иное поведение сети при любом её состоянии. Мы могли бы использовать термин "подмножество разметки", но предпочитаем "ресурс", поскольку рассматриваем ресурс не как "подмножество данной разметки", а как "общую часть всех разметок, содержащих данное мультимножество фишек". Например, ресурсом является мультимножество фишек, достаточное для срабатывания некоторого перехода.

Вводится понятие подобных ресурсов. Два ресурса подобны, если в любой разметке мы можем заменить один из них на другой, и при этом дальнейшее наблюдаемое поведение сети не изменится (в смысле бисимуляционной эквивалентности поведений).

Примером подобных ресурсов в реальной жизни могут служить, два набора монет — одна монета по десять копеек и две монеты по пять копеек, при условии кратности цен на интересующие нас товары десяти копейкам. В данном случае различный номинал монет соответствует различным позициям сети Петри, количество монет — разметке соответствующей позиции, покупка товара — срабатыванию перехода, а цена на товар — кратности исходящих из позиций дуг.

В диссертации исследуются свойства подобия ресурсов — отношения на множестве ресурсов сети Петри, состоящего из всех пар подобных ресурсов.

Утверждение 2.4. Подобие ресурсов является сужением максимальной бисимуляции разметок.

Лемма 2.5. Подобие ресурсов является отношением эквивалентности, замкнутым относительно сложения.

Теорема 2.3. Подобие ресурсов обладает конечным АТ-базисом.

Доказывается, что корректное слияние позиций является сужением подобия ресурсов, состоящим из пар ресурсов единичной мощности. Тогда из неразрешимости корректного слияния позиций получаем:

Следствие 2.1. Проблема распознавания подобия ресурсов неразрешима.

Поскольку интерес представляют разрешимые отношения, далее в диссертации рассматривается более сильное отношение.

В разделе 2.3 вводится и исследуется понятие условного подобия ресурсов.

Ресурсы г и я подобны при условии Ь, если в любой разметке, содержащей ресурс г + Ь, мы можем заменить г на в, и при этом дальнейшее наблюдаемое поведение сети не изменится (в смысле бисимулярной эквивалентности поведений). Ресурсы условно подобны, если они подобны при некотором условии.

Доказывается ряд свойств условного подобия ресурсов, в частности, его замкнутость относительно сложения, вычитания и объединения условий. Устанавливается взаимосвязь подобия ресурсов и условного подобия ресурсов, также доказывается неразрешимость проблемы распознавания условного подобия ресурсов.

Устанавливается свойство подобия ресурсов:

Теорема 2.5. Множество пар подобных ресурсов полулинейно, причем в качестве базиса разложения можно использовать пары условно подобных ресурсов.

В разделе 2.4 вводится и исследуется понятие бисимуляции ресурсов обыкновенной сети Петри, предлагаемое в качестве приближения подобия ресурсов.

Симметричное рефлексивное отношение В на множестве ресурсов называется бисимуляцией ресурсов, если его АТ-замыкание является бисимуляцией разметок.

Теорема 2.6. Любая бисимуляция ресурсов является сужением подобия ресурсов.

Обратное в общем случае неверно — не всякое подмножество подобия ресурсов есть бисимуляция ресурсов. Отношение бисимуляции ресурсов замкнуто относительно срабатывания переходов. Для отношения подобия ресурсов это условие может и не выполняться.

Поскольку любая бисимуляция ресурсов симметрична и рефлексивна, она обладает конечным АТ-базисом.

Доказываются следующие свойства бисимуляций ресурсов: Теорема 2.7.

1. Объединение двух бисимуляций ресурсов является бисимуляцией ресурсов.

2. Для любой помеченной сети Петри N существует наибольшая по вложению бисимуляция ресурсов (обозначается 8(Л/)), которая является отношением эквивалентности.

На рис.1 показаны взаимные включения рассматриваемых в работе отношений эквивалентности на множестве ресурсов/разметок сети.

Рис 1 Отношения эквивалентности на пегл/псях г.рти

Здесь (~) - максимальная бисимуляция разметок, (я) - подобие ресурсов, В(Л/) - максимальная бисимуляция ресурсов; сплошной линией обозначены отношения, обладающие конечным АТ-базисом.

Для проверки того, является ли данное отношение подобием ресурсов, требуется в общем случае бесконечное число проверок пар ресурсов. В случае бисимуляции ресурсов достаточно проверить только конечное число пар ресурсов. Это обусловлено выполнением для каждой бисимуляции ресурсов так называемого слабого свойства переноса.

Отношение В на множестве ресурсов сети Петри обладает слабым свойством переноса, если для любой принадлежащей В пары ресурсов (г, 5) е В и для любого перехода такого, что 7 п л* 0, найдется переход и, обладающий следующими свойствами:

1. Переходы tw и помечены одной и той же меткой срабатывания.

/

2. Обозначим М( = 7иг и Мг^Ч- г+ б. Выполняется М, -»М/ и

и

Мг ->М2\ причем (Ми М2) е ВТ. Слабое свойство переноса — это более слабый (локальный) вариант полного свойства переноса (используемого при определении бисимуляции разметок). Рассматриваются не все разметки сети, а только

разметки, входящие в конечное множество минимальных покрытий данного перехода.

Теорема 2.8. Симметричное рефлексивное отношение на множестве ресурсов сети Петри обладает слабым свойством переноса тогда и только тогда, когда оно является бисимуляцией ресурсов данной сети.

В пункте 2.4.3 приводится имеющий полиномиальную сложность алгоритм 2.3 проверки того, является ли данное конечное отношение В бисимуляцией ресурсов. Алгоритм состоит из двух этапов. На первом при помощи алгоритма 2.2 строится основной базис отношения В. На втором этапе производится проверка выполнения слабого свойства переноса для всех пар ресурсов. При этом для проверки принадлежности пар разметок отношению В*1 используется алгоритм 2.1.

В пункте 2.4.4 исследуются возможности построения максимальной бисимуляции ресурсов 6(Л/). Приводится имеющий экспоненциальную сложность алгоритм 2.4 построения отношения В(Л/, (¡г) — максимальной бисимуляции ресурсов над множеством ресурсов, мощность которых не превышает данного натурального числа д.

Отношение В{Ы, д) можно рассматривать как аппроксимацию отношения В(Л/)- Действительно, любой элемент отношения В(ЛУ) принадлежит В(Л/, д) при некотором q. Более того, поскольку В(Л/) имеет конечный базис, то для любой помеченной сети N существует число 7о(Л/). Для которого выполняется В(Л/, до(Л/)) = В(Л/). Однако возможность эффективного вычисления до(Л/) или верхней оценки для него остается открытой проблемой.

В разделе 2.5 рассматриваются некоторые методы и правила редуцирующих преобразований обыкновенных помеченных сетей Петри, сохраняющих бисимуляционную эквивалентность сетей.

Предлагаются три различных вида редукции:

• Замена в начальной разметке сети большего по мощности ресурса на меньший подобный.

• Замена "подобных" выходных дуг переходов. Если срабатывание некоторого перехода f помещает в его выходные позиции некоторый ресурс г, у которого имеется подобный ресурс з, то мы можем заменить у перехода t все выходные дуги, соответствующие мультимножеству позиций г, на дуги, соответствующие мультимножеству я, и при этом поведение сети не изменится (в смысле бисимупярности). Если мощность ресурса г больше мощности ресурса 5, то получаемая сеть

меньше исходной. Редукция корректна для сети с любой начальной разметкой. Пример замены "подобных" дуг

приведен на рис. 2.

«= . - 0

Р1

Рг

Рг

Рис. 2. Редукция заменой выходных дуг. В сети N подобны ресурсы р? и 0, 2рг и рг- Сеть Л/' получена заменой соответствующих дуг.

• Полная замена подобных ресурсов. Пусть заменяемый ресурс "неделим" с точки зрения начальной разметки сети и с точки зрения всех переходов. Другими словами, ресурс входит в начальную разметку "целое" число раз и всякий переход при срабатывании забирает из входных позиций и помещает в выходные позиции "целое" число таких ресурсов. Это условие достаточно сильное, однако оно позволяет производить полную замену одного ресурса в сети на другой (подобный). Ресурс заменяется как в начальной разметке, так и в графовой структуре сети Петри — заменой соответствующих дуг. Пример редукции путем замены подобных ресурсов приведен на рис. 3.

Л/:

Р>

Рг

Л/':

Р1 Рг

Рз

Рз

Рис. 3. Редукция заменой подобных ресурсов. В сети N подобны ресурсы 2р, и рг- Сеть № получена заменой ресурса 2р1 на ресурс рг.

При такой редукции также возникают избыточные позиции и переходы, которые могут быть удалены из сети. В работе

!

1

I

' приводится один критерий избыточности позиции,

определяемый подобием ресурсов данной сети и ее начальной разметкой.

Описанные преобразования могут применяться по отдельности и комплексно. Получаемые редукции корректны с точки зрения бисимуляционной эквивалентности, что гарантирует сохранение поведенческих свойств сети, таких, как живость, ограниченность и др.

В третьей главе исследуются понятия ресурса, подобия и бисимуляции ресурсов применительно к классу сетей Петри с невидимыми переходами.

Класс сетей Петри с невидимыми переходами представляет собой ^ расширение класса обыкновенных сетей Петри за счет введения понятия

скрытого внутрисистемного срабатывания (обозначаемого символом т).

Известно, что сети Петри с невидимыми переходами строго мощнее I по выразительности обыкновенных сетей Петри. Этот факт проявляется

и при рассмотрении отношений на множестве ресурсов. Определенные

I

по аналогии со случаем обыкновенных сетей г-подобие и г-бисимуляция I ресурсов обладают не всеми описанными выше свойствами подобия и

I бисимуляции ресурсов. Доказывается, что выполнения слабого свойства

г-переноса недостаточно для того, чтобы отношение являлось г-бисимуляцией ресурсов.

В случае сетей с невидимыми переходами требуется ещё большее 1 усиление отношений и ограничение класса сетей.

В диссертации рассматривается класс р-насыщенных сетей с невидимыми переходами, в которых срабатывание любой последовательности переходов с не более чем одной видимой меткой

* может быть имитировано одновременным (независимым) ' срабатыванием некоторого множества переходов с той же меткой (так

называемого "параллельного шага"). Известно, что в р-насыщенных сетях Петри г-бисимуляция разметок совпадает с более сильной гр-бисимуляцией разметок, при которой переход должен имитироваться не

• последовательностью срабатываний переходов, а параллельным шагом.

Доказывается один критерий р-насыщаемости для сетей Петри с невидимыми переходами. Вводятся понятия гр-подобия ресурсов и ф-бисимуляции ресурсов. Доказывается, что в насыщенной сети ф-подобие ресурсов совпадает с г-подобием ресурсов (то же и для бисимуляций). Доказывается, что ф-бисимуляция ресурсов может быть эффективно проверена при помощи слабого свойства гр-переноса.

Приводится алгоритм построения аппроксимации максимальной ,7.-бисимуляции ресурсов для насыщенной сети Петри с невидимыми переходами.

В четвертой главе исследуются понятия ресурса, подобия и бисимуляции ресурсов в применении к классу сетей Петри высокого уровня на примере раскрашенных сетей, введенных К. Йенсеном в 1981 г.

В отличие от обыкновенных сетей Петри, синтаксис сетей Петри высокого уровня обладает конструкциями модульности и иерархичности. Это делает их более удобными в практическом применении. В настоящее время большинство программных средств моделирования и анализа параллельных и распределенных систем используют в качестве базовой модели именно сети высокого уровня (чаще всего раскрашенные сети Йенсена).

Известно, что сети Петри высокого уровня имеют ту же выразительную мощность, что и обыкновенные сети Петри, то есть могут быть преобразованы в обыкновенные и проанализированы при помощи методов и алгоритмов теории обыкновенных сетей Петри Однако такой подход не всегда удобен, поскольку обратное преобразование обыкновенной сети в сеть высокого уровня (после проведения редукции) не всегда возможно и редко приводит к удобным и наглядным моделям. В связи с этим интерес представляют методы анализа, оперирующие непосредственно сетями высокого уровня и не "спускающиеся" до уровня обыкновенных сетей.

В диссертации предлагаются такие высокоуровневые методы для построения и анализа подобия ресурсов и бисимуляции ресурсов.

Ресурс в сети высокого уровня представляет собой не мультимножество, а вектор заданной длины, элементами которого являются мультимножества. Это обусловлено тем, что разметкой позиции сети высокого уровня является не натуральное число, а мультимножество индивидуальных фишек. Необходим другой по сравнению с обыкновенными сетями способ задания ресурса.

Поэтому для сетей Петри высокого уровня в диссертации вводится понятие элементарного ресурса — пары вида (позиция, индивидуальная фишка).

Разметка и ресурс раскрашенной сети Петри могут рассматриваться как мультимножества над множеством элементарных ресурсов. Это позволяет перенести определения подобия и бисимуляции ресурсов на

случай раскрашенных сетей.

В работе исследуются свойства определенных таким образом отношений на множестве ресурсов раскрашенной сети Петри. Доказывается, что отношения подобия и бисимуляции ресурсов сети Петри высокого уровня обладают всеми теми же свойствами, что и соответствующие отношения на множестве ресурсов обыкновенной сети Петри.

Приводится алгоритм построения аппроксимации максимальной бисимуляции ресурсов раскрашенной сети Петри.

В пятой главе исследуются понятия ресурса, подобия и бисимуляции ресурсов в применении к классу вложенных сетей Петри, введенному в работах И.А. Ломазовой.

Во вложенных сетях Петри в качестве фишек выступают обычные сети Петри (элементные фишки), которые могут функционировать как автономно, так и во взаимодействии между собой (горизонтальная синхронизация) и с системной сетью (вертикальная синхронизация). Это позволяет моделировать с помощью вложенных сетей Петри сложные иерархические и мультиагентные системы, имеющие динамическую структуру.

В данной главе рассматриваются двухуровневые вложенные сети Петри. В двухуровневых вложенных сетях наряду с «глобальными» состояниями сети, сопоставляющими каждой позиции системной сети мультимножество размеченных сетевых фишек, можно рассматривать также два вида локальных состояний:

1. Локальные состояния элементных сетей - сетевых фишек.

2. Состояния системной сети без учета состояний сетевых фишек.

Показывается, что каждый из этих трех видов состояний порождает

свой вариант определения ресурса и подобия ресурсов.

Во-первых, можно рассматривать сетевую фишку как обыкновенную сеть Петри и находить в ней подобные ресурсы. Доказывается, что такие ресурсы подобны и с точки зрения вложенной сети в целом.

Во-вторых, можно рассматривать всю вложенную сеть и ее «глобальные» состояния. В этом случае можно, аналогично случаю сетей Петри высокого уровня, строить аппроксимацию максимальной бисимуляции ресурсов. Однако число параметров, ограничивающих размер ресурсов, в случае вложенных сетей Петри увеличивается: ограничивается не только общее количество фишек в разметке системной сети, но и количество фишек в оазметках всех сетевых

фишек. Существенно возрастает в этом случае и трудоемкость алгоритма.

И, наконец, третий случай, когда разметки системной сети рассматриваются без учета внутренних состояний сетевых фишек. В диссертации доказывается, что в общем случае нельзя абстрагироваться от структуры фишек и рассматривать системную сеть как обыкновенную или даже как раскрашенную сеть Петри без потери существенной информации об ее поведении. Таким образом, при анализе ресурсов сети необходимо различать обычные и сетевые фишки.

В то же время, в некоторых случаях можно все же абстрагироваться от состояния сетевых фишек, что существенно уменьшает сложность поиска подобных ресурсов. С этой целью в работе вводится понятие подобия системно-автономных ресурсов.

Подобные системно-автономные ресурсы — это мультимножества позиций системной сети, которые, во-первых, подобны как ресурсы при рассмотрении системной сети как обыкновенной сети Петри, и, во-вторых, неразличимы с точки зрения находящихся в них сетевых фишек. При этом сетевые фишки различают позиции системной сети только по тем ограничениям, которые накладывает на их поведение вертикальная синхронизация.

Отношение подобия системно-автономных ресурсов может использоваться только для систем без горизонтальной синхронизации. В работе доказано, что при наличии во вложенной сети хотя бы одной пары горизонтально синхронизированных переходов максимальное по вложению подобие системно-автономных ресурсов является тождественным отношением.

В разделе 5.5 рассматривается обобщение вложенных сетей — так называемые рекурсивные вложенные сети Петри, в которых в качестве фишек могут выступать не только обыкновенные, но и вложенные сети. Такими сетями удобно моделировать системы, имеющие динамическую рекурсивную структуру.

Доказывается, что класс контекстно-свободных языков строго вкладывается в класс тупиковых языков вложенных рекурсивных сетей, то есть рекурсивные сети обладают большей выразительной мощностью, чем обыкновенные сети Петри. Из этого следует, в частности, что отношения подобия и бисимуляции ресурсов в случае рекурсивных сетей не могут быть построены с той же степенью эффективности.

В заключении формулируются основные результаты и перечисляются возможные направления дальнейшей работы.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ И ВЫВОДЫ

1. Введено понятие ресурса сети Петри. Определено и исследовано отношение подобия ресурсов. Показано, что оно соответствует содержательному понятию возможности заменить одни ресурсы на другие так, чтобы наблюдаемое поведение системы не менялось с точки зрения бисимуляционной эквивалентности. Обнаружены следующие свойства подобия ресурсов:

• подобие ресурсов является сужением максимальной бисимуляции разметок;

• подобие ресурсов обладает конечным базисом относительно аддитивного транзитивного замыкания;

• подобие ресурсов неразрешимо;

• множество пар подобных ресурсов полулинейно, причем в качестве базиса разложения можно использовать лары условно подобных ресурсов.

2. Определено отношение бисимуляции ресурсов. Исследованы его свойства и взаимосвязь с подобием ресурсов Показано, что бисимуляция ресурсов является сужением подобия ресурсов. Предложен алгоритм проверки того, является ли данное отношение бисимуляцией ресурсов. Предложен алгоритм построения аппроксимации максимальной (по вложению) бисимуляции ресурсов для данной сети Петри.

3. Определены и исследованы понятия ресурса, подобия и бисимуляции ресурсов для трех классов формальных систем, основанных на обыкновенных сетях Петри:

• сетей Петри с невидимыми переходами;

• сетей Петри высокого уровня;

• вложенных сетей Петри.

4. Разработаны методы редукции обыкновенных сетей Петри на основе бисимуляции ресурсов, не изменяющие поведение сети в смысле бисимуляционной эквивалентности.

^

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Башкин В.А. Методы насыщения сетей Петри с невидимыми переходами // Моделирование и анализ информационных систем. — Ярославль: ЯрГУ. 1999. Вып.6. — С.16-20.

2 Башкин В.А., Ломазова И.А. О языках вложенных рекурсивных сетей Петри // Интеллектуальное управление: новые интеллектуальные технологии в задачах управления (ICIT'99). Труды международной конференции, Переспавль-Залесский, 69 декабря 1999. — М.:Наука. Физматлит, 1999. — С.9-13.

3. Башкин В.А. Бисимуляция ресурсов в сетях Петри с невидимыми переходами // Современные проблемы математики и информатики: Сборник научных трудов молодых ученых, аспирантов и студентов. — Ярославль: ЯрГУ. 2002. Вып.5. — С.79-85.

4. Башкин В.А. Конечное представление отношений на мультимножествах // Моделирование и анализ информационных систем. — Ярославль: ЯрГУ. 2003. Вып.10. — С.56-59.

5. Башкин В.А. Бисимуляция ресурсов в сетях Петри // Тез. докладов на IV ежегодной научно-практической конференции студентов, аспирантов и молодых ученых Ярославской области. — Ярославль, 2003. — С.15.

6. Башкин В.А., Ломазова И.А. Бисимуляция ресурсов в сетях Петри // Известия РАН: Теория и системы управления. — 2003. №4, —С. 115-123.

7. Bashkin V.A., Lomazova I.A. Reduction of Coloured Petri nets based on resource bisimulation // Joint Bulletin of NCC & IIS, Сотр. Science. — Novosibirsk. 2000. V.13. — P.12-17.

8. Bashkin V.A., Lomazova I.A. Resource bisimulations in Nested Petri Nets // Proc. of CS&P'2002. — Berlin: Humboldt-Universitat zu Berlin. 2002. Vol.1. Informatik-Bericht №161. — P.39-52.

9. Bashkin V.A., Lomazova I.A. Petri Nets and resource bisimulation // Fundamenta Informaticae. — 2003. Vol.55. №2. — P.101-114.

10. Bashkin V.A., Lomazova I.A. Resource similarities in Petri net models of distributed systems // Proc. of PaCT2003. — Lecture Notes in Computer Science. 2003. Vol.2763. — P.35-48.

2о оЗМ

Р 17 3 0 6

Введение

1. Сети Петри и бисимуляция разметок

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

1.2. Системы помеченных переходов, бисимулящщ.

1.3. Сети Петри.

2. Бисимуляция ресурсов в обыкновенных сетях Петри

2.1. Конечное представление отношений.

2.1.1. Базисы отношений.

2.1.2. Конечность базиса ЛТ-замыкания.

2.1.3. Свойства основного базиса.

2.2. Подобие ресурсов.

2.2.1. Определение подобия.

2.2.2. Свойства.

2.2.3. Неразрешимость.

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

2.3.1. Определение условного подобия.

2.3.2. Свойства.

2.3.3. Полулинсйность множества пар подобных ресурсов

2.4. Бисимуляция ресурсов

2.4.1. Определение бисимуляции.

2.4.2. Слабое свойства переноса

2.4.3. Проверка бисимулярности отношения

2.4.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. Алгоритм построения аппроксимации

5. Бисимуляция ресурсов во вложенных сетях Петри

5.1. Вложенные сети Петри.

5.2. Объектные ресурсы.

5.3. Системные ресурсы.

5.4. Системно-автономные ресурсы

5.5. Рекурсивные вложенные сети Петри.

В настоящее время большой и устойчивый интерес проявляется к средствам моделирования и анализа сложных параллельных и распределенных систем. Такими системами являются, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы и алгоритмы, протоколы взаимодействия (коммуникационные, верифицирующие), модели технологических и бизнес-процессов. Это обусловлено в первую очередь высоким риском возникновения ошибок на стадии проектирования таких систем и чрезвычайно высокой ценой проявления этих ошибок на стадии эксплуатации.

При исследовании сложной системы нас могут интересовать различные ее свойства, например, наличие тупикового состояния, возможность переполнения буфера и т.п. Математические методы во многих случаях позволяют получить однозначный ответ на подобные вопросы. При этом важное значение имеет первоначальный выбор используемого формализма, то есть способа моделирования реальной системы.

Для решения задач анализа и верификации в теории параллельных и распределенных вычислений в настоящее время предлагаются различные способы моделирования реальных систем [1, 2]. К числу наиболее известных формализмов можно отнести конечные автоматы, алгебры процессов, CCS Р.Милнера, языки трасс, а также различные их модификации, в том числе с добавлением конструкций времени и вероятности.

Различные классы моделей обладают различными свойствами выразительности и алгоритмической разрешимости. Причем эти два параметра модели, как правило, противоречат друг другу: выбранный формализм может оказаться или очень выразительным и не поддающимся анализу, или же позволяющим эффективно решать все необходимые проблемы, но при этом слишком слабым, недостаточно полно описывающим моделируемую систему.

Сети Петри — достаточно выразительная модель параллелизма, обладающая в то же время значительным набором разрешимых свойств. В частности, для обыкновенных сетей Петри разрешимы проблемы достижимости, останова, живости, ограниченности, покрытия (см. обзоры [30, 31, 53, 55]).

Основы теории сетей Петри были заложены в 60-х годах XX века немецким ученым Карлом Петри [51]. С тех пор теория сильно разрослась и до сих пор продолжает активно развиваться. Причиной популярности сетей Петри является простота и наглядность описания параллелизма, а также удобное графическое представление модели. К тому же за время исследований сетей Петри было накоплено большое количество теоретических результатов и практического опыта в области спецификации и анализа параллельных и распределенных систем. Существуют достаточно обширные электронные архивы научной информации по сетям Петри (см. [62, 63, 64, 65]).

Среди отечественных исследований по сетям Петри и спецификации и анализу распределенных систем отметим работы Н.А. Анисимо-ва, O.JI. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, P.JI. Смелянского, В.А. Соколова, JI.A. Черкасовой.

В основе формализма сетей Петри лежит идея моделирования создания, уничтожения и перемещения внутренних ресурсов системы, представленных в виде маркеров (фишек). Фишки располагаются во внутренних ячейках сети Петри — так называемых позициях, откуда их забирают в момент срабатывания переходы, моделирующие действия системы. Переход может сработать только при наличии необходимого числа фишек в своих входных позициях, он же в момент срабатывания помещает в свои выходные позиции соответствующий набор фишек.

Подобная система при всей своей простоте оказывается весьма выразительной. Сети Петри позволяют с достаточной степенью детализации моделировать вычислительные процессы, процессы управления в параллельных системах и протоколы взаимодействия. В них имеются простые конструкции для описания структур параллелизма: последовательная композиция, выбор, параллельное слияние.

Существует большое число классов формальных моделей, построенных на основе сетей Петри. Некоторые являются расширением класса обыкновенных сетей Петри и по выразительности приближаются к машинам Тьюринга, некоторые — сужением (иногда до конечных систем). Существуют сети Петри с ингибиторными дугами, с невидимыми переходами, сети со временем и вероятностью, объектно-ориентированные сети Петри [32, 55]. В работах В.Е. Котова и Л.А. Черкасовой [9] были определены формализмы регулярных и иерархических сетей Петри, обладающие удобным алгебраическим представлением.

За последние два десятилетия образовался довольно обширный набор классов формальных систем с общим названием "сети Петри высокого уровня", в которых тем или иным способом вводятся конструкции модульности и иерархичности [32, 33, 44, 57, 58]. Среди всех формализмов сетей Петри высокого уровня следует выделить раскрашенные сети К. Йенсена (Coloured Petri Nets, CPN) [43, 44], получившие наибольшее распространение в практических приложениях. В частности, на их основе создана популярная система моделирования и верификации De-sign/CPN [45].

Большое внимание уделяется разработке формализмов для представления при помощи сетей Петри мультиагентных систем со сложной динамической структурой (вплоть до рекурсивности). К формализмам такого рода можно отнести объектные сети Р. Фалька [61], схемы рекурсивно-параллельных программ О.Б. Кушнаренко и В.А. Соколова [18], рекурсивные сети С. Хаддада и Д. Пватрено [34]. В работах И.A. Jlo-мазовой [10, 12] были определены вложенные сети Петри и рекурсивные вложенные сети Петри. В таких сетях некоторые фишки в свою очередь могут быть сетями Петри, что позволяет естественным образом моделировать динамические объекты в системе.

Понятие эквивалентности поведений — важнейшее понятие теории формальных систем. Поведенческие эквивалентности позволяют сравнивать параллельные и распределенные системы с учетом тех или иных аспектов их функционирования, а также абстрагироваться от излишней информации. Эквивалентностиые отношения используются также для сохраняющей поведение редукции систем и в процессе верификации, когда сравнивается ожидаемое и реальное поведения систем. Эквивалентные преобразования занимают важное место в теории автоматов, теории схем программ (см., например работу Р.И. Подловченко [15]).

Для параллельных программ и систем в литературе определен ряд видов поведенческих эквивалентности. Одна из них — языковая эквивалентность [14, 38], то есть эквивалентность порождаемых системами языков. Она широко используется при анализе последовательных систем, поскольку языки однозначно описывают поведение таких систем. Языковая эквивалентность позволяет также сравнивать и поведение параллельных систем, однако с ее помощью нельзя уловить некоторые особенности их функционирования, в частности, обнаруживать тупиковые состояния (дедлоки).

Для сравнения поведения параллельных систем Д. Парком и Р. Мил-нером [50, 48] в начале 80-х гг. было введено понятие бисимуляцион-ной эквивалентности. Бисимуляционная эквивалентность стала фундаментальным понятием в теории параллельных и распределенных систем.

Бисимуляция обладает четкой математической трактовкой и более тонко отслеживает ветвления в дереве срабатываний системы по сравнению с языковой эквивалентностью. Два состояния системы бисимулярны, если внешний наблюдатель, который видит только метки срабатываний переходов, по наблюдаемому поведению системы не может определить, с какого из этих двух состояний она начала работу.

Кроме обычной бисимуляции, широко используется также слабая бисимуляция, при которой внешний наблюдатель не видит срабатываний некоторых переходов (они считаются внутрисистемными).

Бисимуляционная эквивалентность изучалась для различных классов формальных моделей. Был получен ряд результатов по ее разрешимости. В частности, бисимуляция разрешима для всех классов моделей с конечным множеством состояний и для таких классов моделей с бесконечным множеством состояний, как:

- базовые параллельные процессы (ВРР, Basic Parallel Processes) [28, 29, 36],

- базовые алгебры процессов (ВРА, Basic Process Algebra) [22, 27],

- нормированные алгебры процессов (normed PA, normed Process Algebra) [37],

- автоматы с одним счетчиком (one-counter machines) [40],

- нормированные магазинные автоматы (normed PDA, normed Pushdown Automata) [59].

Также известен ряд негативных результатов. Бисимуляция неразрешима для следующих классов моделей (упорядочены по возрастанию выразительной мощности и в обратном хронологическом порядке по времени доказательства неразрешимости бисимуляции):

- автоматы мультимножеств (MSA, Multiset Automata) [49],

- помеченные сети Петри (labelled PN, labelled Petri Nets) [39],

- универсальные модели (машины Минского, машины Тьюринга, сети Петри с ингибиторными дугами).

Класс MS А является подклассом помеченных сетей Петри и совпадает с классом параллельных магазинных автоматов (PPDA, Parallel Pushdown Automata). Неразрешимость бисимуляции для MS А была доказана

Ф. Моллером [49] с использованием техники, предложенной П. Жанка-ром в [39]. Этот способ доказательства состоит в "слабом" моделировании сетью Петри машины Минского и сведении проблемы бисимуляр-ности состояний сети к проблеме останова машины Минского (которая является неразрешимой). Открытие этого метода позволило получить множество результатов по разрешимости бисимуляции для различных классов формальных моделей (см. обзоры [49] и [42]).

В случае сетей Петри текущее состояние задается с помощью разметки — мультимножества фишек (маркеров) в позициях сети. Соответственно две разметки сети Петри называются бисимуляционно эквивалентными (в смысле обычной бисимуляции), если выбор любой из них в качестве начальной дает одно и то же наблюдаемое поведение сети.

Кроме обычной бисимуляции разметок, существует достаточно широкий набор других классов бисимуляционных эквивалентностей для сетей Петри. В данной области следует отметить работы И.В. Тарасюка [19, 60], в которых рассматриваются сети Петри (в том числе временные сети и сети с невидимыми переходами) и алгебры процессов и сравниваются различные виды бисимуляционных эквивалентностей для них.

Бисимуляция разметок (состояний) разрешима лишь для достаточно ограниченных подклассов сетей Петри (например, для сетей с пометками "один-к-одному" и для бисимулярно-детерминированных сетей [39]). Тем не менее, изучение поведения сети в смысле бисимулярности является актуальной задачей. В частности, это объясняется потребностями бисимуляционной редукции сетей Петри. Под бисимуляционной редукцией данной сети понимается сокращение ее размера при сохранении поведенческих свойств (в смысле бисимулярности). Дело в том, что большинство алгоритмов анализа сетей Петри имеют экспоненциальную сложность, поэтому любое предварительное сокращение размера модели может существенно облегчить ее дальнейший анализ.

Посколько бисимуляция разметок неразрешима, важное значение приобретает задача построения более сильных эквивалентностей на множестве состояний сети Петри, сохраняющих бисимулярность и в то же время поддающихся анализу (эффективно вычислимых).

Ф. Шнобелеи и С. Аутон [20, 21] определили и исследовали понятие бисимуляции позиций. Бисимуляция позиций — это отношение эквивалентности на конечном множестве позиций сети Петри, аддитивное замыкание которого является подмножеством бисимуляции разметок, замкнутым относительно достижимости. Бисимулярность двух позиций означает, в частности, что в любой разметке перенос фишки из первой позиции во вторую не меняет наблюдаемого поведения сети. В отличие от бисимуляции разметок, бисимуляция позиций разрешима.

Бисимуляция позиций задает "хорошо структурированное" подмножество бисимуляции разметок. В данном случае "хорошая структурированность" означает, во-первых, возможность представить любую входящую в полученное отношение пару разметок как сумму пар позиций (разметок, содержащих ровно одну фишку), и, во-вторых, замкнутость полученного отношения относительно срабатываний переходов.

В работах Н.С. Сидоровой [16, 17, 56] было введено и исследовано более слабое отношение на множестве позиций сети Петри — корректное слияние — отличающееся от бисимуляции позиций отсутствием требования замкнутости относительно срабатывания переходов. Такое расширение бисимуляции позиций позволяет отражать более тонкие эквивалентности на множестве разметок, однако приводит к неразрешимости отношения.

Общей особенностью всех проводившихся ранее исследований является то, что при определении подмножества бисимуляции разметок сети Петри в качестве базиса используются отношения на множестве позиций сети (бисимуляция позиций и корректное слияние позиций). В первую очередь это обусловлено тем, что множество позиций сети Петри конечно, и все отношения на нем можно эффективно перечислить. Следовательно, различные свойства таких отношений (в частности, биси-муляционные) можно проверить непосредственно перебором. Однако у такого подхода есть и свои недостатки.

Отношения на множестве позиций не позволяют выразить некоторые естественные эквивалентности в сетях Петри. Например, через бисиму-ляцию позиций и корректное слияние позиций не выражаются следующие бисимулярности:

1) Бисимулярность любого количества фишек в тупиковой позиции сети (позиции, у которой нет исходящих дуг) пустому множеству фишек.

2) Бисимулярность любого ненулевого количества фишек любому ненулевому количеству фишек в позиции простого цикла (подграфа, состоящего из одной позиции и одного перехода, соединенных двумя противоположно направленными дугами).

3) Бисимулярность двух множеств фишек различной мощности.

В то же время все приведенные выше структуры могут быть выявлены эмпирически, путем анализа графовой структуры сети Петри.

Данное наблюдение позволяет предположить, что бисимуляция позиций задает не всё разрешимое подмножество бисимуляции разметок. В связи с этим возникает задача нахождения более общего способа построения разрешимых подмножеств отношения бисимуляции разметок.

Разметку сети Петри можно рассматривать как мультимножество ее позиций, отмеченных фишками. Фишки в разметке сети часто содержательно трактуются как некоторые ресурсы, необходимые для выполнения того или иного действия, или же получающиеся в результате выполнения некоторого действия. Содержательно эквивалентность ресурсов в системе означает, что в любой разметке ресурс можно заменить на эквивалентный ему, и наблюдаемое поведение сети при этом не изменится. Таким образом, мультимножество позиций сети Петри можно рассматривать не только как разметку целиком, но и как некоторый ресурс, который может входить в другие разметки.

Исследование эквивалентностей на множестве ресурсов сети представляет теоретический и практический интерес, по крайней мере, с двух точек зрения:

- нахождение эквивалентных ресурсов может подсказать разработчикам системы более эффективные способы ее реализации;

- эквивалентности ресурсов, как и эквивалентности разметок, можно использовать для редукции сети.

Цель работы состоит в точном определении и исследовании отношения эквивалентности ресурсов в сетях Петри, которое соответствовало бы содержательному понятию возможности заменить одни ресурсы на другие так, чтобы наблюдаемое поведение системы не менялось с точки зрения бисимуляционной эквивалентности. Основное внимание при этом уделяется проблеме разрешимости определяемого отношения и алгоритмам нахождения бисимуляционно эквивалентных ресурсов для заданной сети Петри.

Для достижения указанной цели решаются следующие задачи:

1) Исследование свойств и структуры отношения подобия ресурсов и других отношений эквивалентности на множестве ресурсов обыкновенной сети Петри, сохраняющих наблюдаемое поведение системы. Исследование разрешимости этих отношений и построение соответствующих алгоритмов.

2) Исследование бисимуляции ресурсов в сетях Петри с невидимыми переходами (когда срабатывание некоторых переходов не видно наблюдателю) и построение соответствующих алгоритмов.

3) Определение и исследование бисимуляции ресурсов для сетей с индивидуальными фишками — сетей Петри высокого уровня и вложенных сетей Петри.

4) Разработка алгоритмов редукции сети Петри на основе бисимуля-ционной эквивалентности ресурсов.

Основные результаты.

1) Введено понятие ресурса сети Петри. Определено отношение подобия ресурсов сети Петри, сохраняющее бисимулярность разметок, исследованы его свойства. В частности, доказано, что подобие ресурсов обладает конечным базисом относительно аддитивного транзитивного замыкания и в то же время неразрешимо.

2) Определено отношение условного подобия ресурсов сети Петри, исследованы его свойства. Доказано, что множество пар подобных ресурсов полулинейно, причем в качестве базиса разложения могут использоваться пары условно подобных ресурсов.

3) Определено отношение бисимуляции ресурсов сети Петри, исследованы его свойства и взаимосвязь с подобием ресурсов. Показано, что бисимуляция ресурсов является сужением подобия ресурсов. Построен алгоритм проверки того, является ли данное отношение на множестве ресурсов бисимуляцией. Получен алгоритм построения для заданной обыкновенной сети Петри отношения бисимуляции на множестве ресурсов размера не больше заданного, т.е. построения отношения, аппроксимирующего максимальную биси-муляцию ресурсов.

4) Отношения подобия и бисимуляции ресурсов также определены и исследованы для следующих классов сетей Петри:

• сети Петри с невидимыми переходами;

• сети Петри высокого уровня (на примере раскрашенных сетей);

• вложенные сети Петри.

5) Сформулированы правила построения редуцирующих преобразований обыкновенных сетей Петри на основе подобия ресурсов.

Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы.

Заключение

Перечислим основные научные результаты данной диссертации:

1) Введено понятие ресурса сети Петри. Определено и исследовано отношение подобия ресурсов. Показано, что оно соответствует содержательному понятию возможности заменить одни ресурсы на другие так, чтобы наблюдаемое поведение системы не менялось с точки зрения бисимуляционной эквивалентности. Обнаружены следующие свойства подобия ресурсов:

• подобие ресурсов является сужением максимальной бисимуляции разметок;

• подобие ресурсов обладает конечным базисом относительно аддитивного транзитивного замыкания;

• иодобие ресурсов неразрешимо;

• множество пар подобных ресурсов полулинейно, причем в качестве базиса разложения можно использовать пары условно подобных ресурсов.

2) Определено и исследовано отношение бисимуляции ресурсов. Показано, что бисимуляция ресурсов является сужением подобия ресурсов. Предложен алгоритм проверки того, является ли данное отношение бисимуляцией ресурсов. Предложен алгоритм построения аппроксимации максимальной (по вложению) бисимуляции ресурсов для данной сети Петри.

3) Определены и исследованы понятия ресурса, подобия и бисимуляции ресурсов для трех классов формальных систем, основанных на обыкновенных сетях Петри:

• сетей Петри с невидимыми переходами (расширение класса обыкновенных сетей Петри за счет введения понятия скрытого внутрисистемного срабатывания);

• сетей Петри высокого уровня (класс, равномощный обыкновенным сетям Петри, на уровне синтаксиса обладающий конструкциями статической модульности и иерархизма);

• вложенных сетей Петри (расширение класса обыкновенных сетей Петри за счет введения динамического иерархизма и модульности).

Для каждого из этих классов формальных моделей получен ряд результатов.

4) Разработаны методы редукции обыкновенных сетей Петри на основе бисимуляции ресурсов, не изменяющие поведение сети в смысле бисимуляционной эквивалентности.

Возможные направления дальнейших исследований:

1) Решение проблемы совпадения максимальной бисимуляции ресурсов и подобия ресурсов.

2) Построение для различных классов сетей Петри алгоритмов редукции сети на основе бисимуляции (подобия) ресурсов.

3) Применение к подобию ресурсов подхода, предложенного Н.С.Сидоровой [16] и состоящего в ограничении рассматриваемого множества состояний некоторым интересующим нас замкнутым подмножеством.

4) Построение аналогов бисимуляции (подобия) ресурсов для других классов формальных систем.

В заключение я хотел бы выразить глубокую признательность своему научному руководителю профессору Ирине Александровне Ломазовой за постоянное внимание и всестороннюю поддержку в научной работе. Эта диссертация многим ей обязана.

Также хочу поблагодарить моих первых научных руководителей — профессора Валерия Анатольевича Соколова и Наталью Сергеевну Сидорову, познакомивших меня со сложным и интересным миром формальных систем.

1. Алгоритмы, математическое обеспечение и архитектура многопроцессорных вычислительных систем. Под ред. Ершова А.П. Новосибирск: Наука. 1982

2. Ачасова С.М., Бандман О.Л. Корректность параллельных вычислительных процессов. Новосибирск: Наука. 1990.

3. Башкин В.А. Методы насыщения сетей Петри с невидимыми переходами // Моделирование и анализ информационных систем. Яро- . славль: ЯрГУ. 1999. Вып.б. С. 16-20.

4. Башкин В.А. Бисимуляция ресурсов в сетях Петри с невидимыми переходами // Современные проблемы математики и информатики: Сборник научных трудов молодых ученых, аспирантов и студентов. Ярославль: ЯрГУ. 2002. Вып.б. С.79-85.

5. Башкин В.А. Конечное представление отношений на мультимножествах // Моделирование и анализ информационных систем. Ярославль: ЯрГУ. 2003. Вып.10. С.56-59.

6. Башкин В.А. Бисимуляция ресурсов в сетях Петри // Тез. доклада на IV ежегодной научно-практической конференции студентов, аспирантов и молодых ученых Ярославской области. Ярославль, 2003. С. 15.

7. Башкин В.А., Ломазова И.А. Бисимуляция ресурсов в сетях Петри // Известия РАН: Теория и системы управления. 2003. №4. С. 115-123.

8. Котов В.Е. Сети Петри. М.: Наука. 1984.

9. Ломазова И.А. Моделирование мультиагентных динамических систем вложенными сетями Петри // Программные системы: Теоретические основы и приложения. М.: Наука. 1999. С.143-156.

10. Ломазова И.А. Некоторые алгоритмы анализа для многоуровневых вложенных сетей Петри // Известия РАН: Теория и системы управления. 2000. т. С.965-974.

11. Ломазова И.А. Рекурсивные вложенные сети Петри: анализ семантических свойств и выразительность // Программирование. 2001. №4. С.21-35.

12. Ломазова И.А. Объектно-ориентированные сети Петри: формальная семантика и анализ // Системная информатика. Новосибирск. 2002. №8. Вып.8. С.143-205.

13. Питерсон Дж. Сети Петри и моделирование систем. М.: Мир. 1984.

14. Подловченко Р.И. Эквивалентные преобразования схем программ с коммутирующими и монотонными операторами // Программирование. 2002. №6. С.301-313.

15. Сидорова Н.С. Преобразования сетей Петри: Дис. канд. физ.-мат. наук. Ярославль: ЯрГУ. 1998.

16. Сидорова Н.С., Соколов В.А. О редукции сетей Петри // Тез. докладов на Третьей международной конференции по алгебре памяти М.И.Каргаполова. Красноярск. 1993. С.305-306.

17. Соколов В.А., Кушнаренко О.Б. Рекурсивно-параллельное программирование и сети Петри: моделирование, анализ и верификация программ // Моделирование и анализ информационных систем. Ярославль: ЯрГУ. 1994. Вып.2. С.98-102.

18. Тарасюк И.В. Эквивалентностные понятия для моделей параллельных и распределенных систем: Дис. канд. физ.-мат. наук. Новосибирск: ИСИ СО РАН. 1997.

19. Autant С., Schnoebelen Ph. Place bisimulations in Petri nets // Proc. of ICATPN'92. Lecture Notes in Computer Science. 1992. V.616. P.45-61.

20. Autant C., Pfister W., Schnoebelen Ph. Place bisimulations for the reduction of labeled Petri nets with silent moves // Proc. of ICCI'94. 1994.

21. Baeten J.C.M., Bergstra J.A., Klop J.W. Decidability of bisimulation equivalence for processes generating context-free languages // Journal of the ACM. 1993. V.40. P.653-682.

22. Bashkin V.A., Lomazova I.A. Reduction of Coloured Petri nets based on resource bisimulation // Joint Bulletin of NCC & IIS, Сотр. Science. Novosibirsk. 2000. V.13. P. 12-17.

23. Bashkin V.A., Lomazova I.A. Resource bisimulations in Nested Petri Nets // Proc. of CS&P'2002. Vol.1. Informatik-Bericht №161. Humboldt-IJniversitat zu Berlin. Berlin. 2002. P.39-52.

24. Bashkin V.A., Lomazova I.A. Petri Nets and resource bisimulation // Fundamenta Informaticae. 2003. V.55. №2. P. 101-114.

25. Bashkin V.A., Lomazova I. A. Resource similarities in Petri net models of distributed systems // Proc. of PACT'2003. Lecture Notes in Computer Science. 2003. V.2763. P.35-48.

26. Christensen S., Hiittel H., Stirling C. Bisimulation relation is decidable for all context-free processes // Proc. of CONCUR'92. Lecture Notes in Computer Science. 1993. V.630. P.138-147.

27. Christensen S., Hirshfeld Y., Moller F. Decomposability, decidability and axiomatisabilitv for bisimulation equivalence on basic parallel processes // Proc. of LICS'93. 1993. P.386-396.

28. Christensen S., Hirshfeld Y., Moller F. Bisimulation relation is decidable for basic parallel processes // Proc. of CONCUR'93. Lecture Notes in Computer Science. 1993. V.715. P. 143-157.

29. Esparza J., Nielsen M. Decidability Issues for Petri Nets — a Survey // Bulletin of the EATCS. 1994. V.52. P.245-262.

30. Esparza J. Decidability and complexity of Petri net problems — an introduction // Lecture Notes in Computer Science. 1998. V.1491. P.374-428.

31. Esser R. An Object Oriented Petri Net Approach to Embedded System Design. PhD theses. Zurich: Swiss Federal Institute of Technology. 1996.

32. Genrich H., Lautenbach K. System modeling with high-level Petri nets // Theoretical Computer Science. 1981. V.13. P.109-136.

33. Haddad S., Poitrenand D. Theoretical aspects of recursive Petri nets // Proc. of ATPN'99. Lecture Notes in Computer Science. 1999. V.1639. P.228-247.

34. Hirshfeld Y. Congruences in commutative semigroups. Research report ECS-LFCS-94-291. Edinburgh: University of Edinburgh, Department of Computer Science. 1994.

35. Hirshfeld Y., Jerrum M., Moller F. A polinomial algorithm for deciding bisimulation equivalence of normed basic parallel processes // Mathematical Structures in Computer Science. 1996. V.6. P.251-259.

36. Hirshfeld Y., Jerrum M. Bisimulation equivalence is decidable for normed Process Algebra // Proc. of ICALP'99. Lecture Notes in Computer Science. 1999. V.1644.

37. Jantzen M. Language Theory of Petri Nets // Lecture Notes in Computer Science. 1987. V.254.

38. Jancar P., Kucera P., Moller F. Simulation and Bisimulation over One-Counter Processes // Proc. of STACS'2000. Theoretical Computer Science. 2000.

39. Jancar P., Moller F. Techniques for decidability and undecidability of bisimilarity // Proc. of CONCUR'99. Lecture Notes in Computer Science. 1999. V.1664. P.30-45.

40. Jensen K. Coloured Petri Nets and the Invariant Method // Theoretical Computer Science. 1981. V.14.

41. Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1: Basic Concepts, 1992. Volume 2: Analysis Methods, 1994. EATCS Monographs in Computer Science. Springer.

42. Jensen K., Christensen S., Huber P., Holla M. Design/CPN Reference Manual. Computer Science Department, University of Aarhus, Denmark. Online:http: //www. daimi . au. dk/designCPN.

43. Lomazova I.A. Nested Petri nets — a Formalism for Specification and Verification of Multi-Agent Distributed Systems // Fundamenta Infor-maticae. 2000. V.43. P.195-214.

44. Lomazova I.A. Nested Petri nets: multi level and recursive systems // Fundamenta Informaticae. 2001. V.47. P.283-293.

45. Milner R. A Calculus of Communicating Systems // Lecture Notes in Computer Science. 1980. V.92.

46. Moller F. Infinite results // Proc. of CONCUR'96. Lecture Notes in Computer Science. 1996. V.1119. P.195-216.

47. Park D.M.R. Concurrency and automata on infinite sequences // Lecture Notes in Computer Science. 1981. V.104.

48. Petri C.A. Kommunikation mit Automaten. PhD theses. Bonn: Institute fur Instrumentelle Mathematik. 1962.

49. Redei L. The theory of finitely generated commutative semigroups. Oxford University Press. 1965.

50. Reisig W. Petri nets. Springer. 1985.

51. Reisig W. Petri nets and algebraic specifications // Theoretical Computer Science. 1991. V.80. P.l-34.

52. Reisig W. Petri net models of distributed algorithms // Lecture Notes in Computer Science. 1995. V.1000.

53. Schnoebelen Ph., Sidorova N. Bisinnilation and the reduction of Petri nets // Proc. of ICATPN'2000. 2000.

54. Smith E. A Survey on High-Level Petri-Net Theory // Bulletin EATCS. 1996. V.59. P.267-293.

55. Smith E. Principles of high-level net theory. Lectures on Petri nets // Lecture Notes in Computer Science. 1998. V.1491. P.174-210.

56. Stirling C. Decidability of bisimulation equivalence for normed pushdown processes // Theoretical Computer Science. 1998. V.195. P.113-131.

57. Tarasyuk I.V. r-Equivalences and Refinement for Petri Net Based Design. Technische Berichte FI00-11. Dresden: Technische Universitat zu Dresden. 2000.