Бисимуляция ресурсов в сетях Петри тема диссертации и автореферата по ВАК РФ 05.13.17, кандидат физико-математических наук Башкин, Владимир Анатольевич

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

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

Введение

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) Построение аналогов бисимуляции (подобия) ресурсов для других классов формальных систем.

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Башкин, Владимир Анатольевич, 2003 год

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.