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

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

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

Башкин Владимир Анатольевич

Некоторые методы

ресурсного анализа сетей Петри

05.13.17 – Теоретические основы информатики

ДИССЕРТАЦИЯ

на соискание ученой степени

доктора физико-математических наук

Научный консультант д. ф.-м. н., проф.

И. А. Ломазова Ярославль – 2014 Содержание Введение...................................... 4 Предварительные сведения.................... Глава 1.

1.1. Множества и отношения........................ 1.2. Эквивалентность поведений............ .......... 1.3. Сети Петри............................... 1.4. Ресурсы в сетях Петри......................... Глава 2. Некоторые методы поиска бисимуляционно-эквивалентных ресурсов.................................... 2.1. Бисимуляция в ограниченных сетях................. 2.2. Ограниченное подобие ресурсов................... 2.3. Расслоенное подобие ресурсов.................... 2.4. Подобие обобщенных ресурсов.................... 2.5. Адаптивное управление процессами на основе подобия ресурсов. Некоторые методы анализа сетей с одномерным ресурсом.. Глава 3.

3.1. Одномерные полулинейные множества................ 3.2. Односчетчиковые контуры............... ........ 3.3. Алгоритмы анализа........................... 3.4. Правильная организованность..................... 3.5. Потоки работ с ресурсом........................ Модели с активными и обобщёнными ресурсами....... Глава 4.

4.1. Сети активных ресурсов........................ 4.2. Модульные АР-сети............... ........... 4.3. Модифицированные АР-сети..................... 4.4. Автоматы, управляемые ресурсами.................. 4.5. Клеточные сети с бесконечномерным ресурсом........... Заключение.................................... Благодарности................................. Литература.................................... Введение Актуальность темы исследования. В последние десятилетия большой и устойчивый интерес проявляется к математическим средствам моделирования и анализа сложных параллельных и распределенных систем, к которым относятся, например, вычислительные машины и комплексы с параллельной и распреде­ ленной архитектурой, параллельные программы и алгоритмы, протоколы взаи­ модействия (коммуникационные, верифицирующие), модели технологических и бизнес–процессов. При разработке подобных систем, как правило, высок риск возникновения ошибки на стадии проектирования и чрезвычайно высока цена проявления ошибки на стадии эксплуатации. Все это обуславливает интерес к формальным математическим средствам анализа и верификации, позволяющим дать ответы на вопросы о свойствах модели, например, о наличии конфликтов, тупиков или неограниченных состояний (переполнений).

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

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

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

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

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

Обычно неформальным термином “ресурс” обозначают содержимое пози­ ции (её разметку) по отношению к использующим это содержимое переходам.

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

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

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

Приведённое определение ресурса всё ещё неформально, однако позволяет по-новому взглянуть на многие аспекты теории сетей Петри. Это представляет­ ся особенно актуальным в связи с ростом интереса в последнее время к таким сферам теоретической информатики, как моделирование и анализ схем потоков работ (workflow), сервис-ориентированных архитектур, GRID-вычислений и т.п.

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

Цели и задачи диссертационной работы.

Целью работы является создание новых методов моделирования и анализа параллельных и распределенных систем на основе понятия ресурса сети Петри.

Для достижения поставленной цели концепция ресурса может быть исполь­ зована различными способами:

1. Как объект анализа. Рассматриваются свойства локальных ресурсов с точки зрения эквивалентности их воздействия на поведение системы.

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

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

Научная новизна. Основные результаты могут быть сгруппированы в со­ ответствии со способом использования понятия ресурса следующим образом:

Методы анализа поведенческих эквивалентностей ресурсов.

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

Базовые понятия теории эквивалентностей ресурсов сетей Петри были сформулированы в кандидатской диссертации соискателя. На защиту выносятся новые результаты, описывающие ключевые структурные свойства и алгоритми­ ческие приемы данной теории.

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

Предложены способы приближения отношения подобия снизу (при помощи ограниченного подобия) и сверху (при помощи расслоённого подобия). Разрабо­ таны методы адаптивного управления процессами на основе различных отноше­ ний эквивалентности ресурсов.

Представленные методы существенно мощнее известных подходов, осно­ ванных на отношении слияния позиций (Ф. Шнеблен, Н. С. Сидорова, 2000–2003), поскольку рассматривают ресурсы произвольной мощности.

Методы моделирования и анализа систем с одномерным ресурсом.

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

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

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

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

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

Разработан ряд алгоритмов анализа односчетчиковых сетей Петри, исполь­ зующих однопериодическое представление одномерного полулинейного множе­ ства достижимых состояний. В частности, для односчётчиковых сетей предло­ жен алгоритм построения символьной свёртки пространства состояний, кото­ рый позволяет получать более компактное (однопериодическое полулинейное) представление, чем известные для одно- и двухсчётчиковых сетей способы сим­ вольного описания при помощи деревьев линейных базисов множеств разметок (Дж. Хопкрофт, Ж.–Ж. Пансио, 1975) и полулинейных формул путей (Ж. Леру, Г. Сютре, 2003–2005).

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

Предложено обобщение класса WF-сетей — сети с одним неограниченным ресурсом. Этот класс достаточно интересен, поскольку позволяет моделировать многие прикладные системы — например, WF-процессы с дискретным време­ нем. Доказана разрешимость бездефектности как для размеченной, так и для неразмеченной одномерной сети (предложены алгоритмы). Предложен алгоритм определения минимального бездефектного ресурса. Эти результаты обобщают до неограниченного случая известные результаты о разрешимости бездефектности для сетей потоков работ с фиксированным ресурсом (К. ван Ней, Н. С. Сидорова и др., 2005–2013).

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

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

Построена иерархия классов одномерных клеточных сетей (цепочек), осно­ ванная на ограничении топологии системной сети. Исследована выразительная мощность ряда базовых классов данной иерархии. Доказано, что: сети с полным набором портов эквивалентны машинам Тьюринга; сети без выходных портов эк­ вивалентны конечным автоматам; сети без входных портов бисимулярны сетям Петри без коммуникаций (communication-free PN).

Методы моделирования и анализа систем, основанные на обобщении понятия ресурса.

Исследованы возможности развития языка сетей Петри засчет явного син­ таксического выделения ресурсов и наделения их расширенной семантикой.

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

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

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

Предложены новые формализмы, использующие концепцию АР-сетей для моделирования распределенных систем с динамической структурой и ненадеж­ ными компонентами. По сравнению с известными формализмами (раскрашенные сети К. Йенсена, объектные сети Р. Фалька, вложенные сети И. А. Ломазовой, гиперсети В. Павловского и др.) предложенные нами языки моделирования об­ ладают дополнительными возможностями описания процессно- и сервис-ори­ ентированных систем, обусловленными дуалистичностью поведения активного ресурса (агента/ресурса).

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

Положения, выносимые на защиту.

1. Методы поиска бисимуляционно-эквивалентных ресурсов в сетях Петри.

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

2. Методы бисимуляционной редукции систем и адаптивного управления про­ цессами на основе отношений эквивалентности ресурсов.

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

4. Методы анализа и оптимизации односчётчиковых сетей на основе сим­ вольных вычислений при помощи однопериодических базисов (глобальная достижимость, глобальная верификация темпоральной логики EF, аппрок­ симация бисимуляции, правильная организованность).

5. Методы проверки бездефектности сетей потоков работ с одномерным неогра­ ниченным ресурсом.

6. Формализм сетей активных ресурсов (АР-сети) — развитие языка сетей Петри засчет явного синтаксического выделения ресурсов и наделения их расширенной семантикой.

7. Композициональные методы анализа АР-сетей и методы нормализации их модульной структуры.

8. Расширения формализма АР-сетей для моделирования тех или иных ас­ пектов распределенных систем: АР-сети с динамическими и ненадежными компонентами, ингибиторные АР-сети, сети управляемых ресурсами авто­ матов (Р-сети).

9. Формализм клеточных Р-сетей — обобщение сетей Петри на случай бес­ конечной регулярной системной сети. Иерархия классов одномерных кле­ точных сетей (цепочек).

