Содержание к диссертации
Введение
1. Сети Петри и бисимуляция разметок 13
1.1. Множества, отношения, мультимножества 13
1.2. Системы помеченных переходов, бисимуляции 16
1.3. Сети Петри 24
2. Бисимуляция ресурсов в обыкновенных сетях Петри 30
2.1. Конечное представление отношений 30
2.1.1. Базисы отношений 30
2.1.2. Конечность базиса ЛТ-замыкания 36
2.1.3. Свойства основного базиса 40
2.2. Подобие ресурсов 45
2.2.1. Определение подобия 46
2.2.2. Свойства 49
2.2.3. Неразрешимость 52
2.3. Условное подобие ресурсов 55
2.3.1. Определение условного подобия 55
2.3.2. Свойства 56
2.3.3. Полулинейность множества пар подобных ресурсов 57
2.4. Бисимуляция ресурсов 63
2.4.1. Определение бисимуляции 63
2.4.2. Слабое свойства переноса 67
2.4.3. Проверка бисимулярности отношения 70
2.4.4. Построение аппроксимации максимальной бисимуляции ресурсов 72
2.5. Редукция сети на основе подобия ресурсов 76
3. Бисимуляция ресурсов в сетях с невидимыми переходами 84
3.1. Сети Петри с невидимыми переходами 84
3.2. Подобие и бисимуляция ресурсов в сетях с г-переходами . 86
3.3. Насыщенные сети Петри 89
3.4. Бисимуляция ресурсов 92
3.5. Алгоритм построения аппроксимации 97
4. Бисимуляция ресурсов в сетях Петри высокого уровня 100
4.1. Сети Петри высокого уровня 100
4.2. Раскрашенные сети Петри 101
4.3. Элементарные ресурсы 105
4.4. Подобие и бисимуляция ресурсов в раскрашенных сетях 106
4.5. Алгоритм построения аппроксимации 109
5. Бисимуляция ресурсов во вложенных сетях Петри 112
5.1. Вложенные сети Петри 112
5.2. Объектные ресурсы 120
5.3. Системные ресурсы 123
5.4. Системно-автономные ресурсы 129
5.5. Рекурсивные вложенные сети Петри 132
Заключение 137
Список литературы 138
- Системы помеченных переходов, бисимуляции
- Полулинейность множества пар подобных ресурсов
- Подобие и бисимуляция ресурсов в сетях с г-переходами
- Подобие и бисимуляция ресурсов в раскрашенных сетях
Введение к работе
В настоящее время большой и устойчивый интерес проявляется к средствам моделирования и анализа сложных параллельных и распределенных систем. Такими системами являются, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы и алгоритмы, протоколы взаимодействия (коммуникационные, верифицирующие), модели технологических и бизнес-процессов. Это обусловлено в первую очередь высоким риском возникновения ошибок на стадии проектирования таких систем и чрезвычайно высокой ценой проявления этих ошибок на стадии эксплуатации.
При исследовании сложной системы нас могут интересовать различные ее свойства, например, наличие тупикового состояния, возможность переполнения буфера и т.п. Математические методы во многих случаях позволяют получить однозначный ответ на подобные вопросы. При этом важное значение имеет первоначальный выбор используемого формализма, то есть способа моделирования реальной системы.
Для решения задач анализа и верификации в теории параллельных и распределенных вычислений в настоящее время предлагаются различные способы моделирования реальных систем [1, 2]. К числу наиболее известных формализмов можно отнести конечные автоматы, алгебры процессов, CCS Р.Милнера, языки трасс, а также различные их модификации, в том числе с добавлением конструкций времени и вероятности.
Различные классы моделей обладают различными свойствами выразительности и алгоритмической разрешимости. Причем эти два параметра модели, как правило, противоречат друг другу: выбранный формализм может оказаться или очень выразительным и не поддающимся анализу, или же позволяющим эффективно решать все необходимые проблемы, но при этом слишком слабым, недостаточно полно описывающим моделируемую систему.
Сети Петри — достаточно выразительная модель параллелизма, обладающая в то же время значительным набором разрешимых свойств. В частности, для обыкновенных сетей Петри разрешимы проблемы до-
гтижимости, останова, живости, ограниченности, покрытия (см. обзоры [30, 31, 53, 55]).
Основы теории сетей Петри были заложены в 60-х годах XX века немецким ученым Карлом Петри [51]. С тех пор теория сильно разрослась и до сих пор продолжает активно развиваться. Причиной популярности сетей Петри является простота и наглядность описания параллелизма, а также удобное графическое представление модели. К тому же за время исследований сетей Петри было накоплено большое количество теоретических результатов и практического опыта в области спецификации и анализа параллельных и распределенных систем. Существуют достаточно обширные электронные архивы научной информации по сетям Петри (см. [62, 63, 64, 65]).
Среди отечественных исследований по сетям Петри и спецификации и анализу распределенных систем отметим работы Н.А. Анисимо-ва, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой.
В основе формализма сетей Петри лежит идея моделирования создания, уничтожения и перемещения внутренних ресурсов системы, представленных в виде маркеров (фишек). Фишки располагаются во внутренних ячейках сети Петри — так называемых позициях, откуда их забирают в момент срабатывания переходы, моделирующие действия системы. Переход может сработать только при наличии необходимого числа фишек в своих входных позициях, он же в момент срабатывания помещает в свои выходные позиции соответствующий набор фишек.
Подобная система при всей своей простоте оказывается весьма выразительной. Сети Петри позволяют с достаточной степенью детализации моделировать вычислительные процессы, процессы управления в параллельных системах и протоколы взаимодействия. В них имеются простые конструкции для описания структур параллелизма: последовательная композиция, выбор, параллельное слияние.
Существует большое число классов формальных моделей, построенных на основе сетей Петри. Некоторые являются расширением класса обыкновенных сетей Петри и по выразительности приближаются к машинам Тьюринга, некоторые — сужением (иногда до конечных систем). Существуют сети Петри с ингибиторными дугами, с невидимыми переходами, сети со временем и вероятностью, объектно-ориентированные сети Петри [32, 55]. В работах В.Е. Котова и Л.А. Черкасовой [9] были определены формализмы регулярных и иерархических сетей Петри, обладающие удобным алгебраическим представлением.
За последние два десятилетия образовался довольно обширный на-
бор классов формальных систем с общим названием "сети Петри высокого уровня", в которых тем или иным способом вводятся конструкции модульности и иерархичности [32, 33, 44, 57, 58]. Среди всех формализмов сетей Петри высокого уровня следует выделить раскрашенные сети К. Йенсена (Coloured Petri Nets, CPN) [43, 44], получившие наибольшее распространение в практических приложениях. В частности, на их основе создана популярная система моделирования и верификации De-sign/CPN [45].
Большое внимание уделяется разработке формализмов для представления при помощи сетей Петри мультиагентных систем со сложной динамической структурой (вплоть до рекурсивности). К формализмам такого рода можно отнести объектные сети Р. Фалька [61], схемы рекурсивно-параллельных программ О.Б. Кушнаренко и В.А. Соколова [18], рекурсивные сети С. Хаддада и Д. Пватрено [34]. В работах И.А. Ло-мазовой [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) Исследование свойств и структуры отношения подобия ресурсов и других отношений эквивалентности на множестве ресурсов обыкновенной сети Петри, сохраняющих наблюдаемое поведение системы. Исследование разрешимости этих отношений и построение соответствующих алгоритмов.
Исследование бисимуляции ресурсов в сетях Петри с невидимыми переходами (когда срабатывание некоторых переходов не видно наблюдателю) и построение соответствующих алгоритмов.
Определение и исследование бисимуляции ресурсов для сетей с индивидуальными фишками — сетей Петри высокого уровня и вложенных сетей Петри.
Разработка алгоритмов редукции сети Петри на основе бисимуля-ционной эквивалентности ресурсов.
Основные результаты.
Введено понятие ресурса сети Петри. Определено отношение подобия ресурсов сети Петри, сохраняющее бисимулярность разметок, исследованы его свойства. В частности, доказано, что подобие ресурсов обладает конечным базисом относительно аддитивного транзитивного замыкания и в то же время неразрешимо.
Определено отношение условного подобия ресурсов сети Петри, исследованы его свойства. Доказано, что множество пар подобных ресурсов полулинейно, причем в качестве базиса разложения могут использоваться пары условно подобных ресурсов.
Определено отношение бисимуляции ресурсов сети Петри, исследованы его свойства и взаимосвязь с подобием ресурсов. Показано, что бисимуляция ресурсов является сужением подобия ресурсов. Построен алгоритм проверки того, является ли данное отношение на множестве ресурсов бисимуляцией. Получен алгоритм построения для заданной обыкновенной сети Петри отношения бисимуляции на множестве ресурсов размера не больше заданного, т.е. построения отношения, аппроксимирующего максимальную биси-муляцию ресурсов.
Отношения подобия и бисимуляции ресурсов также определены и исследованы для следующих классов сетей Петри:
сети Петри с невидимыми переходами;
сети Петри высокого уровня (на примере раскрашенных сетей);
вложенные сети Петри.
5) Сформулированы правила построения редуцирующих преобразований обыкновенных сетей Петри на основе подобия ресурсов.
Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы.
В первой главе диссертации приводятся общие определения из теории мультимножеств, теории бисимуляций и теории сетей Петри.
Во второй главе приводятся результаты о способах задания бесконечных отношений на мультимножествах при помощи конечных базисов. Доказывается, что любое аддитивно и транзитивно замкнутое отношение на множестве мультимножеств обладает конечным базисом. Приводится структура одного такого конечного базиса, названного основным базисом. Доказывается ряд его свойств, приводятся алгоритм проверки принадлежности данной пары мультимножеств замыканию основного базиса и алгоритм построения основного базиса отношения по любому другому конечному базису.
Вводятся понятия ресурса сети Петри как мультимножества над множеством позиций сети. Вводится понятие подобных ресурсов. Два ресурса подобны, если в любой разметке мы можем заменить один из них на другой, и при этом дальнейшее наблюдаемое поведение сети не изменится (в смысле бисимуляционной эквивалентности поведений).
Исследуются свойства подобия ресурсов — отношения на множестве ресурсов сети Петри, состоящего из всех пар подобных ресурсов. Доказывается, что подобие ресурсов является отношением эквивалентности, замкнутым относительно сложения. Оно обладает конечным базисом относительно аддитивного транзитивного замыкания.
Доказывается, что корректное слияние позиций [16] является сужением подобия ресурсов, состоящим из пар ресурсов единичной мощности. Из этого следует неразрешимость подобия ресурсов для случая обыкно-венньус сетей Петри.
Вводится понятие условного подобия ресурсов, исследуются его свойства. Доказывается теорема о полулинеиности множества пар подобных ресурсов.
Вводится понятие бисимуляций ресурсов. Описываются его свойства, взаимосвязь с подобием ресурсов, приводятся алгоритм проверки бисимуляций ресурсов с использованием слабого свойства переноса и алгоритм построения аппроксимации максимальной бисимуляций ресурсов.
Рассматриваются способы редукции обыкновенных сетей Петри на основе подобия (бисимуляций) ресурсов.
В третьей главе рассматривается расширение класса сетей Петри — сети Петри с невидимыми переходами. Показывается, что обобщение бисимуляции ресурсов — т-бисимуляция ресурсов — в силу ряда причин не может быть эффективно построена. Предлагается более сильное вычислимое отношение - гр-бисимуляция ресурсов, обладающее слабым свойством переноса в случае р-насыщенности сети. Доказывается один критерий р-насыщешюсти сети Петри с невидимыми переходами.
В четвертой главе понятие бисимуляции ресурсов переносится на сети Петри высокого уровня — формализм той же выразительной мощности, что и обыкновенные сети Петри, но обладающий элементами статической модульности и иерархичности. Рассматривается один из наиболее популярных классов сетей Петри высокого уровня — раскрашенные сети К. Йенсена [44]. Предлагается обобщение понятия позиции сети Петри — так называемый элементарный ресурс. Его использование позволяет строить бисимуляции ресурсов непосредственно в сетях высокого уровня, без преобразования к обыкновенным.
В пятой главе рассматривается класс вложенных сетей Петри [10]. Этот формализм гораздо более выразителен, чем обыкновенные сети Петри, и позволяет строить модели сложных мультиагентных систем с динамической структурой. Предлагается три вида подобий ресурсов во вложенных сетях Петри, использующие различные виды локальностей (на разных "слоях" модели).
Рассматривается обобщение вложенных сетей — так называемые рекурсивные вложенные сети Петри [12], в которых в качестве фишек могут выступать не только обыкновенные, но и вложенные сети. Доказывается, что класс контекстно-свободных языков строго вкладывается в класс тупиковых языков вложенных рекурсивных сетей. Из этого следует, в частности, что отношения подобия и бисимуляции ресурсов в случае рекурсивных сетей не могут быть построены с той же степенью эффективности.
Системы помеченных переходов, бисимуляции
Заметим, что для любой пары (х,у) Є ВА выполняется х + у — Зг, где г N (так как при сложении пар из В кратность суммы их компонентов трем сохраняется). Следовательно, для последней пары последовательности выполняется е + 3 = Зг, то есть є также кратно трем. Последовательно применив это рассуждение для всех остальных пар (справа налево), получим, что а кратно трем. Тогда 1 + а не может быть кратно трем, то есть пара (1,а) не принадлежит ВА — противоречие. 4) Имеем Вт = {(1,1),(2,2),(1,2),(2,1)}. Следовательно, и в данном случае выполняется (1,3) (ВТ)А. 5) Рассмотрим пару (2,3). Имеем: (2,3) Є(ВТ)А, так как (2,3) = (1,1) + (1,2). (2,3) . {ВА)Т, так как в противном случае пара (1,3) принадлежала бы отношению (ВА)Т (как транзитивное замыкание пар (1,2) и (2,3)), что мы уже опровергли в доказательстве пункта 3.
Следовательно, (ВА)Т % {ВТ)А. 6) В качестве примера рассмотрим множество X из одного элемента и отношение В = {(1,2)}. Рассмотрим пару (1,4). Имеем: (1,4) Є {ВА)Т (как транзитивное замыкание пар (1,2) и (2,4)). (1,4) (ВТ)А (очевидно). Следовательно, (ВТ)А % {ВА)Т. Таким образом, ЛГ-замыкание — наиболее эффективный способ построения бесконечных отношений (получаемые с его помощью бесконечные отношения — самые слабые). Определим, в каких случаях конечный базис существует всегда (у любого отношения В, удовлетворяющего заданным ограничениям). Пусть а Є {А,Т,АТ}. Определение 2.4. Отношение В С М(Х) х М(Х) называется а-базисом отношения В, если (В )а = Ва. Базис В называется минимальным а-базисом отношения В, если не существует В" С В , такого что (В")а = Ва. Лемма 2.2. 1) Вес минимальные а-базисы отношения В либо конечны, либо бесконечны. 2) Если у В существует конечный а-базис, то все минимальные а-базисы отношения В конечны; 3) Если у В существует бесконечный минимальный а-базис, то все а-базисы отношения В бесконечны. Доказательство. 1) Предположим противное. Пусть В/ и В, - различные минимальные базисы отношения В, причем В/ - конечный, а Д -бесконечный. Каждый элемент базиса В/ может быть выражен через конечное число элементов Д. Поскольку число элементов В/ конечно, весь базис В/ может быть выражен через конечное подмножество базиса Д. Следовательно, если Д не конечен, то он не минимален - противоречие. 2) В качестве одного из минимальных базисов можно взять часть данного конечного базиса. Тогда из первой части леммы следует конечность всех минимальных базисов. 3) Предположим противное - существует конечный базис. В качестве одного из минимальных базисов можно взять часть данного конечного базиса. Тогда из первой части леммы следует конечность всех минимальных базисов - противоречие. Мы хотим определить, при каких условиях а-замкнутое и в общем случае бесконечное отношение В обладает конечным а-базисом, то есть может быть представлено конечным числом элементов. Мы не рассматриваем в качестве а симметричные замыкания, так как с их помощью невозможно получить из конечного отношения бесконечное. Также мы не рассматриваем рефлексивные замыкания, так как получаемые с их помощью бесконечные отношения имеют простую структуру. В качестве возможных ограничений на В мы рассматриваем требования его симметричности, рефлексивности и транзитивности. Рассмотрим в качестве а аддитивные и транзитивные замыкания. Оказывается, даже если В - отношение эквивалентности, у него могут существовать бесконечные минимальные базисы. Утверждение 2.1. 1) Существуют отношения эквивалентности с бесконечными минимальными А-базисами. 2) Существуют отношения эквивалентности с бесконечными минимальными Т-базисами. Пример 2.1. В качестве примера для обоих случаев рассмотрим множество Л из одного элемента и отношение эквивалентности Я = {(і,0,(1,і+ 2),(і + 2,1) \ІЄЩ (пары мультимножеств представлены как пары натуральных чисел). Рассмотрим случай Л-замыкания. Пусть В = {(0,0),(1,1)} U {(l,i + 2), (г + 2,1) і Щ. Отношение В является Л-базисом отношения ВА. Докажем минимальность В . Предположим противное: пусть некоторая пара (х,у) Є В может быть получена аддитивным замыканием других пар из В . Однако при любом сложении мультимножеств видов (1,г + 2), (г + 2,1) или (1,1) (пустую пару можно не рассматривать) в итоговой паре оба коэффициента становятся больше единицы - противоречие. Рассмотрим случай Т-замыкания. Пусть В = {(0,0)} U {(1,і + 2), (г + 2,1) і Є N}. Очевидно, что В является Т-базисом отношения Вт (любая пара вида (г, 0 может быть по лучена транзитивным замыканием двух симметричных пар). Докажем минимальность В . Предположим противное: некая пара (х, у) Є В , где х ф у, может быть получена транзитивным замыканием других пар из В . Однако при любом транзитивном замыкании мультимножеств ви дов (1л + 2) и (г + 2,1) может получиться только рефлексивная пара противоречие. Итак, ни аддитивное, ни транзитивное замыкание не могут быть использованы для генерации бесконечных отношений на основе конечных базисов, даже если В - отношение эквивалентности. Кроме того, легко показать, что существуют аддитивные и транзитивные замыкания отношений эквивалентности, которые сами не являются отношениями эквивалентности. Рассмотрим в качестве а аддитивное транзитивное замыкание. В случае аддитивных транзитивных замыканий вместо полной рефлексивности отношения В достаточно требовать только 1-рефлексив-ности, так как аддитивное замыкание 1-рефлексивного отношения рефлексивно (с точностью до пустой пары (0,0)). Использовать же полную рефлексивность неудобно, так как рефлексивные отношения на мультимножествах бесконечны a priori. Утверждение 2.2. 1) Существуют симметричные отношения с бесконечными минимальными AT -базисами. 2) Существуют 1-рефлексивные отношения с бесконечными минимальными АТ-базисами. В качестве доказательства рассмотрим примеры: Пример 2.2. Рассмотрим множество X из двух элементов и симметричное отношение
Полулинейность множества пар подобных ресурсов
Таким образом, условное подобие замкнуто относительно сложения. Кроме того, оно инвариантно относительно расширения условия. Утверждения 2.6.4 и 2.6.5 показывают, что общая часть может быть удалена из подобных ресурсов. Утверждения 2.6.6 и 2.6.7 показывают, что разность как пар подобных, так и пар условно подобных ресурсов является парой условно подобных ресурсов. Кроме того, условное подобие ресурсов замкнуто относительно сложения ресурсов и объединения условий (утверждение 2.6.8).
Отметим, что, в отличие от подобия ресурсов, условное подобие замкнуто относительно вычитания. Это свойство будет далее использовано при конструировании базиса отношения условного подобия ресурсов.
Следующее утверждение устанавливает взаимосвязь между подобием ресурсов и условным подобием ресурсов: Утверждение 2.7. Пусть г,.s,m,m М{Р), га га . Тогда Доказательство. (= ) Пусть га + г и т + s. Поскольку m « га , по свойству подобия получим га + г % га + s. Тогда из утверждения 2.6.1 получим г %m s. (4=) Пусть г «т 5. Из утверждения 2.6.1 получим га + г « га + s. Тогда из т % т по свойству подобия получим га + г « га + s. Отношение (]) более хорошо структурировано, чем отношение (). В частности, оно замкнуто не только относительно сложения пар, но и относительно вычитания. Поэтому оно должно обладать более простым базисом. Построим такой базис. Определение 2.11. Пусть г, s, г , s , г", s" Є М{Р). Пара условно подобных ресурсов г « s называется минимальной, если ее нельзя представить как сумму двух других пар условно подобных ресурсов, то есть для любой непустой пары г « s из г = г + г" и 5 = s + s" следует г = г и s = .; . Из утверждения 2.6.7 получаем Следствие 2.2. Любая пара условно подобных ресурсов может быть представлена в виде суммы минимальных пар условно подобных ресурсов. Поскольку пара условно подобных ресурсов может быть представлена как вектор длины 2\Р\ с целочисленными неотрицательными координатами, а минимальная пара условно подобных ресурсов минимальна также и относительно обычного покоординатного сравнения таких векторов, для любой помеченной сети Петри множество минимальных пар условно подобных ресурсов конечно. Следовательно, Утверждение 2.8. Множество всех пар условно подобных ресурсов является аддитивным замыканием конечного множества минимальных пар условно подобных ресурсов. Определение 2.12. Пара подобных ресурсов г и s называется минимальной, если ее нельзя представить как сумму непустой пары подобных ресурсов и пары условно подобных ресурсов, то есть для любой непустой пары подобных ресурсов г « s из г = г + г" и $ = а + $" следует г = г и S = .$ . Из утверждений 2.6.6 и 2.8 имеем Следствие 2.3. Любая пара подобных ресурсов может быть представлена в виде суммы одной минимальной пары подобных ресурсов и нескольких минимальных пар условно подобных ресурсов. Заметим, что по свойству покоординатного сравнения векторов с целочисленными неотрицательными компонентами, для любой пары условно подобных ресурсов г « s множество ее минимальных условий (относительно покоординатного сравнения) конечно. Обозначение 2.1. Пусть R С М(Р) х М{Р) — некоторое подмножество множества пар условно подобных ресурсов (г RJJ S для всех (г, з) Є R). Пусть множество всех общих условий для R. Через Cond(R) обозначим множество минимальных элементов В (относительно покоординатного сравнения, рассматривая элементы В как вектора длины 2Р). Заметим, что из утверждения 2.7 следует, что для любой пары (и, v) Cond(R) оба ресурса и и v являются условиями для любой пары (г, s) Є R. Кроме того, в силу свойства покоординатного сравнения векторов, для любого R множество Cond(R) конечно. Обозначение 2.2. Пусть u,v Є М(Р) и и й v. Через S(u,v) обозначим множество всех потенциальных дополнений к паре (и, У) (корректных относительно подобия ресурсов): S{u,v) = {(г,г ) ЄМ{Р)хМ(Р) u + r &v + r }. Через Sm-m(u,v) обозначим множество всех минимальных относительно покоординатного сравнения элементов множества S(u,v). Утверждение 2.9. Пусть u,v,u ,v Є М.{Р) v. Тогда 1) S(u,v) является отношением эквивалентности; 2) S(u,v) замкнуто относительно сложения; 3) и « и, и » v , (и, и) (и1, v ) = S(u,v) С S(u ,v ); 4) Smi„{u,v) конечно. Доказательство. 1) Рефлексивность. Очевидно, что и : v = u + r v + г для любого г. Симметричность. Пусть (г, s) Є S(u,v). Покажем, что (s,r) Є S(u,v). По определению S(u,v) выполняется и + г к v + s. Из u и, S Ri S и свойства аддитивной замкнутости подобия имеем u + s « v + s. Замкнув пары и + r и v + s и u + s v + s по транзитивности, получим u + s « u + r. По свойству подобных ресурсов мы можем заменить в правой части и на v. и + s « и + г. Транзитивность. Пусть (r,s),(s,t) 6 S(u,v). Покажем, что (г, t) Є S(u,u). Из симметричности S(u,v) имеем (t,s) Є 5(u,u), то есть U + t « U + S. Замкнув по транзитивности эту пару и пару u + r s» и + s, получим и + г й и + !. По свойству подобных ресурсов мы можем заменить в правой части и на v: и + г и v + t. 2) Пусть (г,$), (г , б ) Є 5(и, и). Покажем, что (г + г , s + 5 ) S(u, v). Из u+r % v+s получим u+r+r w t +s+r . Из симметричности 5(и, v) следует (s , г ) 5(u, и), то есть u + s « u + r . Тогда и+ 5 +з « u + r + s. Замкнув пары по транзитивности, получим и + г + г « и + 5 + 5 . По свойству подобных ресурсов мы можем заменить в правой части и на и: U + Г + г 5 V + 5 + s . 3) Обозначим (и , v ) = (и, v) + (u?, w ). Пусть и + г » и + г для некоторой пары (г, г ). Тогда u + w + rwu + zy + r Riu + u -fr ftJu + ty + r , то есть и + г и и + г . 4) Из свойств покоординатного сравнения целочисленных векторов с неотрицательными коэффициентами. Из первой и второй части утверждения следует, что множество S(u, v) обладает конечным АТ-базисом. В частности, согласно теореме 2.1, оно обладает основным базисом, составленным из минимальных относительно С элементов. Обозначение 2.3. Пусть N — помеченная сеть Петри. Через A(N) обозначим множество всех множеств потенциальных дополнений в N: A{N) = {H\3(u,v) :«Й»Л H = S(u,v)}. Утверждение 2.10. Множество A(N) конечно для любой сети N. Доказательство. Предположим противное: существует бесконечно много различных множеств потенциальных дополнений. Рассмотрим соответствующие пары подобных ресурсов. Существует бесконечно много таких пар, следовательно, существует бесконечная возрастающая последовательность (и,-,и,) пар подобных ресурсов, таких, что 5(и,-,и,-) ф S(iij,Vj) для любых і ф j. Поскольку (и,-,и,-) (ui+i,v,-+i) для любого г, из утверждения 2.9.3 получим S(i4,Vi) С S(ui+uvi+l). Напомним, что любое 5(»,-, г?,-) обладает конечным основным базисом, состоящим из минимальных относительно П. пар. Увеличение множества S(u{, ь\) может проявляться в его основном базисе двумя способами:
Подобие и бисимуляция ресурсов в сетях с г-переходами
Класс обыкновенных сетей Петри не всегда удобен для моделирования систем, содержащих большие наборы одинаковых элементов или хорошо структурированные иерархические конструкции. Сети Петри слабо структурированы, поэтому существует достаточно много формализмов на их основе, в которых тем или иным способом вводятся конструкции модульности и/или иерархичности.
Среди всех этих формализмов выделяется (как по степени изученности, так и по популярности в практическом применении) набор классов моделей, объединенных общим названием "сети Петри высокого уровня". Это, например, базисные сети высокого уровня [58], предикатные сети [33], алгебраические сети [54], раскрашенные сети К. Йенсена [44].
В отличие от обыкновенных сетей Петри, где используется только один вид фишек (черная точка), в сетях высокого уровня разметка задается при помощи фишек различных типов (цветов). Количество типов конечно, каждый тип содержит конечное число индивидуальных фишек. Например, тип Boolean содержит два экземпляра фишек — true и false.
Чтобы управлять значениями переносимых фишек, в сетях высокого уровня дугам присваиваются специальные выражения некоторого типизированного языка, содержащие в том числе переменные. Таким образом, переходы могут срабатывать в различных режимах, в зависимости от переносимых по инцидентным дугам фишек. Кроме того, каждому переходу присваивается булевская охранная функция, разрешающая или запрещающая его срабатывание в зависимости от значений фишек на входе.
Сети Петри высокого уровня позволяют строить гораздо более компактные и структурированные модели для многих классов систем. В них удобнее вносить элементы объектно-ориентированного подхода, конструкции модульности и иерархичности. При этом сети высокого уровня (при условии конечности множества индивидуальных фишек) по выразительной мощности совпадают с классом обыкновенных сетей и, следовательно, сохраняют все положительные свойства разрешимости обыкновенных сетей Петри.
Существуют простые алгоритмы, преобразующие сеть Петри высокого уровня в обыкновенную сеть (как правило, гораздо большего размера). Однако обратное преобразование весьма проблематично, поскольку может привести к совершенно неудачным с точки зрения наглядности и удобства анализа моделям. Если сравнивать сети Петри с языками программирования, то сети высокого уровня — это процедурные языки высокого уровня наподобие C++ или Pascal (хотя и без рекурсии), а обыкновенные сети Петри — низкоуровневые машинные языки или Assembler. Известно, что восстановить по машинному коду исходный текст программы практически невозможно; в сетях Петри наблюдается похожая ситуация.
Очевидно, что наибольший интерес представляют алгоритмы анализа именно для сетей высокого уровня, без перевода их в низкоуровневые сети. Далее на примере раскрашенных сетей К. Иенсена будет показано, что для подобия ресурсов и бисимуляции ресурсов такие методы существуют.
Раскрашенные сети Петри (Coloured Petri Nets, CPN) были предложены в 1981 году К. Йенсеном [43, 44]. В настоящее время это один из наиболее популярных и широко применяемых на практике формализмов. CPN-модели используются во многих программных системах моделирования и анализа (среди которых нужно выделить в первую очередь открытую систему Design/CPN [45]).
В раскрашенных сетях множество типов фишек называется множеством цветов. Позициям также приписан цвет, при этом позиция может содержать только фишки соответствующего цвета. На практике иногда используют модели на основе CPN, содержащие цвета с потенциально бесконечным набором различимых фишек, например, тип Integer. Это не совсем корректно, так как раскрашенная сеть в таком случае рав-номощна машине Тьюринга и не поддается анализу. Но, с другой стороны, на практике тип Integer никогда не является бесконечным, он ограничивается возможностями ЭВМ и допусками конкретной системы программирования.
В данной работе рассматриваются раскрашенные сети Петри с конечными типами (цветами). Рассмотрим их формальное определение. Пусть задан некоторый язык С типизированных выражений и некоторая конечная модель U этого языка. Выражения в языке С построены из переменных и констант с использованием только операции сложения мультимножеств. Элементами Ы являются индивидуальные (различимые) фишки. Тип (цвет) определяется как конечное подмножество /, типом суммы двух мультимножеств является объединение их типов. Тип элемента є обозначается как Туре(е), тип выражения 0 Є С — как Туре(в). Var(b) обозначает множество всех переменных в выраже-ниип 6.
Подобие и бисимуляция ресурсов в раскрашенных сетях
Позиции в объектной сети означают следующее: О "около вагона (нет напарника)" — грузчик находится около вагона, но он еще не принял решение брать носилки; О "около вагона (есть напарник)" — грузчик находится около вагона, и он принял решение брать носилки; О "с носилками около склада" — грузчик находится около склада, причем он пришел сюда с носилками; О "без носилок около склада" — грузчик находится около склада, причем он пришел сюда без носилок; О "перенесенный груз" — количество мешков, уже перенесенных грузчиком. Переходы в объектной сети означают следующее: .4) — грузчик вместе с каким-то другим грузчиком решают взять но силки; D 2 — грузчик вместе с каким-то другим грузчиком решают все-таки не брать носилок; D .s.3 — грузчик в паре с каким-то другим грузчиком переносят на носилках 4 мешка из вагона на склад; ? .$4 — грузчик в паре с каким-то другим грузчиком возвращаются к вагону с носилками; ? $5 — грузчик в одиночку переносит 1 мешок из вагона на склад; ? s6 — грузчик возвращаются к вагону без носилок. В данной сети представлены оба вида синхронизации — вертикальная и горизонтальная. Вертикальная синхронизация моделирует использование объектами (грузчиками) системного ресурса (носилок). Горизонтальная синхронизация моделирует взаимодействие между объектами (грузчиками) при их совместной деятельности (принятие решения брать/не брать носилки).
Например, переход в системной сети может сработать только при наличии вертикальной синхронизации с обеими переносимыми им сетевыми фишками (х и у), то есть при наличии как минимум двух грузчиков, готовых нести носилки. Переход Si в объектной сети может сработать только совместно с таким же переходом в "соседней" фишке, то есть грузчик принимает решение брать носилки только одновременно с другим грузчиком. Этим гарантируется наличие четного числа грузчиков, готовых нести носилки. Таким образом, системная сеть описывает правила поведения агентов (грузчиков) с точки зрения системы и системных ресурсов (носилок и мешков). Объектная сеть моделирует поведение отдельного агента. Такое разделение очень удобно при моделировании мультиагентных систем. Например, если мы захотим ввести в модель еще один вид грузчиков, которые не умеют пользоваться носилками, то нам не придется менять системную сеть — достаточно добавить еще один вид сетевых фишек. С другой стороны, если мы захотим добавить в модель явление недетерминированной пропажи груза со склада/из вагона (без участия грузчиков), то нам не придется менять описание поведения грузчика, достаточно добавить соответствующие переходы в системную сеть. Менять оба уровня модели (системный и объектный) придется только при появлении нового вида взаимодействия между агентом и системой или нового вида системных ресурсов (например, тачек).
Определим бисимуляцию разметок для вложенных сетей Петри. Определение 5.6. Пусть NPN = (21, {ENU..., ENk}, SN, Lab, A) — помеченная вложенная сеть Петри. Скажем, что отношение R С Vft(NPN) х 9JI(/VPyV) обладает свойством переноса, если для любой пары разметок (МьМг) Є R и для любого срабатывания перехода t Є T(NPN), такого, что М\ — М[, найдется имитирующее срабатывание и Є T(NPN), такое, что /(0 = 1{и), М2 4М (М{, М 2) R. Заметим, что из определений Lab и Act следует, что автономный шаг должен быть имитирован автономным шагом (системно- или элементно-автономным), шаг горизонтальной синхронизации — обязательно шагом горизонтальной синхронизации, шаг вертикальной синхронизации — шагом вертикальной синхронизации. Определение 5.7. Если отношения R и Я-1 обладают свойством переноса, то отношение R называется бисимуляцией разметок. Обыкновенные сети Петри являются частным случаем вложенных сетей Петри (при 21 = {} и О = 0). Следовательно, бисимуляция разметок неразрешима и для вложенных сетей Петри. 5.2. Объектные ресурсы Одним из замечательных свойств сетей Петри является то, что состояние моделируемой системы задается при помощи набора локальных состояний (позиций). Таким образом, существует два уровня иерархии: глобальное состояние — разметка сети в целом, и локальное состояние — количество фишек именно в данной позиции. Срабатывание отдельного перехода зависит не от глобального состояния системы, а от конечного набора локальных состояний (определяемого входными позициями данного перехода). В отличие от обыкновенных сетей Петри и созданных на их основе сетей высокого уровня, двухуровневые вложенные сети представляют собой формализм, позволяющий выделить не один, а три существенно различных вида локальных состояний: 1) Локальные состояния позиций элементных сетей. 2) Локальные состояния позиций системной сети, то есть мультимножества сетевых фишек, расположенных в данный момент в данной позиции, с учетом их разметок. 3) Локальные состояния позиций системной сети без учета состояний сетевых фишек. Ресурс в обыкновенной сети Петри представляет собой обобщение понятия позиции. Во вложенных сетях Петри появляется возможность при определении ресурса использовать любой из перечисленных выше видов "позиции". Как будет показано далее, некоторые из подобий, индуцированных этими тремя видами ресурсов, эффективно вычислимы. Определим понятие ресурса, использующее первый (внутриэлемент-ный) вид локальности. Определение 5.8. Объектным ресурсом помеченной вложенной сети Петри NPN = {2l,{ENu...,ENk},SN,Lab,A) называется пара (ENt,r), где г М{Р{). Объектными ресурсами вложенной сети являются ресурсы её элементных сетей, которые являются обыкновенными сетями Петри. Пусть N — (P,T,F,l) — обыкновенная сеть Петри. Для удобства обозначим максимальную бисимуляцию разметок сети N как дг.