Степень достоверности и апробация результатов. Основные результаты диссертации докладывались на научных семинарах ЯрГУ им. П. Г. Демидова и ВЦ РАН им. А. А. Дородницына, а также на международных конференци­ ях: “Интеллектуальное управление: новые интеллектуальные технологии в за­ дачах управления” (Переславль–Залесский 1999); “Concurrency, Specification and Programming” (Берлин 2002, Руциане–Нида 2005, Берлин 2006, Краков 2009, Бер­ лин 2010, Пултуск 2011, Берлин 2012); “Parallel Computing Technologies” (Ниж­ ний Новгород 2003, Москва 2005, Санкт-Петербург 2013); “Методы и средства обработки информации” (Москва 2005); “Интеллектуальные системы и компью­ терные науки” (Москва 2006); “Программные системы: теория и приложения” (Переславль–Залесский 2006); “Дискретные модели в теории управляющих си­ стем” (Москва 2006, 2009); “Параллельные вычисления и задачи управления” (Москва 2008); “Компьютерные науки и технологии” (Белгород 2009); “Инфор­ мационные технологии в науке, образовании и производстве” (Орёл 2010); “Се­ мантика, спецификация и верификация программ: теория и приложения” (Ка­ зань 2010, Санкт–Петербург 2011, Н.Новгород 2012, Екатеринбург 2013); “Petri Net Compositions (Petri Nets 2011)” (Ньюкасл–на–Тайне 2011); “Petri Nets and Software Engineering (Petri Nets 2013)” (Милан 2013).

Публикации. Материалы диссертации опубликованы в 55 печатных рабо­ тах, из них 16 статей в изданиях, рекомендованных ВАК (8 статей в российских журналах из перечня ВАК [12, 18, 21, 22, 24, 25, 27, 31] и 8 статей в зару­ бежных изданиях, входящих в международные индексы цитирования из перечня ВАК [23, 34, 79–81, 86, 87, 89]), 10 статей в прочих рецензируемых журна­ лах [3, 4, 7, 10, 66, 68, 70, 73, 77, 85], 27 статей в сборниках трудов конференций и прочих сборниках [5, 8, 9, 11, 13, 14, 16, 17, 19, 20, 26, 28–30, 33, 67, 69, 71, 72, 74–76, 78, 82–84, 88], одна монография [32] и одно учебное пособие [15]).

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

Гранты.

Работа по теме диссертации поддерживалась следующими гран­ тами: РФФИ №№ 99-01-00-309-а, 03-01-00804-а, 06-01-00106-а, 07-01-07038-д, 07-01-00702-а, 09-01-00277-а, 09-0109370-моб_з, 11-01-00737-а, 11-07-00549-а, 12-01-00281-а, 12-01-31508-а; федеральная целевая программа “Научные и на­ учно-педагогические кадры инновационной России” (проекты 2009-1.1113-050-и 14.B37.21.0392).

Структура и объем. Работа состоит из введения, четырёх глав, заключения и списка литературы (209 пунктов). Общий объем работы 268 страниц, включая 92 рисунка.

1.1. Множества и отношения Через Z, Z и Z+ обозначим, соответственно, множества целых, отрица­ тельных целых и положительных целых чисел. Через Nat обозначим множество неотрицательных целых чисел.

Обозначение 1.1. Пусть X и Y — два множества. Будем использовать обозна­ чения:

X Y, если X является подмножеством Y;

X Y, если X является собственным подмножеством Y;

|X| — мощность множества X;

X Y — объединение множеств X и Y;

X Y — пересечение множеств X и Y;

X Y = {(x, y) | x X y Y} — декартово произведение множеств X и Y.

Определение 1.1. Пусть X и Y — некоторые множества. Отношение R между множествами X и Y — это подмножество множества X Y.

Будем говорить, что отношение R определено на множестве X, если R — это отношение между X и X.

Обозначение 1.2. Пусть X — некоторое множество, R — отношение, опреде­ ленное на X. Будем использовать обозначения:

Id(X) = {(x, x) | x X} — отношение идентичности на X;

R1 = {(y, x) | (x, y) R} — отношение, обратное R;

R1 R2 = {(x, y) | z : (x, z) R2 (z, y) R1 } — композиция отношений R Отношение R на множестве X есть отношение эквивалентности, если оно рефлексивно, симметрично и транзитивно.

Обозначение 1.3. Для стандартных отношений на X будем использовать сле­ дующие обозначения:

Rk, где k Nat, задается рекурсивным определением:

R+ = R1 R2... — транзитивное замыкание R;

R* = Id(X) R+ — рефлексивное транзитивное замыкание;

R — рефлексивно-симметрично-транзитивное замыкание R. Очевидно, что это — наименьшее отношение эквивалентности на X, содержащее R.

Определение 1.2. Пусть A — некоторое множество. Конечной последователь­ ностью на A будем называть отображение множества {1, 2,..., n} в A. Отоб­ ражение : A будем называть пустой последовательностью.

Пусть : 1,..., n A : a1... an — конечная последовательность, тогда ее длину n будем обозначать ||. Длина пустой последовательности равна 0.

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

1.1.1. Мультимножества Мультимножество является естественным обобщением множества. В муль­ тимножестве один объект может находиться в нескольких экземплярах.

Пусть X — непустое множество.

Определение 1.3. Мультимножеством M над множеством X называется функ­ ция M : X Nat.

Мощность мультимножества |M| = Числа {M(x) | x X} называются коэффициентами мультимножества, коэф­ фициент M(x) определяет число экземпляров элемента x в M. Если x X M(x) 1, то M является обычным множеством.

Мультимножество M конечно, если конечно множество Множество всех конечных мультимножеств над множеством X обозначается как (X).

Операции и отношения теории множеств естественным образом расширя­ ются на конечные мультимножества.

Определение 1.4. Пусть M1, M2, M3 (X). Полагаем:

M1 = M2 x X M1 (x) = M2 (x) — отношение равенства;

M1 M2 x X M1 (x) M2 (x) — отношение включения;

включения;

M1 = M2 + M3 x X M1 (x) = M2 (x) + M3 (x) — операция сложения двух мультимножеств;

M1 = M2 M3 x X M1 (x) = min(M2 (x), M3 (x)) — операция пересечения двух мультимножеств;

мультимножеств (где — вычитание до нуля);

мультимножества на скаляр.

Пример 1.1. Рассмотрим M1 и M2 — мультимножества над множеством X = {a, b, c}, такие, что M1 = {a, a, b}, M2 = {b, c}.

Выполняется:

Одним из способов записи мультимножеств являются вектора над Nat. При этом различным координатам вектора сопоставляются различные элементы X.

Пример 1.2. Мультимножества M1 и M2 из примера 1.1 могут быть записаны как Утверждение 1.1. Множество (X) мультимножеств над X изоморфно мно­ жеству Nat|X| векторов длины |X| с целочисленными неотрицательными коэф­ фициентами.

Доказательство:

Рассмотрим мультимножества, представленные в виде векторов.

Определение 1.5. Множество векторов m Natk называется линейным, если Определение 1.6. Множество называется полулинейным, если оно является объединением конечного числа линейных множеств.

Определим также операции сдвига множеств векторов:

Определение 1.7. Пусть M (X) и m (X). Полагаем:

Для полулинейных множеств M, M Natk и вектора m Natk множества Natk M, M M, M M, M m и M m также полулинейны [129]. Полули­ нейные множества — в точности все множества, выразимые при помощи формул арифметики Пресбургера ([182], см., например, [36]).

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

Пусть (M1, M2 ), (M1, M2 ) (X) (X) — пары мультимножеств над мно­ жеством X. Их сумма определяется как Пусть B (X) (X) — бинарное отношение на множестве мультимно­ жеств над X.

Определение 1.8. Для данного отношения B его аддитивным замыканием BA на­ зывается наименьшее (по вложению) подмножество множества (X) (X), такое, что Определение 1.9. Для данного отношения B его транзитивным замыканием BT называется наименьшее (по вложению) подмножество множества (X) (X), такое, что Определение 1.10. Для данного отношения B его аддитивным транзитивным замыканием BAT называется наименьшее (по вложению) подмножество мно­ жества (X) (X), такое, что В дальнейшем будем использовать сокращения A-замыкание, T -замыкание и AT -замыкание соответственно.

В случае отношений на мультимножествах AT -замыкание отношения не всегда совпадает с аддитивным замыканием транзитивного замыкания отноше­ ния и с транзитивным замыканием аддитивного замыкания отношения. Строго говоря, имеет место следующая вложенность друг в друга различных видов за­ мыканий отношений на мультимножествах (см. также рисунок 1.1):

Рис. 1.1. Вложенность различных видов замыканий Лемма 1.1. [6] 1. X, B (X)(X) выполняется (BA )T BAT ;

2. X, B (X)(X) выполняется (BT )A BAT ;

6. X, B (X)(X) : (BT )A Таким образом, AT -замыкание — наиболее эффективный (из представлен­ ных) способ построения бесконечных отношений (получаемые с его помощью бесконечные отношения самые слабые).

На практике в теории формальных моделей мы почти всегда имеем дело с транзитивно замкнутыми отношениями на множестве состояний исследуемой системы (или даже отношениями эквивалентности). Накладывая дополнитель­ ное требование аддитивной замкнутости, мы получаем возможность выделять некоторые “структурированные” подмножества базового отношения (возможно, представимые конечным базисом). Как показано в лемме 1.1, аддитивную за­ мкнутость можно вводить тремя различными способами.

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

Определение 1.11. Отношение B (X) (X) называется -базисом от­ ношения B, если (B ) = B.

Базис B называется минимальным -базисом отношения B, если не суще­ ствует B B, такого что (B ) = B.

Лемма 1.2. [6] 1. Все минимальные -базисы отношения B либо конечны, либо бесконечны.

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

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

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

Рассмотрим в качестве аддитивные и транзитивные замыкания. Оказы­ вается, даже если B — отношение эквивалентности, у него могут существовать бесконечные минимальные базисы.

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

Рассмотрим случай A-замыкания.

Пусть B = {(0, 0), (1, 1)} {(1, i + 2), (i + 2, 1) | i Nat}. Отношение B является A-базисом отношения BA. Докажем минимальность B. Предположим противное: пусть некоторая пара (x, y) B может быть получена аддитивным замыканием других пар из B. Однако при любом сложении мультимножеств видов (1, i + 2), (i + 2, 1) или (1, 1) (пустую пару можно не рассматривать) в итоговой паре оба коэффициента становятся больше единицы — противоречие.

Рассмотрим случай T -замыкания.

Пусть B = {(0, 0)} {(1, i + 2), (i + 2, 1) | i Nat}. Очевидно, что B является T -базисом отношения BT (любая пара вида (i, i) может быть получена тран­ зитивным замыканием двух симметричных пар). Докажем минимальность B.

Предположим противное: некая пара (x, y) B, где x y, может быть получена транзитивным замыканием других пар из B. Однако при любом транзитивном замыкании мультимножеств видов (1, i+2) и (i+2, 1) может получиться только рефлексивная пара — противоречие.

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

Рассмотрим в качестве аддитивное транзитивное замыкание.

Потребуется одно техническое определение:

Определение 1.12. Отношение R (X) (X) называется 1-рефлексивным, если R содержит все пары вида (x, x), где |x| = 1.

В случае аддитивных транзитивных замыканий вместо полной рефлексив­ ности отношения B достаточно требовать только 1-рефлексивности, так как ад­ дитивное замыкание 1-рефлексивного отношения рефлексивно (с точностью до пустой пары (, )). Использовать же полную рефлексивность неудобно чисто технически, так как рефлексивные отношения на мультимножествах бесконечны a priori.

Во-первых, заметим, что существуют симметричные отношения с бесконечными минимальными AT -базисами.

Пример 1.4. В качестве примера рассмотрим множество X из двух элементов и симметричное отношение (пары мультимножеств представлены как пары векторов длины 2).

Покажем, что базис B – минимальный. Пусть – первые k элементов базиса B. Нам достаточно показать, что (k+1)-й элемент не может быть выражен через предыдущие, то есть Заметим, что и в левой, и в правой части всех пар векторов из B второй коэффициент на единицу больше первого. При сложении любых двух пар в левой и правой части получатся вектора, где второй коэффициент больше первого на 2. Только при транзитивном замыкании таких пар разность коэффициентов не меняется. Однако, очевидно, что одним транзитивным замыканием пару ((k + 1, k + 2), (k + 1, k + 2)) из Bk не получить.

Во-вторых, существуют 1-рефлексивные отношения с бесконечными мини­ мальными AT -базисами.

Пример 1.5. В качестве примера рассмотрим множество X из двух элементов и 1-рефлексивное отношение (пары мультимножеств представлены как пары векторов длины 2).

Покажем, что базис B – минимальный. Пусть – первые k + 2 элементов базиса B. Достаточно показать, что (k + 3)-й элемент не может быть выражен через предыдущие, то есть Рассмотрим все нерефлексивные элементы отношения Bk. Они имеют вид ((1, 0), (i, 1)), где i 2. Первый коэффициент в правой части пары на i1 больше, чем первый коэффициент в левой. Второй коэффициент в правой части пары на 1 больше, чем второй коэффициент в левой.

Рассмотрим рефлексивные пары ((1, 0), (1, 0)) и ((0, 1), (0, 1)). В них левые и правые части совпадают.

Если сложить любые две нерефлексивные пары, то в полученной паре раз­ ность между вторым коэффициентом в правой и левой части увеличится и станет равной двум. При любом транзитивном замыкании эта разность умень­ шиться не сможет, поскольку в Bk во всех парах “правая” координата не мень­ ше “левой”. В то же время для построения пары ((1, 0), (k+1, 1)) нам необходимо по крайней мере одно суммирование нерефлексивных пар – чтобы увеличить на единицу разность по первому коэффициенту.

Итак, по отдельности симметричность и 1-рефлексивность не гарантируют существования конечного AT -базиса. Использование обоих ограничений1 при­ водит к полностью конечному случаю.

Определение 1.13. [6] Определим частичный порядок на множестве B (X) (X) пар мультимножеств:

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

для рефлексивных пар (кроме (, )) для нерефлексивных пар рефлексивная часть и нерефлексивный остаток срав­ ниваются отдельно Заметим, что рефлексивные и нерефлексивные пары отношения B не сравнимы Через Bs обозначим множество минимальных (относительно ) элементов BAT. В случае, когда (, ) B, к Bs также добавляется пара (, ).

Теорема 1.1. [6] Пусть отношение B симметрично и 1-рефлексивно. Тогда от­ ношение Bs является его базисом и Bs конечно.

Базис Bs называется основным базисом отношения B.

Из теоремы 1.1 и второго утверждения леммы 1.2 вытекает:

Теорема 1.2. [6] Если отношение B симметрично и 1-рефлексивно, то все его минимальные AT -базисы конечны.

Это утверждение (хотя и в несколько другой формулировке и в терминах конгруэнтностей в коммутативных полугруппах) было доказано Л.Редеи [185], а позднее (независимо) Й.Хиршфельдом [135]. В нашей работе [6] было использо­ вано новое, конструктивное доказательство, описывающее структуру элементов конечного базиса.

Приведем пример основного базиса.

Пример 1.6. Рассмотрим множество X из одного элемента и симметричное 1-рефлексивное отношение (пары мультимножеств представлены как пары чисел).

Основной базис — Bs = {(1, 1), (1, 2), (2, 1)}.

Основной базис отношения не всегда является минимальным. Например, в базисе из примера 1.6 избыточной является пара (1, 1), которая может быть получена транзитивным замыканием двух других пар. Однако важным достоин­ ством основного базиса является хорошая структурированность. К тому же он по определению единственнен для любого B, тогда как минимальных AT -базисов может существовать бесконечно много [6].

Другим важным достоинством основного базиса (кроме его конечности) является то, что при помощи процедуры разложения, использованной в дока­ зательстве теоремы 1.1, мы можем за конечное число шагов проверить при­ надлежность произвольной пары ресурсов замыканию BAT. В частности, в [6] представлен алгоритм трудоёмкости O(|X||Bs |2 ).

Отношение B может задаваться произвольным конечным базисом (не обя­ зательно минимальным и не обязательно основным). Однако любой конечный симметричный 1-рефлексивный базис можно преобразовать в основной базис при помощи эффективной процедуры — в [6] представлен алгоритм такой транс­ формации, имеющий трудоёмкость O(|X||B|4 ). Однако необходимо заметить, что на практике мощность B часто находится в экспоненциальной зависимости от мощности основного множества X.

1.2. Эквивалентность поведений Понятие эквивалентности поведений — важнейшее понятие теории фор­ мальных систем. Поведенческие эквивалентности позволяют сравнивать парал­ лельные и распределенные системы с учетом тех или иных аспектов их функ­ ционирования, а также абстрагироваться от излишней информации. Эквивалент­ ностные отношения используются также для сохраняющей поведение редукции систем и в процессе верификации, когда сравнивается ожидаемое и реальное поведения систем. Проблемы проверки эквивалентности поведений занимают важное место в теории автоматов и теории схем программ (см., например, рабо­ ты А. А. Летичевского, Р. И. Подловченко, В. А. Захарова и др. [39, 40, 42, 50– 52, 181, 209]).

1.2.1. Системы помеченных переходов Системы помеченных переходов — абстрактная низкоуровневая модель опи­ сания поведения дискретных систем.

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

Определение 1.14. Системой помеченных переходов (Labelled Transition System) называется набор LT S = (S, Act,, s0 ), где - S — множество состояний с элементами s0, s1, s2,... ;

- Act — некоторый алфавит ( множество имен действий);

- (S ActS ) — отношение переходов между состояниями (с пометками - s0 S — выделенное состояние, называемое начальным состоянием систе­ мы переходов.

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

Состояния, не имеющие последующих состояний называются финальными. Если некоторый переход переводит состояние s в состояние s, то пишем s s. Через Succ(s) будем обозначать множество последующих состояний для s, через Pred(s) — множество его предыдущих состояний. Мы рассматриваем только системы переходов с конечным ветвлением (finitely branching), то есть такие, в которых для любого s множество Succ(s) конечно.

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

Определение 1.15. Последовательное исполнение для LT S есть конечная или бесконечная цепочка переходов s0 s1 s2 · · ·, где s0 — начальное состо­ яние системы. Каждому исполнению LT S соответствует некоторая строка в алфавите Act, составленная из меток сработавших переходов, называемая распознанной строкой или трассой LT S.

Запись s s означает, что имеется конечная последовательность перехо­ дов, переводящая состояние s в состояние s.

Графически система переходов LT S изображается как помеченный ориен­ тированный граф, в котором вершинами являются элементы множества состоя­ ний S, а дуги определяются отношением переходов так, что дуга, помеченная a, соединяет вершину s с вершиной s в том и только том случае, когда s s.

Каждому последовательному исполнению в LT S соответствует ориентиро­ ванный путь с началом в вершине s0 в графе LT S.

Одним из важнейших инструментов анализа динамики функционирования систем переходов является эквивалентность языков (трасс) [146].

Определение 1.16. Языком системы помеченных переходов LT S (языком, рас­ познаваемым системой LT S ) называется множество строк из алфавита Act, соответствующих всем последовательным исполнениям для LT S.

Языковая эквивалентность учитывает так называемую интерливинговую (последовательную) операционную семантику. Другими словами, анализируются “моментальные проекции” поведения системы, представляющие строки в неко­ тором алфавите, без учета ветвлений.

Пример 1.7. Рассмотрим системы переходов, изображенные на рисунке 1.3.

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

В первом автомате клиент сначала опускает монету (действие “монета” — получение автоматом монеты), а затем выбирает либо кофе, либо чай — автомат отвечает действиями “кофе” или “чай” соответственно. Во вто­ ром автомате выбор кофе/чай происходит уже в самом начале, до опускания монеты. Далее от клиента уже ничего не зависит — автомат отрабатывает либо программу “монета кофе”, либо “монета чай”, не задавая дополнительных вопросов.

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

В то же время очевидно, что системы все-таки существенно различны. Если в первой после срабатывания “монета” можно выбрать и “чай”, и “кофе”, то во второй реальный выбор уже произошел, и изменить что-либо клиент уже не в состоянии.

Операционная семантика, учитывающая ветвления, называется семантикой ветвящегося времени (branching time). Если в последовательной семантике си­ стема полностью описывается распознаваемым языком (множеством трасс), то в семантике ветвящегося времени рассматривается полный граф срабатываний.

Для анализа динамики функционирования систем в семантике ветвящегося времени используется понятие бисимуляций.

1.2.2. Бисимуляции Бисимуляционная эквивалентность [171, 176] — фундаментальное понятие в теории параллельных и распределенных систем. Бисимуляция обладает четкой математической трактовкой и более тонко отслеживает ветвления в дереве сра­ батываний системы по сравнению с языковой эквивалентностью. Два состояния системы бисимулярны (симулируют друг друга), если внешний наблюдатель по наблюдаемому поведению системы не может определить, с какого из этих двух состояний она начала работу.

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

Бисимуляцию определяют с помощью так называемого свойства переноса:

Определение 1.17. Пусть R S S — отношение на множестве состояний системы помеченных переходов. Отношение R обладает свойством переноса, если для любой пары (s, t) R и любого перехода s s найдется имитирующий переход t t, такой что (s, t ) R.

Свойство переноса можно проиллюстрировать диаграммой:

Определение 1.18. Отношение R S S на множестве состояний системы помеченных переходов называется отношением бисимуляции, если R и R1 обла­ дают свойством переноса.

Простейшими примерами бисимуляций являются отношение идентичности Id(S ) и пустое отношение.

Определение 1.19. Состояния s и t системы помеченных переходов называются бисимуляционно эквивалентными (или бисимулярными), что обозначается как s t, если существует отношение бисимуляции R, такое, что (s, t) R.

Пример бисимулярных состояний приведен на рисунке 1.4. У изображенной системы помеченных переходов бисимулярны состояния s и s, а также t, t и t.

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

В качестве “игровой доски” берется система помеченных переходов, в кото­ рой выделяются два состояния — E0 и F0 (в этом случае для игры используется обозначение G(E0, F0 )). В игре участвуют два игрока, Алиса (подразумевается “Attacker”) и Боб (“Bisimulator”), которые являются наблюдателями, выбираю­ щими переходы системы. Алиса стремится доказать, что состояния E0 и F0 в некотором смысле “различны”, Боб — что они в том же самом смысле “эквива­ лентны”. Результатом игры является конечная или бесконечная последователь­ ность вида причем каждая следующая пара последовательности получена из предыдущей по правилу:

1. Алиса выбирает срабатывание (дугу в графе LT S ) Ei Ei+1 или Fi Fi+1.

2. Боб выбирает некоторое имитирующее срабатывание Fi Fi+1 или Ei Ei+1 (обязательно с той же меткой a, что и у срабатывания, выбранного Алисой).

Алиса выигрывает игру, если на некотором ходе Боб не может ответить на ее ход своим (имитирующих переходов не осталось); у Боба два варианта выигрыша:

1. Алиса попала в тупик и не может сделать ни одного хода (из вершин Ei и Fi не ведет ни одной дуги).

2. Игра бесконечна, то есть последовательность ходов не закончилась ни по­ бедой Алисы, ни первым вариантом победы Боба.

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

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

Определение 1.20. Состояния E0 и F0 называются бисимулярными, если у Боба существует выигрывающая стратегия для игры G(E0, F0 ).

Пример 1.8. Рассмотрим игру G(s, s ) в системе переходов, изображенной на рисунке 1.4. У Боба существует очевидная выигрывающая стратегия — отве­ чать на ходы Алисы ходами с той же меткой срабатывания. В состояниях s и s возможны срабатывания с метками a и b (причем только по одному на каждую метку!), в состояниях t, t и t — только единственное срабатывание с меткой c. Кроме того, как легко заметить, при любом последовательном исполнений состояния видов s* и t* чередуются.

Утверждение 1.2. Определения бисимулярности 1.19 и 1.20 эквивалентны.

Основные свойства бисимуляции:

Утверждение 1.3. Пусть R, R1, R2 S S — отношения бисимуляции на мно­ жестве состояний системы помеченных переходов. Тогда:

1. Отношение Id(S ) есть бисимуляция.

2. Отношение R1 есть бисимуляция.

3. Отношение R1 R2 есть бисимуляция.

4. Отношение R есть бисимуляция.

5. Отношение R2 R1 есть бисимуляция.

6. Отношение =de f бисимуляция на множестве S (относительно вложения).

7. Отношение является отношением эквивалентности на множестве S.

Доказательство:

бисимуляции.

Свойство 5: Покажем, что R2 R1 обладает свойством переноса, и, следова­ тельно, является бисимуляцией.

Пусть (s1, s3 ) R2 R1, тогда существует состояние s2 такое, что выполняется Рассмотрим шаг s1 s. Тогда существует шаг s2 s, такой что (s, s ) R1, и, следовательно, существует шаг s2 s, такой что (s, s ) R2, то есть (s, s ) R2 R1. Аналогично можно показать, что отношение R2 R1 обладает свойством переноса в обратном направлении. Таким образом, R2 R1 — бисиму­ ляция.

Свойство 4: Поскольку свойства 2 и 3 могут быть обобщены для объедине­ ния (композиции) бесконечного числа множеств, а то очевидно, что R — бисимуляция.

Свойство 6 является очевидным следствием свойства 3, а свойство 7 — следствием свойств 3 и 4.

Бисимуляция — достаточно тонкая эквивалентность на множестве состоя­ ний, адекватно отражающая свойства системы в семантике ветвящегося времени.

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

Бисимуляционная эквивалентность изучалась для различных классов фор­ мальных моделей [56, 63, 105, 136, 139–142, 145, 173, 194, 196]. Был получен ряд результатов по ее разрешимости. В частности, бисимуляция разрешима для всех классов систем с конечным числом состояний (конечных автоматов), так как в них для проверки бисимулярности достаточно просто перебрать множе­ ство состояний. Бисимуляция разрешима также для таких классов моделей с бесконечным множеством состояний, как:

- базовые параллельные процессы (BPP, Basic Parallel Processes) [105, 106, - базовые алгебры процессов (BPA, Basic Process Algebra) [63, 107], - нормированные алгебры процессов (normed PA, normed Process Algebra) - автоматы с одним счетчиком (one-counter machines) [141], - нормированные магазинные автоматы (normed PDA, normed Pushdown Automata) [194].

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

- автоматы мультимножеств (MSA, Multiset Automata) [173], - помеченные сети Петри (labelled PN, labelled Petri Nets) [140], - универсальные модели (машины Минского, машины Тьюринга, сети Петри с ингибиторными дугами,... ).

Важным примером расширения бисимуляции является так называемая рас­ слоенная (stratified) бисимуляция [145] (обозначается n ). Она определяется ин­ дуктивно:

Во-первых, полагаем s1 0 s2 для любых s1, s2 S. Далее, для любого n Nat полагаем s1 n+1 s2, если для любого a Act :

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

Все последующее поведение сети просто игнорируется.

Известно, что для любого n отношение n является эквивалентностью, кро­ ме того, (n+1 ) (n ). Также выполняется s1 s2 s1 n s2 для любого n Nat.

Наибольшая бисимуляция является пределом последовательности расслоенных бисимуляций: () = ( ).

Известно [145], что проблема n-расслоенной бисимулярности разрешима для любого n.

1.3. Сети Петри Определение 1.21. Обыкновенной сетью Петри (ordinary Petri Net) называется набор N = (P, T, F), где P — конечное множество позиций;

T — конечное множество переходов, P T = ;

F : (P T ) (T P) Nat — функция инцидентности.

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

Определение 1.22. Пусть N = (P, T, F) — обыкновенная сеть Петри. Разметкой (состоянием) сети N называется функция вида M : P Nat, сопоставляющая каждой позиции сети некоторое натуральное число или ноль.

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

Графически разметка изображается при помощи маркеров (называемых “фишками”) — черных точек внутри позиций. При разметке M в каждую по­ зицию p помещается ровно M(p) фишек. Если не хватает места на рисунке, то вместо точек рисуется число M(p).

Определение 1.23. Маркированной (размеченной) сетью Петри называется па­ ра (N, M0 ) — сеть Петри N вместе с некоторой выделенной разметкой M0, называемой начальной разметкой.

Рис. 1.5. Сеть Петри, моделирующая химическую реакцию Определим поведение сети Петри.

Определение 1.24. Пусть N = (P, T, F) — обыкновенная сеть Петри.

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

Готовый к срабатыванию переход t может сработать, порождая новую разметку M =de f M t + t (используется обозначение M M ).

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

Определение 1.25. Пусть (N, M0 ) — маркированная сеть Петри. Разметка M сети N называется достижимой, если существует последовательность перехо­ дов T *, переводящая сеть из начального состояния M0 в состояние M:

что обозначается как M0 M или просто как M0 M.

Множество всех достижимых разметок сети обозначается как (N, M0 ) Определение 1.26. Пусть (N, M0 ) — маркированная сеть Петри. Позиция p P называется ограниченной, если n Nat, такое, что M (N, M0 ) выполня­ ется M(p) n.

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

На рисунках 1.6–1.8 приведены примеры того, как при помощи обыкновен­ ных сетей Петри можно моделировать некоторые элементы реальных систем.

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

Сеть 1.7 моделирует систему разделения доступа для двух различных про­ цессов к общей ячейке памяти [177]. Чтобы исключить одновременный доступ процессов к памяти (чтение и запись в данном случае не различаются), использо­ вано классическое семафорное решение. Имеется один общий ключ (моделиру­ ется фишкой в позиции ключ), который дает право на доступ. Пока работающий процесс не вернул его на место, ожидающий процесс не может перейти в рабочее состояние. В начальном состоянии оба процесса находятся в стадии ожидания доступа.

На рисунке 1.8 показан элемент памяти FIFO (очередь), состоящий из двух ячеек (позиции 1 и 2). Позиция 1 моделирует первую ячейку FIFO (куда посту­ пают данные), позиция 2 — последнюю (откуда они забираются). В начальном состоянии системы обе ячейки свободны, на входе имеются три фишки “дан­ ных”.

Рис. 1.7. Семафор (разделенный доступ к памяти)

E E E E E E E

Для анализа поведения систем, моделируемых сетями Петри, необходимо формально сопоставить реальные объекты (действия) элементам модели. Сраба­ тывания переходов в сети Петри соответствуют различным наблюдаемым собы­ тиям в моделируемой системе. Чтобы идентифицировать их, переходы помеча­ ются метками из Act.

Определение 1.27. Помеченной сетью Петри называется набор N = (P, T, F, l), где (P, T, F) — сеть Петри, l : T Act — помечающая функция.

Внешний наблюдатель видит не сам переход t, а метку срабатывания l(t), которой он помечен. Если два перехода помечены одной и той же меткой, то их срабатывания считаются идентичными. Таким образом, внешний наблюдатель рассматривает систему как “черный ящих”, порождающий те или иные события.

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

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

Определение 1.28. Пусть N = (P, T, F, l) — помеченная сеть Петри. Скажем, что отношение R (P) (P) обладает свойством переноса, если для любой пары разметок (M1, M2 ) R и для любого перехода t T, такого что M1 M1, найдется имитирующий переход u T, такой что l(t) = l(u), M2 M2 и (M1, M2 ) R.

Свойство переноса может быть проиллюстрировано при помощи следую­ щей диаграммы:

Определение 1.29. Если отношения R и R1 обладают свойством переноса, то R называется бисимуляцией разметок.

На рисунке 1.9 приведен пример бисимулярных разметок в сети Петри.

Выполняется (1, 0, 0) (0, 1, 1) (разметки записаны как вектора длины 3).

Бисимуляции разметок в сетях Петри по определению обладают всеми свой­ ствами общего определения бисимуляции для LT S (так как сети Петри есть частный случай LT S ).

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

1. Ограниченные сети Петри (так как они совпадают с классом конечных автоматов).

2. Сети Петри с одной неограниченной позицией.

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

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

В 1994 году П.Жанкар доказал [140, 145], что в общем случае бисимуляция разметок в сетях Петри неразрешима. Более того, бисимуляция неразрешима да­ же для сетей с двумя неограниченными позициями. Это весьма существенное ограничение, не позволяющее использовать бисимуляцию разметок при изуче­ нии свойств достаточно широких классов систем с бесконечным числом состо­ яний. Необходимо искать более сильные эквивалентности, лучше поддающиеся алгоритмическому анализу.

Примером таких отношений могут служить введенные Ф. Шнобеленом, С. Аутоном и Н. С. Сидоровой отношения бисимуляции позиций и корректного слияния позиций [53, 61, 62, 190]. В диссертации [6] нами было введено и исследовано промежуточное по силе между бисимуляцией разметок и слиянием позиций отношение подобия ресурсов.

1.4. Ресурсы в сетях Петри В данном разделе представлено ключевое понятие ресурса сети Петри. При­ водятся некоторые результаты из [6], касающиеся свойств отношений эквива­ лентности ресурсов, в частности, подобия ресурсов и бисимуляции ресурсов.

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

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

1.4.1. Подобие ресурсов Определение 1.30. Пусть N = (P, T, F) — обыкновенная сеть Петри. Ресурсом сети N называется мультимножество над множеством позиций P.

Формально определение ресурса не отличается от определения разметки.

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

В данном определении ресурс рассматривается не как “подмножество дан­ ной разметки”, а как “общая часть всех разметок, содержащих данное (муль­ ти)множество фишек”. Суть различий наиболее ярко проявляется в определении подобных ресурсов:

Определение 1.31. Пусть N = (P, T, F, l) — помеченная сеть Петри. Ресурсы r и s называются подобными (обозначается r s), если для любой разметки R, такой, что r R, выполняется Отношением подобия ресурсов сети Петри N называется максимальное по вложению отношение на множестве ресурсов (P), такое, что любые два связанных им ресурса подобны (обозначается ).

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

Заметим, что для сети Петри, представляющей реакцию синтеза воды (рис.

1.5), одна молекула кислорода эквивалентна одной молекуле водорода с точки зрения бисимулярности разметок, так как и в том и в другом случае переход сети не сработает. Однако подобными ресурсами указанные две молекулы не являются.

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

Рассмотрим модель подобной ситуации, изображенную на рисунке 1.10.

Покупается товар стоимостью 20 копеек. Позиция “магазин” моделирует коли­ чество товара в магазине, “куплено” — количество уже купленного товара, “10к” и “5к” — количество неизрасходованных монет. Покупка возможна тремя спо­ собами — переходы t1, t2 и t3. Во всех трех случаях тратится различное число различных монет.

В такой ситуации использование пятикопеечных монет избыточно, что и отражается в подобии ресурсов “10к”“5к”+“5к”.

Примеры подобных ресурсов приведены на рисунке 1.11.

Рис. 1.10. Модель покупки товара с использованием двух видов монет На рисунке а) изображена сеть Петри, содержащая два перехода, помечен­ ных одинаковой меткой a и приводящих к одинаковой разметке p3. Здесь подоб­ ны ресурсы p1 и p2, так как они приводят к полностью идентичному поведению сети — срабатыванию перехода с меткой a с помещением фишки в позицию p3. Более того, подобны все ресурсы, содержащие одинаковое число фишек в позициях p1 и p2.

На рисунке б) изображена простейшая сеть, состоящая из одного перехода.

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

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

а) параллельные срабатывания в) циклические срабатывания B г) ресурсы различной мощности Рис. 1.12. Подобие ресурсов не совпадает с бисимуляцией разметок На рисунке г) изображена более сложная сеть. Выполняется p1 p2 + p3, то есть замена одной фишки в позиции p1 на две фишки — одну в позиции p2 и еще одну в позиции p2 никак не влияет на наблюдаемое поведение сети в целом.

1.4.2. Свойства подобия ресурсов Утверждение 1.4. [6] Пусть N = (P, T, F, l) — помеченная сеть Петри, r, s — ресурсы сети N (которые также могут рассматриваться как разметки сети N). Тогда Другими словами, () (), то есть подобие ресурсов является сужением максимальной бисимуляции разметок.

качестве контрпримера рассмотрим сеть, изображенную на рисунке 1.12.

В данной сети p1 p2, так как при этих разметках может сработать только сработать переход t3, помеченный b).

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

Подобие ресурсов рефлексивно, симметрично, транзитивно и замкнуто от­ носительно сложения:

Лемма 1.3. [6] Пусть N = (P, T, F, l) — помеченная сеть Петри, r, s, u, v — ре­ сурсы сети N. Тогда Таким образом, подобие ресурсов обладает всеми свойствами AT -замыкания некоторого отношения (другими словами, отношения и ()AT совпадают).

Например, из подобия ресурсов r s немедленно следует подобие ресурсов 2r 2s, 2r+s r+2s, 5r 3r+2s и так далее, что может быть описано формулой Из подобия ресурсов r 2r немедленно следует подобие ресурсов:

То есть любая пара подобных ресурсов может рассматриваться в качестве базиса для некоторого бесконечного отношения. С другой стороны, всё отноше­ ние подобия ресурсов также обладает конечным базисом:

Теорема 1.3. [6] Подобие ресурсов в помеченных сетях Петри обладает конеч­ ным AT -базисом.

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

В то же время в некоторых сетях бисимуляция разметок также может обла­ дать конечным базисом:

Рис. 1.13. Пример сети Петри, в которой подобие ресурсов и бисимуляция разметок совпадают Пример 1.9. На рисунке 1.13 изображена сеть Петри, представляющая собой цикл, состоящий из двух позиций и двух переходов, помеченных одним и тем же символом a.

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

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

Это же отношение является подобием ресурсов данной сети:

Подобие ресурсов задается следующим основным базисом:

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

Рис. 1.14. Пример сети Петри, в которой существует АТ-замкнутое сужение бисимуляции разме­ ток, не входящее в подобие ресурсов Заметим также, что подобие ресурсов не является наибольшим по вложению AT-замкнутым сужением бисимуляции разметок:

Пример 1.10. На рисунке 1.14 изображена сеть Петри, состоящая из трех по­ зиций и четырех переходов. Бисимуляция разметок этой сети содержит пары вида kp1 lp3, где k, l > 0. Действительно, при любой из разметок вида kp или lp3 могут сработать только переходы, помеченные a (сколь угодно много раз). Множество всех таких пар замкнуто относительно сложения и относи­ тельно транзитивности. С другой стороны, очевидно, что ни одна из них не принадлежит подобию ресурсов, так как kp1 + p2 lp3 + p2.

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

Теорема 1.4. [6] Проблема распознавания подобия ресурсов в сети Петри нераз­ решима.

Таким образом, даже несмотря на существование конечного базиса, подобие ресурсов не может быть эффективно построено.

Рис. 1.15. Отношение B1 — не бисимуляция ресурсов, отношение B2 — бисимуляция ресурсов 1.4.3. Бисимуляция ресурсов В работах Ф. Шнобелена и др. ([61, 62]) при определении вычислимых со­ храняющих бисимулярность отношений на множестве позиций сети Петри был использован способ замыкания отношения относительно срабатываний перехо­ дов. Отношение на множестве разметок замкнуто относительно срабатываний переходов, если оно является бисимуляцией разметок.

В диссертации [6] аналогичный подход был применён для случая ресурсов.

Определение 1.32. Пусть N = (P, T, F, l) — помеченная сеть Петри. Симмет­ ричное 1-рефлексивное отношение B (P) (P) называется бисимуляцией ресурсов сети N, если BAT есть бисимуляция разметок сети N.

Теорема 1.5. [6] Пусть N = (P, T, F, l) — помеченная сеть Петри, B (P) (P) — бисимуляция ресурсов сети N и (r, s) B. Тогда r s.

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

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

Пример 1.11. Рассмотрим сеть, изображенную на рисунке 1.15. Отношение B1 является подмножеством подобия ресурсов, однако оно не замкнуто отно­ сительно срабатывания переходов.

Рассмотрим пару разметок (p1, p3 ) (B1 )AT. Срабатывание p1 q1 мо­ жет быть имитировано при разметке p3 только срабатыванием перехода t3 : p3 q2. Однако пара (q1, q2 ) не принадлежит отношению (B1 )AT. Сле­ довательно, (B1 )AT не является бисимуляцией разметок, и B1 не является биси­ муляцией ресурсов.

Дополним отношение B1 парами (q1, q2 ) и (q2, q1 ). Полученное отношение B2 является отношением бисимуляции ресурсов, так как (B2 )AT является бииму­ ляцией разметок.

Заметим, что отношение B2 всё ещё не содержит всех пар подобных ресурсов (например, оно не содержит пару p1 p2 ).

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

Следующая теорема описывает основные свойства бисимуляции ресурсов.

Теорема 1.6. [6] Пусть N = (P, T, F, l) — помеченная сеть Петри. Тогда 1. если B1, B2 (P) (P) — бисимуляции ресурсов, то B1 B2 — бисиму­ ляция ресурсов;

2. для сети N существует максимальная по вложению бисимуляция ресурсов (обозначается как );

3. () является отношением эквивалентности.

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

Взаимная вложенность максимальной бисимуляции разметок, подобия ре­ сурсов и максимальной бисимуляции ресурсов изображена на рисунке 1.16.

Сплошной линией обозначены отношения, обладающие конечным AT -базисом (в силу своей аддитивной и транзитивной замкнутости).

Как и любая бисимуляция разметок, АТ-замыкание бисимуляции ресурсов обладает свойством переноса. Однако хорошая структурированность бисимуля­ ции ресурсов (по сравнению с произвольной бисимуляцией разметок) позволяет использовать и более слабый (локальный) вариант свойства переноса — когда для перехода t рассматриваются только те разметки, при которых он может сработать.

Определение 1.33. Отношение B (P) (P) обладает слабым свойством переноса, если для всех (r, s) B, t T, таких что t r, найдется имитиру­ ющий переход u T, такой что l(t) = l(u) и, обозначив M1 = t r и M2 = t r + s, Слабое свойство переноса может быть представлено в виде следующей диаграммы:

Поясним данную диаграмму. Пусть имеются ресурсы r и s, связанные отно­ шением B. Ресурс r при этом пересекается с предусловием перехода t. Обозначим результат срабатывания перехода t как M1 :

Заменив в разметке t r ресурс r на ресурс s, получим новую разметку t r + s.

Слабое свойство переноса состоит в том, что обязательно найдется переход u с той же меткой l(t), который может сработать от разметки t r + s :

причём результат его срабатывания (разметка M2 ) будет связан с разметкой M отношением BAT.

Теорема 1.7. [6] Симметричное и 1-рефлексивное отношение B (P) (P) обладает слабым свойством переноса тогда и только тогда, когда B — биси­ муляция ресурсов.

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

В [6] приводится алгоритм, определяющий, является или нет данное ко­ нечное отношение на множестве ресурсов данной сети Петри бисимуляцией ресурсов, и имеющий временную сложность O(max{|P||B|4, |T |2 |P||Bs |3 }), где Bs — простой базис отношения B.

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

Одним из вариантов приближенного решения является построение аппрок­ симации максимальной бисимуляции ресурсов данной сети. Если рассматривать не все множество ресурсов сети (по определению бесконечное), а только его ко­ нечное подмножество (например, только ресурсы, чья мощность не превышает заданный параметр), то конечным становится и число пар в рассматриваемых от­ ношениях, и мы можем использовать проверку слабого свойства переноса. В [6] приводится такой алгоритм аппроксимации.

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

Гипотеза 1.1. Для любой помеченной сети Петри N выполняется () = (), то есть максимальная бисимуляция ресурсов совпадает с подобием ресурсов.

Таким образом, в соответствие с этой гипотезой на диаграмме, изображен­ ной на рисунке 1.16, множества () и () должны совпадать. Контрпримером являлась бы пара подобных ресурсов, не принадлежащих максимальной биси­ муляции ресурсов.

Заметим также, что, если приведённая гипотеза верна, то, во-первых, биси­ муляция ресурсов в сетях Петри неразрешима (так как подобие ресурсов нераз­ решимо по следствию 1.4), и, во-вторых, описанный в [6] способ приближения максимальной бисимуляции ресурсов (при помощи параметризованной аппрок­ симации) — единственно возможный. Другими словами, имея некоторое отноше­ ние B (P)(P), мы можем сказать, является ли это отношение бисимуляци­ ей ресурсов, но не можем сказать, является ли оно максимальной бисимуляцией ресурсов.

1.4.4. Условное подобие ресурсов Расмотрим еще один способ определения корректного с точки зрения би­ симулярности отношения на (P). При этом способе мы выделяем некоторую разметку (начальное условие) и рассматриваем все возможные пары ресурсов, которые одинаково влияют на поведение сети при условии наличия данного на­ чального ресурса.

Определение 1.34. Пусть r, s, b (P). Ресурсы r и s называются подобными при условии b (обозначается r |b s), если для любого ресурса m (P), такого, что b m, выполняется m + r m + s.

Ресурсы r и s называются условно подобными (обозначается r | s), если существует ресурс b (P), такой, что r |b s.

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

Рассмотрим сеть, изображенную на рисунке 1.17(а). Ресурсы p1 и p2 не подобны, так как при разметке p1 ни один из переходов не может сработать, тогда как при разметке p2 может сработать переход a. С другой стороны, они подобны при условии q, то есть при наличии в сети ресурса q ресурсы p1 и p полностью взаимозаменяемы.

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

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

Следующее утверждение устанавливает некоторые важные свойства условного подобия ресурсов:

Утверждение 1.5. [6] Пусть r, s, b, b, m, m (P). Тогда Итак, условное подобие ресурсов замкнуто относительно сложения. Кроме того, оно инвариантно относительно расширения условия. Утверждения 1.5.4 и 1.5.5 показывают, что общая часть может быть удалена из подобных ресурсов.

Утверждения 1.5.6 и 1.5.7 показывают, что разность как пар подобных, так и пар условно подобных ресурсов является парой условно подобных ресурсов. Кроме того, условное подобие ресурсов замкнуто относительно сложения ресурсов и объединения условий (утверждение 1.5.8).

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

Следующее утверждение устанавливает связь между подобием ресурсов и условным подобием ресурсов:

Утверждение 1.6. [6] Пусть r, s, m, m (P), m m. Тогда Определение 1.35. Пусть r, s, r, s, r, s (P). Пара условно подобных ре­ сурсов r | s называется минимальной, если ее нельзя представить как сумму двух других пар условно подобных ресурсов, то есть для любой непустой пары Достаточно очевидным следствием утверждения 1.5.7 является:

Теорема 1.8. [6] Любая пара условно подобных ресурсов может быть пред­ ставлена в виде суммы минимальных пар условно подобных ресурсов.

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

Определение 1.36. Пара подобных ресурсов r s называется минимальной, если ее нельзя представить как сумму непустой пары подобных ресурсов и пары условно подобных ресурсов, то есть для любой непустой пары подобных ресурсов Теорема 1.9. [6] Любая пара подобных ресурсов может быть представлена в виде суммы одной минимальной пары подобных ресурсов и нескольких минималь­ ных пар условно подобных ресурсов.

Заметим, что по свойству покоординатного сравнения векторов с целочис­ ленными неотрицательными компонентами, для любой пары условно подобных ресурсов r | s множество ее минимальных условий (относительно покоорди­ натного сравнения) конечно.

Обозначение 1.4. Пусть R (P)(P) — некоторое подмножество множе­ ства пар условно подобных ресурсов (r | s для всех (r, s) R). Пусть — множество всех общих условий для R. Через Cond(R) обозначим множе­ ство минимальных элементов B (относительно покоординатного сравнения, рассматривая элементы B как вектора длины 2|P|).

Заметим, что из утверждения 1.6 следует, что для любой пары (u, v) Cond(R) оба ресурса u и v являются условиями для любой пары (r, s) R. Кро­ ме того, в силу свойства покоординатного сравнения векторов, для любого R множество Cond(R) конечно.

Обозначение 1.5. Пусть u, v (P) и u v. Через S (u, v) обозначим множе­ ство всех потенциальных дополнений к паре (u, v) (корректных относительно подобия ресурсов):

Через S min (u, v) обозначим множество всех минимальных относительно покоор­ динатного сравнения элементов множества S (u, v).

Утверждение 1.7. [6] Пусть u, v, u, v (P) и u v. Тогда 1) S (u, v) является отношением эквивалентности;

2) S (u, v) замкнуто относительно сложения;

4) S min (u, v) конечно.

Из первой и второй части утверждения следует, что множество S (u, v) об­ ладает конечным AT-базисом. В частности, согласно теореме 1.1, оно обладает основным базисом, составленным из минимальных относительно элементов.

Обозначение 1.6. Пусть N — помеченная сеть Петри. Через A(N) обозначим множество всех множеств потенциальных дополнений в N:

Утверждение 1.8. [6] Множество A(N) конечно для любой сети N.

Следующая теорема демонстрирует взаимосвязь между обычным подобием ресурсов и условным подобием ресурсов:

Теорема 1.10. [6] Пусть N — помеченная сеть Петри, () — множество всех пар подобных ресурсов в N, (| ) — множество всех пар условно подобных ре­ сурсов в N. Тогда множество () — полулинейно, причём существует конечное множество R (| ), такое, что где 2R — множество всех подмножеств множества R, lc(Z) — множество всех линейных комбинаций над Z.

Подобие ресурсов представимо при помощи некоторого конечного набо­ ра пар условно подобных ресурсов (причем в виде полулинейного множества).

Может возникнуть вопрос: нельзя ли использовать только минимальные условно подобные ресурсы в этом разложении? Действительно, это было бы гораздо удоб­ нее. Однако, к сожалению, это невозможно. Только лишь минимальные условно подобные ресурсы не отражают всей структуры подобия ресурсов.

Рассмотрим в качестве примера сеть Петри, изображенную на рисунке 1.18.

Минимальной парой условно подобных ресурсов для данной сети является пара 0 |2 1. Одна фишка подобна любому числу фишек при условии наличия как минимум двух других фишек в единственной позиции сети. Однако существует и другая (не минимальная) условно подобная пара 1 |1 2 с меньшим минимальным условием — только одной фишкой.

На рисунке 1.19 представлен другой пример, показывающий, что сумма ми­ нимальных условно подобных пар может иметь меньшее минимальное условие, чем слагаемые. Пары m1 |b1 m и m2 |b2 m являются минимальными пара­ ми условно подобных ресурсов, но пара m1 + m2 m + m обладает пустым условием!

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

Итак, условное подобие сильно взаимосвязано с обычным подобием ресур­ сов. Это влияет на разрешимость:

Теорема 1.11. [6] Проблема распознавания условного подобия ресурсов нераз­ решима для сетей Петри, то есть невозможно построить алгоритм, отвеча­ ющий на вопрос, являются ли данные ресурсы подобными при данном условии в данной сети Петри.

Как и подобие ресурсов, условное подобие ресурсов в общем случае не может быть эффективно построено.

1.4.5. Редукция (оптимизация) модели Подобие ресурсов может использоваться для редукции сети Петри, то есть сокращения ее размера при сохранении наблюдаемого поведения (в смысле би­ симулярности разметок). В частности, такая редукция представляет собой до­ статочно мощное средство оптимизации сложных (в том числе распределенных) процессов и систем [61]. Спектр сходных задач весьма широк: от реинжиниринга бизнес-процессов до оптимизирующей компиляции параллельных программ.

Для определения эквивалентности поведения сетей различной структуры нам потребуется понятие бисимуляции разметок между двумя сетями Петри:

Определение 1.37. Пусть N1 = (P1, T 1, F1, l1 ) и N2 = (P2, T 2, F2, l2 )— помеченные сети Петри. Отношение R (P1 )(P2 ) обладает свойством переноса, если для любой пары разметок (M1, M2 ) R и для любого перехода t T 1, такого, что в сети N1 существует срабатывание M1 M1, найдется имитирующий переход u T 2, такой, что l1 (t) = l2 (u) и в сети N2 существует срабатывание M2 M2, где (M1, M2 ) R.

Если отношения R и R1 обладают свойством переноса, то R называется бисимуляцией разметок между N1 и N2.

Маркированные сети Петри (N1, M1 ) и (N2, M2 ), такие, что существует отношение бисимуляции R, для которого (M1, M2 ) R, называются бисимуляр­ ными (обозначается (N1, M1 ) (N2, M2 )).

Известно, что для любых сетей Петри N1 и N2 существует максимальная бисимуляция разметок между ними, обозначаемая как [N1,N2 ].

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

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

Заметим, что всякому подобию ресурсов (мультимножеств позиций) можно сопоставить “подобие” выходных дуг переходов. Другими словами, если сра­ батывание перехода t помещает в его выходные позиции некоторый ресурс r, у которого есть подобный ресурс s, то мы можем заменить у перехода t все выходные дуги, соответствующие r, на выходные дуги, соответствующие s, и наблюдаемое поведение полученной сети ничем не будет отличаться от поведе­ ния исходной (в смысле бисимулярности).

Утверждение 1.9. [6](замена “подобных” выходных дуг) Пусть N = (P, T, F, l) — помеченная сеть Петри; r, s (P) — ресурсы сети N, такие, что r s; t T — переход, такой, что r t. Пусть N = (P, T, F, l) — помеченная сеть Петри, Рис. 1.20. Редукция заменой “подобных” выходных дуг. Для сети N выполняется p1, 2p2 p2.

Соответствующие этим ресурсам дуги заменены у переходов t1 и t2.

такая, что p P F (t, p) = F(t, p) r(p) + s(p). Тогда для любой M (P) выполняется (N, M) (N, M).

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

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

Рассмотрим редукцию сети Петри N, изображенной на рисунке 1.20. Сеть N получена из исходной сети N при помощи следующих замен “подобных” дуг:

1. p1. Дуга (t1, p1 ) заменена на (t1, ) (то есть удалена).

2. 2p2 p2. Две дуги (t2, p2 ) заменены на одну такую же.

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

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

Во-первых, заметим, что в случае входных дуг необходимо учитывать на­ чальную разметку. Рассмотрим сеть, изображенную на рисунке 1.21. В данном случае дуги (p1, t1 ) и (p2, t1 ) заменены на дугу (p3, t1 ), в начальной разметке ре­ Рис. 1.21. Пример редукции заменой входных дуг и изменением начальной разметки. Для сети N выполняется p1 + p2 p3.

Рис. 1.22. Пример некорректной редукции. Для сети N выполняется p1 + p2 p3, однако (N, p1 + 2p2 ) сурс p1 + p2 заменен на p3. Если бы мы не изменили начальную разметку, то в сети N ни один переход не смог бы сработать.

Однако и замены начальной разметки не всегда достаточно для корректной редукции. Рассмотрим сети, изображенные на рисунке 1.22. Сеть N получена из сети N тем же преобразованием, что и в предыдущем случае. Однако мар­ кированные сети (N, p1 + 2p2 ) и (N, p2 + p3 ) не бисимулярны. Действительно, в сети (N, p1 +2p2 ) возможна последовательность срабатываний t3.t1.t1, помеченная словом “baa”, тогда как в сети (N, p2 + p3 ) переход, помеченный символом “a”, может сработать только один раз.

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

Рассмотрим следующее условие. Пусть заменяемый ресурс “неделим” с точ­ ки зрения начальной разметки сети и с точки зрения предусловий и постусловий ВСЕХ переходов. Другими словами, этот ресурс входит в начальную размет­ ку “целое” число раз и всякий переход при срабатывании забирает из входных позиций и помещает в выходные позиции “целое” число таких ресурсов.

Это условие достаточно сильное, однако оно позволяет производить полную замену одного ресурса на другой (подобный):

Утверждение 1.10. [6](замена подобных ресурсов) Пусть (N, M0 ) — помеченная маркированная сеть Петри, где N = (P, T, F, l) — помеченная сеть Петри. Пусть r, s (P) — ресурсы сети N, такие, что - для любого перехода t T выполняется t = it r + gt, где it Nat, gt r =, Пусть M0 = ns + M 0, N = (P, T, F, l) — помеченная сеть Петри, такая, что Тогда (N, M0 ) (N, M0 ).

Очевидно, что после такой замены многие позиции могут остаться несвя­ занными ни с одним переходом, и их можно будет просто удалить из сети. Строго говоря, Утверждение 1.11. [6] Пусть выполнены все условия утверждения 1.10, p P.

Рис. 1.23. Пример редукции заменой подобных ресурсов. Для сети N выполняется 2p1 p2.

Произведена замена при r = 2p1, s = p2.

Другими словами, позиция p избыточна, если она принадлежит ресурсу r и не принадлежит ресурсу s.

Это не единственный “побочный” эффект от замены подобных ресурсов.

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

На рисунке 1.23 приведен пример редукции заменой подобных ресурсов.

Сеть N получена из сети N заменой ресурса 2p1 на ресурс p2. Сеть N полу­ чена из сети N удалением избыточной позиции p1 и перехода t1, дублирующего переход t2.

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

Рис. 1.24. Пример редукции сети Петри на основе подобия ресурсов. Для сети N выполняется Пример “комплексной” редукции сети Петри на основе подобия ресурсов приведен на рисунке 1.24. В данном случае объединены ресурсы p2 и 2p5, удале­ ны ресурсы (позиции) p1 и p4 (как тупиковые, то есть подобные пустому ресурсу ). Переходы с меткой a слиты в один переход.

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

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

Предлагаются следующие подходы:

1. Построение множеств пар ресурсов, соответствующих некоторому конеч­ ному поведению сети (бисимуляции ограниченных разметок).

2. Приближение подобия ресурсов снизу (ограниченное подобие ресурсов).

3. Приближение подобия ресурсов сверху (расслоенное подобие ресурсов).

4. Выражение свойств эквивалентности не только пассивных ресурсов-фишек, но и активных агентов-переходов (подобие обобщённых ресурсов).

5. Использование отношений эквивалентности ресурсов для адаптивного управ­ ления процессами.

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

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

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

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

2.1.1. Расслоенная бисимуляция разметок Напомним, что n-расслоенная бисимуляция разметок — это бисимуляция разметок в том случае, когда нам не важно, что будет происходить с сетью после n-го шага (см. определение в разделе 1.2.2). Все последующее поведение сети просто игнорируется.