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

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

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

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

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

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

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

17 А.ПР 201

Ярославль - 2014

005547251

Работа выполнена на кафедре теоретической информатики Федерального государственного бюджетного образовательного учреждения высшего профессионального образования "Ярославский государственный университет им. П. Г. Демидова".

Научный консультант: доктор физико-математических наук, профессор Ломазова Ирина Александровна Официальные оппоненты:

Вагин Вадим Николаевич, доктор технических наук, профессор (Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования "Национальный исследовательский университет "МЭИ") Дехтярь Михаил Иосифович, доктор физико-математических наук, доцент (Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования "Тверской государственный университет") Захаров Владимир Анатольевич, доктор физико-математических наук, доцент (Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования "Московский государственный университет имени М. В. Ломоносова")

Ведущая организация: Федеральное государственное бюджетное учреждение науки "Институт системного программирования Российской академии наук"

Защита состоится '19" рлеЛ. 2014 г. в К часов на заседании диссертационного совета Д 002.017.02 в Федеральном государственном бюджетном учреждении науки "Вычислительный центр им. А. А. Дородницына Российской академии наук", расположенном по адресу: 119333, г. Москва, ул. Вавилова, д. 40.

С диссертацией можно ознакомиться в библиотеке ВЦ РАН.

Автореферат разослан /и¿f>T4 2014 г. Ученый секретарь

диссертационного совета Д 002.017.02,

д.ф.-м.н., профессор

В. В. Рязанов

Общая характеристика работы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

щенных чисел Фробениуса.

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

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

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

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

Сети потоков работ (\\Т-сети) представляют собой специальный подкласс сетей Петри, используемый для формализации управления технологическими процессами, бизнес-процессами, \уеЬ-сервисами, распределенными вычислени-

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

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

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

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

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

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

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

Предложен новый формализм моделей распределенных систем, названный

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Степень достоверности и апробация результатов. Основные результаты диссертации докладывались на научных семинарах ЯрГУ им. П. Г. Демидова и ВЦ РАН им. А. А. Дородницына, а также на международных конференциях: "Интеллектуальное управление: новые интеллектуальные технологии в задачах управления" (Переславль-Залесский 1999); "Concurrency, Specification and Programming" (Берлин 2002, Руциане-Нида 2005, Берлин 2006, Краков 2009, Берлин 2010, Пултуск 2011, Берлин 2С12); "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 статей в российских журналах из перечня ВАК [1-8] и 8 статей в зарубежных изданиях, входящих в международные индексы цитирования из перечня ВАК [9-16]), 10 статей в прочих рецензируемых журналах [17-26], 27 статей в сборниках трудов конференций и прочих сборниках [27-53], одна монография [54] и одно учебное пособие [55]).

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

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

Содержание работы

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

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

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

Мультимножеством М над конечным множеством X называется функция М : X -* Nat, где Nat — множество неотрицательных целых чисел. Числа [М(х) | х е X] называются коэффициентами мультимножества, коэффициент М{х)

определяет число экземпляров элемента хъМ. Множество всех мультимножеств над X обозначается как М(Х).

Для отношения В £ М(Х) X М(Х) его аддитивным транзитивным замыканием ВАТ называется наименьшее по вложению подмножество множества М{Х) х ЛКХ), такое, что: (1) В с ВАТ; (2) Ч(МиМ2), (М[,М'2) е ВАТ (My + М[, М2 + Щ) е ВАГ; (3) V(Mb М2), (Mi, Мъ) е ВАТ (My, Л/3) е ВЛТ.

Отношение В' с М(Х) х М(Х) называется АТ-базисом отношения В, если (В')АТ = ВАТ. Базис В' называется минимальным АТ-базисом отношения В, если не существует В" с В', такого что (В")АТ = ВЛТ.

Определение 1.13. На множестве В с М(Х) х М(Х) определим частичный порядок С (отдельно для рефлексивных и нерефлексивных пар):

def

(n.n)C (г2,г2) о n Сг2 Л г,

def

(Г1+01,Г1+0\)С(,Г2+02,Г2+0'2) «

def

<=> Oi П o'j = 0 Л 02 П 02 = 0 Л rl С г2 л £ с>2 Л o'l G С>2-

Через Bs обозначим множество минимальных относительно С элементов Влт. В случае, когда (0,0) е В, к Bs также добавляется пара (0,0).

Теорема 1.1. Пусть отношение В симметрично и 1-рефлексивно (содержит все пары вида (х, х), где |х| = 1). Тогда Bs является его базисом и Bs конечно.

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

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

Системой помеченных переходов называется набор LTS = (S,Act, —So), где S — конечное множество состояний, Act — конечный алфавит имен действий, —>S (S xActxS) — отношение переходов (с пометками из Act), sq е S — начальное состояние. Переход (s, a, s') из —» обычно обозначается как s Д s'.

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

(Р)

О

н2о

Н.СЧ

Ог

О

н2о

Рис. 1. Срабатывание перехода в сети Петри, моделирующее химическую реакцию

Отношение R QS х 5 обладает свойством переноса, если для любой пары (s, Г) е R и любого перехода sA / найдется имитирующий переход t А такой что (i',f') 6Л. ОтношениеR QS xS называется отношением бисимуляции, если Кий-1 обладают свойством переноса. Наибольшее по вложению отношение бисимуляции обозначается как (~).

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

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

Обыкновенной сетью Петри называется набор N = (Р, Т, F), где Р — конечное множество позиций; Т — конечное множество переходов, Р П Т = 0; F : (Р х Г) U (Г х Р) -> Nat — функция инцидентности. Разметкой (состоянием) сети N называется функция вида М : Р -»Nat.

Разметка может рассматриваться как мультимножество над множеством позиций сети. Графически разметка изображается при помощи маркеров (называемых "фишками") — черных точек внутри позиций (Рис. 1).

Для перехода t е Т через't и f* обозначим мультимножества его входных и выходных позиций, такие, что Vp е Р 't(p) =л-/ F(p,t), t'(p) =def F(t,p).

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

Разметка М называется достижимой от Мц, если существует последовательность переходов сг е Т*, переводящая сеть из состояния М0 в состояние М.

Множество всех достижимых разметок сети обозначается как Mo)

Помеченной сетью Петри называется набор N = (Р, Г, F, I), где (Р, Т, F) — сеть Петри, I: Т -* Act — помечающая функция.

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

Определение 1.30. Ресурсом сети N = (Р, Т, F, Г) называется мультимножество над множеством позиций Р.

Определение 131. Ресурсы г и s называются подобными (обозначается г и s), если для любой разметки М, такой, что г с М, выполняется М ~ M—r+s.

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

Теорема 1.3. Отношение подобия ресурсов обладает конечным АГ-базисом.

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

Определение 132. Симметричное 1-рефлексивное отношение В с М(Р) х М(Р) называется бисимуляцией ресурсов, если ВАТ есть бисимуляция разметок.

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

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

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

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

Ресурсы г и s называются условно подобными (обозначается г s), если существует ресурс b' е М(Р), такой, что г ~\ь> s.

Теорема 1.10. Пусть («) — множество всех пар подобных ресурсов сети,

(я|) — множество всех пар условно подобных ресурсов. Тогда множество (я) — полулинейно, причём существует конечное множество Л с (я|), такое, что

(») = \JiCondiZ) + 1с(Т)1 2<ая

где 2я — множество всех подмножеств Л, Соги1(£) — множество всех минимальных общих условий для элементов Z, 1с(2) — множество всех линейных комбинаций над 2.

Теорема 1.11. Проблема распознавания условного подобия неразрешима.

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

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

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

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

Определение 2.1. Бисимуляция достижимых разметок (~[кл/„)])

М\ ~Им„)] Мг « ~ М2 л Мх е Я(ЛГ, М„) л М2 е Ш, Ш-

Определение 2.2. Бисимуляция ограниченных разметок (~щ): М\ М2 о М1 ~ М2 Л |Я(ЛГ, Л/,)| < оо л М2)\ < оо.

Определение 2.3. Расширение бисимуляции (~[е(м0)]) :

Mi ~[с(Мо)1 Мг « ЭМ3 е Л/0) : М, ~ М2 - М3.

Теорема 2.1. Отношения (~[км0)]) и (~мм0)]) разрешимы в ограниченных сетях Петри.

Наибольший практический интерес представляет отношение (~[<.(м0)])- Однако оно может содержать бесконечно много пар разметок, поэтому необходимо уметь строить какие-то его конечные представления или подмножества.

Определение 2.4. Элементарным расширением бисимуляции назовём отношение (~[«(а/о)]) с (~[,.(а/0)]), такое, что

Ml ~[ee(Ma)] м2 $М3 е М(Р) : {Mi ~ М2 ~ Мг Л (М3 с М, V М3 с М2)>.

Теорема 2.2. Множество (~[«(м0)]) вычислимо в ограниченных сетях.

В доказательстве теоремы приведён алгоритм построения.

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

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

=def {(Г, S) е (*) | (И < n & |i| < п) V (г, S) е («я)ЛГ).

Соответствующее отношение назовем ti-ограниченным подобием ресурсов.

Утверждение 2.7. Для любой помеченной сети Петри N найдется число и € Nat, такое что (и) = (=sj).

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

Теорема 2.3. «-ограниченное подобие неразрешимо для любого п > 0.

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

Пусть (~„) — и-расслоенная бисимуляция разметок (бисимуляция разметок в том случае, когда поведение сети после п-го шага игнорируется).

Определение 2.6. Через («„) обозначим множество пар ресурсов, задающее на (~„) отношение подобия:

(«л) =&/ 1 (г, s) е М(Р) х М(Р) | VAi б ЩР) (М + г, М + s) е (-„)).

Соответствующее отношение назовем п-расслоенным подобием ресурсов.

Утверждение 2.8. Для любого п € Nat, п > 0, выполняется (=„+i) с («„).

Утверждение 2.10. (») - (ям).

Теорема 2.4. л-расслоенное подобие ресурсов вычислимо.

В доказательстве теоремы приведён алгоритм построения.

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

Определение 2.8. Пара (г, а), ще г е М(Р),а е М(Т) и "а с г, называется обобщенным ресурсом сети N.

Определение 2.9. Обобщенные ресурсы (г, а) и (s,ß) называются подобными (обозначается (г, а) » (s,ß)), если

1. /(а) = /08);

2. для любой разметки М е М(Р) и параллельного срабатывания М + г^*М'

р

возможно параллельное срабатывание М + s —» М", где М' ~ М".

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

Следствие 2.5. Подобие обобщенных ресурсов обладает конечным основным базисом.

Следствие 2.7. Подобие обобщенных ресурсов неразрешимо.

В разделе 2.5 рассматривается важная область применения отношений эквивалентности ресурсов — адаптивное управление.

На практике в ходе эксплуатации автоматизированных систем управления (в частности, систем управления потоками работ — Workflow Management Systems) в процесс зачастую приходится вносить изменения непосредственно в ходе его выполнения. Это может происходить по причине доступности/недоступности тех или иных ресурсов, сбоев в отдельных модулях, в силу необходимости обрабатывать нестандартные ситуации/запросы и по многим другим причинам. В связи с этим необходимо уметь автоматически находить эквивалентные замены для отказавших элементов системы.

В подразделе 2.5.1 рассматривается управление "без потерь" на основе подобия обобщенных ресурсов — отказавшие материальные и/или инструментальные ресурсы заменяются на подобные, при этом наблюдаемое поведение системы сохраняется (в смысле бисимулярности).

В подразделе 2.5.2 рассматривается тактическое управление "с потерями" на основе расслоенного подобия. Дается гарантия на сохранение поведения только до определенного времени (шага), в дальнейшем системе позволяется изме-

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

Третья глава посвящена исследованию систем, содержащих один потенциально неограниченный ресурс, моделируемый целочисленным неотрицательным счетчиком. Односчетчиковые сети, известные также как одномерные системы векторного сложения с состояниями (1-dim Vector Addition Systems with States — VASS), эквивалентны сетям Петри с одной неограниченной позицией, а также магазинным автоматам с односимвольным стековым алфавитом. Ограничение на число счетчиков делает данный формализм менее выразительными, чем обыкновенные сети Петри, однако существенно облегчает анализ. В данной работе используется теоретико-числовой метод, основанный на числах Фробениуса.

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

Для удобства введём новое обозначение одномерных линейных множеств (линейных множеств натуральных чисел). Пусть т с Nat линейно, тогда для некоторого / е Z+ выполняется

т = Lin{v, {wj,..., и>7}} =def {v + n\wi +... + щщ | пь...,щ е Nat),

где v, wi,..., w; € Nat фиксированы.

Множество т с Nat назовём ограниченно неполным линейным множеством, если т - т'\т", где т' — линейное множество, а т" — конечное множество. Если т' = Lin{v,[wi,..., w;)} и iv е Nat — наибольший элемент т", то мы обозначаем т как DLin{v, w + 1, {wi,..., и>;)|.

Лемма 3.1. Пусть т = Lin[v, {wi, vv2}} — линейное множество с двумя периодами. Тогда т может быть представлено как ограниченно неполное множество

с одним периодом. Обозначив р = НОД(н>ь иъ) и b = получим

т = DLin[v, b, {/>}}. Оценка границы неполной части является точной.

Лемма 3.2. Пусть Lin{v, (и>ь..., и>Л) — линейное множество с s периодами. Тогда т может быть представлено как ограниченно неполное множество с одним периодом. Обозначив р = HOfl(wi,...,wJ), с = max(vvb...,vv^l2 и b = v + j, получим

m = DLiti{v, b, (pi).

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

Теорема 3.1. Любое полулинейное множество т с Nat распадается на конечное множество и конечное семейство линейных множеств с одинаковым периодом: для некоторых р, b е Nat, существует характеристическое множество

*F с {b, b + 1, b + 2,..., b + (р - 1)), такое, что

ф

m = moU m„, где то с [JO? < kp), т„ = Uc^-ы с1)

Jt= 1 k=0

Здесь < и > — операции сдвига множеств целых неотрицательных чисел соответственно влево и вправо на натуральное число.

Теорема 3.2. Пусть т £ Nat — полулинейное множество, представленное в форме (1), х,у € Nat. Пусть {А(0} — последовательность полулинейных множеств, такая что

А(0) = ш, А(М) = (А(/><х)>у. Тогда существует j < шах{[^], НОК(р, \х - у|)} + 1, такое, что

QA<» = [>1 1=1 1=1

Теорема 3.1. утверждает, что мы можем использовать в качестве конечного символьного представления произвольного полулинейного одномерного множества т его однопериодический базис (mo. b, р, v), состоящий из

• конечного базового множества то,

• базового элемента Ь,

• длины периода р,

• вектора периода v.

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

Определение 3.1. Базис Z = (то, b, р, v) полулинейного множества т с Nat называется минимальным, если для любого базиса Z' = (m'0,b',p', v') множества т выполняется р < р' или (р = р' nb < Ь').

Утверждение 3.1. Для любого одномерного полулинейного множества т с Nat минимальный базис существует и единственен.

Минимальный базис множества т обозначим как Baseitn); множество, определяемое базисом Z, обозначим как Ser(Z).

Утверждение 3.2. Произвольный базис (гщ, b, р, v) полулинейного множества т с Nat может быть преобразован в минимальный базис Base(m) за полиномиальное время относительно b * р.

Обозначим процедуру минимизации полулинейного базиса (то, b, р, v) как Mmz(mo,b,p,v).

Для двоичных векторов v,V е {0,1}р через NOT(v), AND(v,v') и OR(v, v') обозначим покомпонентное умножение, сложение и отрицание:

AND(v, v')[«]=dcfminm, v'[i]}, OR(v, v')[i]=deffnax{v[i], v'[i']}, ATOr(v)M=def<l-v[/]).

Через v* обозначим конкатенацию k векторов v: v* =def У-v-v-____v..

k

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

Теорема 3.3. Пусть т,т' с Nat — полулинейные, Base(m) = (mo,b,p, v), Base(tri) = (m'0,b',p\v'), у € Nat. Обозначим К = max{b,b'} и L = HOK(p,p'). Пусть К - b + ip = b' + jp' для некоторых f, j e Nat. Тогда:

1. Base(Nat) = (0,0,1,(1));

2. Base(m U m') = Mmz({x e mUm' \ x < K),K,L, OR(vК (v')7));

3. Base(m П m') = MmzQx e m n m' \ x < К], K, L, AND(vK (v')^));

4. Base(m \ rri) = Mmz({x e m \ m' \ x < К], K, L,AND(v',NOT((y')b));

5. mem' AND(v',(v'y) = v' AVxem(x<K=>xe m');

6. Baseim >y) = Mmz([x + y \ xe mo], b + y,p, v);

7. Base(m < y) = Mmz({x - у \ x e m, x < B,x > у), B, p, v), где

В - mirikeNatib + kp-y\b + kp-y>0).

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

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

(Непомеченной) односчетчиковой сетью называется пара N = (Q,T), где Q — конечное множество управляющих состояний, TtzQxQxX — конечное множество переходов.

Состояние сети описывается парой q\c, где q е Q — текущее управляющее состояние, с е Nat — текущее значение счетчика.

Переход t - (q, q', z) активен в состоянии q\c, если с + z > О. Активный переход может сработать, переводя сеть в состояние q']c+z (обозначается q\c q'\c + z). Для перехода t = (q,q',z) величина z также называется эффектом t

(обозначается ЕЩ/))- Ресурс перехода определяется как:

(■ 0, г > 0;

8ирр(г)=^1|г|, г<0.

Размеченной односчетчиковой семью называется пара (М, 5о), гае N = (¡2, Г) — односчетчиковая сеть, 5о е бхМй- начальное состояние (начальная разметка). Её множество достижимости ¿о) определяется как:

ЖК =ае{ {5 е й^Ым \ ¡о Л 5).

Для выделенного управляющего состояния д е ¡2 его множество достижимых значений счетчика 5о)[?] определяется следующим образом:

Я(ЛГ, л-0)М =асГ [с б Л^г/1 50 Д д\ с).

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

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

Лемма 3.4. Любой положительный цикл содержит хотя бы один генератор.

Узел д называется отрицательным генератором, если существует отрицательный маршрут в от д до д (образующий отрицательный цикл), такой, что БиррСб) = -ЕЩб).

Лемма 3.5. Любой отрицательный цикл содержит хотя бы один генератор.

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

Теорема 3.4. Пусть N = (2, Т) — положительный Д-контур, е е N01 -наибольший эффект среди всех циклов некоторое управляющее со-

стояние, и8ирр(<?) - наименьшее значение счетчика, при котором (И, <2|Ширр(д))

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

ЖЛГ, Я\иШ = Ширрф, Ширрф + + е\ {Д}}.

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

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

В разделе 3.3 рассматриваются некоторые ключевые методы анализа од-носчетчиковых сетей, основанные на символьных вычислениях с использованием однопериодической арифметики (однопериодических базисов).

В подразделе 3.3.1 предложен Алгоритм 3.1 построения однопериодическо-го представления множества достижимости односчётчиковой сети. Такое представление (однопериодическая свёртка) позволяет эффективно определять достижимость любого состояния сети, то есть решает глобальную проблему достижимости.

В подразделе 3.3.2 представлен Алгоритм 3.2 глобальной верификации формулы темпоральной логики ЕР (эта логика формализует свойства достижимости; она является расширением логики Хеннесси-Милнера и сужением логики СТЬ). Производится индуктивный разбор по структуре темпоральной формулы, использующий однопериодическую свёртку множества достижимости в качестве эффективного источника информации о структуре множеств выполнимости.

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

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

Определение 3.7. Размеченная сеть (N,q0\c0) называется правильной, если для любого т 6 Nat выполняется или R(N, q0\ca + m) = {(q\c + ri) : (q\c) e K{N,qo\co)), или K(N,qo\co) = \(q\c + n) : (<?)c) 6 «(AUofco + m)} для некоторого n e Nat.

Представление односчегчиковых сетей в виде деревьев контуров (описанное в разделе 3.2) позволяет эффективно определять правильность сети.

Утверждение 3.12. Размеченная односчетчиковая сеть (W, <jo|co) правильна тогда и только тогда, когда выполнены два условия:

1. в её дереве контуров все верхние контуры неотрицательны;

2. значение со не меньше максимального правильного ресурса входных узлов всех верхних контуров.

Следствие 3.2. Для любой размеченной односчётчиковой сети существует эквивалентная (обладающая тем же множеством достижимости) правильная односчетчиковая сеть.

Описано соответствующее преобразование дерева контуров.

Раздел 3.5 посвящён проблеме корректного построения схем потоков работ (workflow) с ресурсом.

Для моделирования потоков работ в литературе используется специальный подкласс сетей Петри — так называемые WF-сети. Сеть Петри N = (Р, Т, F) называется WF-сетью (сетью потока работ), если

1. в Р имеются две специальные позиции i и о, такие, что '/ = о* = 0;

2. любой элемент множества PUT лежит на пути из i в о.

Одной из основных задач при разработке workflow является обеспечение их правильной организованности — отсутствия тупиков, избыточных переходов, необоснованного использования ресурсов и т.п. Применяется формальный критерий бездефектности. WF-сеть N называется бездефектной, если для любой достижимой разметки М е "R(N, i) выполняется

1. ое7?(ЛГ,М);

2. о + М' е R(N,M) М' = 0.

Известно, что бездефектность разрешима для WF-сетей и для их расширения — ресурсно-ограниченных сетей (Resource-Constrained Workflow Nets, RCWF-сетей). В RCWF-сетях дополнительно добавляются ресурсы, фишки из которых могут использоваться при работе процесса, но должны вернуться на свои места по его завершении (тем самым гарантируется ограниченность сети).

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

Определение 3.11. Сетью потоков работ с ресурсами (RWF-сетью) называется набор N = (Рс, Pr, Т, Fc, Fr), где

• Nc = (Рс, Т, Fc) — обыкновенная WF-сеть (называемая управляющей подсетью сети N, при этом элементы множеств Рс и Fc называются управляющими позициями и дугами соответственно);

• Рг — конечное множество ресурсных позиций, РсС\Рг = 0;

• Fr : (Pr x Г) U (Г X Рг) -* Nat — конечное множество ресурсных дуг.

Разметка RWF-сети распадается на две составляющие — управляющую и ресурсную часть. Мультимножество с + г, в котором с е М(РС) иге М(РГ), мы будем обозначать как (с|г).

Определение 3.13. Размеченная RWF-сеть (N, с\г) называется бездефектной, если 4s е M(Pr), VM б R(N, c\r + s) выполняется:

1. 3s' б М(РГ) : o\s* е R(N, M);

2. с'У e-R(N,M) с' — о v с'По = 0.

Утверждение 3.13. Если размеченная RWF-сеть бездефектна, то размеченная WF-сеть, полученная из неё удалением ресурсных позиций и инцидентных им дуг, также бездефектна.

Следствие 3.3. Для любой бездефектной RWF-сети N множество C(N) достижимых управляющих состояний конечно.

Определение 3.14. Пусть N — RWF-сеть, с е C(N). Определим:

1 res(c) =def {г е M(Pr)\(.N,c\r) бездефектна} — множество всех бездефектных ресурсов для с;

2. mresic) =def ir е res(c) | e res{c) : г1 с r) — множество всех минимальных бездефектных ресурсов для с.

Утверждение 3.15. Для любой бездефектной RWF-сети N и для любой её управляющей разметки с e C(N) множество mres(c) конечно.

Вопрос разрешимости бездефектности произвольной RWF-сети (и вычислимости множества mres(c)) остаётся открытым. Далее мы рассматриваем частный случай RWF-сетей с одномерным ресурсом (одной ресурсной позицией), который, тем не менее, является строгим обобщением WF-сетей и RWF-сетей в силу потенциальной неограниченности множества достижимости.

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

Определение 3.15. Состояние сети (c|r) е C(N)xNat называется тупиком, если с Ф о и не существует перехода t е Т, такого, что (с|г) (с'\г').

Конечное подмножество L с C(N)xNat множества состояний сети называется блокировкой, если: (1) |L| > 1; (2) для любых (c[r), (c'lr') € L существует конечная последовательность переходов сг б Т', такая, что (с|г) (с'Ю; (3) для любых (c|r) € L и t е Г, таких, что (с|г) -4 (с"|г"), выполняется (c"\r") € L.

Утверждение 3.17/3.19. Множество тупиков/блокировок одномерной RWF-сети конечно.

Теорема 3.8. Проблема бездефектности разрешима для размеченных одномерных RWF-сетей.

Приводится алгоритм проверки бездефектности.

Определение 3.16. (Неразмеченная) RWF-сеть N называется бездефектной, если существует ресурс г, такой, что размеченная сеть (N, i|r) бездефектна.

Теорема 3.9 / 3.10. Неразмеченная одномерная RWF-сеть не бездефектна из-за тупиков/блокировок тогда и только тогда, когда в ней существуют тупиковое/блокирующее состояние (с|г), отрицательный генератор q и простой маршрут q с, такие, что ЕЩсг) е Supp(cr-) < г (здесь в — усечённое вычитание).

Следствие 3.5. Проблема бездефектности разрешима для неразмеченных одномерных RWF-сетей.

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

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

В разделе 4.1 представлен формализм сетей активных ресурсов (АР-сетей).

Рис. 2. Срабатывания узлов в сети активных ресурсов

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

Определение 4.1. Сетью активных ресурсов (АР-сетью) назовем набор AR = (V, I, О), где

• V — конечное множество вершин (ресурсов);

• / : V х V —> Nat — множество потребляющих дуг;

• О : V х V —» Nat — множество производящих дуг.

Графически вершины изображаются кружками, потребляющие дуги — пунктирными, а производящие дуги — непрерывными стрелками (Рис. 2).

Определение 4.2. Размеченной сетью активных ресурсов (сетью с начальной разметкой) назовем пару (AR, А/о), где AR = (V, I, О) — сеть активных ресурсов, Mo : V —»Nat — начальная разметка.

Определение 43. Ресурс v е V активен при разметке М, если

• Ai(v) > 0 (узел v непустой);

• Vw е V M(w) > /(w,v) (в потребляемых узлах содержится достаточное

количество фишек).

Активный при разметке М ресурс v может сработать, порождая при этом новую разметку М', где Vw е V Af'(vv) M(w) — I(w, v) + 0(v, w).

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

Теорема 4.1. Класс сетей активных ресурсов совпадает с классом обыкновенных сетей Петри.

Описаны линейные по времени процедуры трансляции сети Петри в эквивалентную ей (относительно графа достижимости) АР-сеть и АР-сети в эквивалентную ей сеть Петри.

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

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

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

В разделе 4.2 исследуются композиционные свойства АР-сетей. В отличие от классических сетей Петри, модуль здесь определяется тривиально — как подсеть, заданная некоторым подмножеством узлов исходной сети. Интерфейсом модуля (набором его связей) является множество дуг, связывающих узлы модуля с узлами внешней подсети. Таким образом, модуль может иметь четыре типа связей: вход, выход, производство и потребление (обозначаемые как А', А", Л' и Л" соответственно). Первые два из них представляют действия самого модуля, два

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

Свойство графа Prop называется наследственным, если из наличия Prop у графа G следует наличие Prop у произвольного подграфа Я графа G. Примерами наследственных свойств являются полнота, планарность, двудольность, ацикличность. Не является наследственной связность.

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

Теорема 4.2. Пусть (N, Мо) — размеченная сеть, р. — модуль сети N. Тогда:

1. если (N, Мо) ограничена, ар — А"Я-модуль, то (Л^, (Л/0)„) ограничена;

2. если (N,Мо) жива, ар — А°11'-модуль, то (А^,(Мо)ц) жива;

3. если (N^,(М0)„) жива, ар — А°-модуль, то (Njj,(М0)д) неограничена;

4. если (Д^, (Мо)м) ограничена, а р — R'-модуль, то (Njz, (М0)^) не жива.

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

Следствие 4.1. Произвольный модуль АР-сети может быть преобразован в R-модуль (модуль с интерфейсными дугами типов R' и Л") без изменения множества достижимости сети.

Таким образом, интерфейс любого модуля может быть упрощен до R-интер-фейса или А-интерфейса.

Представлен алгоритм соответствующего преобразования. Мы называем такую трансформацию R-нормализацией модуля р. и обозначаем как p(RK

Следствие 4.2. Пусть (ТУ, Мо) — размеченная АР-сеть, р — её модуль. Тогда

1. (1Я, Мо) ограничена => (Л/м<я>,(Мо),,<»>) ограничена;

2. (Л^иДМо^т) неограничена => (Ы, Мо) неограничена.

Определение 4.5. Плоской модуляризацией П сети N называется разбиение V на непересекающиеся модули {¿л, • • ■ ,Цп)- Плоская модуляризация называется плоской А/Я-модуляризацией, если каждый модуль является либо А-модулем, либо Я-модулем.

Следствие 4.3. Пусть £1 = ,...,/!„} — плоская модуляризация сети N. Пусть б — граф с вершинами из £2, в котором вершины //,■ и р,- соединены ребром тогда и только тогда, когда существует связь между модулями /и,- и Ц] в N. Сеть N может быть преобразована в эквивалентную (относительно достижимости) сеть для которой П является АЛ1-модуляризацией, тогда и только тогда, когда хроматическое число графа С равно 2.

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

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

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

Теорема 4.3. СД-эквивалентность неразрешима для АР-сетей.

Также вводится и исследуется понятие более сильной универсальной эквивалентности модулей относительно системной достижимости. УСД-эквива-лентность двух модулей означает, что они производят одинаковые множества

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

Представлен критерий УСД-эквивалентности произвольного модуля (с некоторыми ограничениями на структуру) и простейшего модуля, состоящего из единственного узла (Теорема 4.4).

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

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

В разделе 4.4 мы расширяем язык АР-сгтей засчёт использования подхода "сеть-внутри-сети" (пе^шкЫп-пе!). В новом формализме, названном Р-сетями (сетями управляемых ресурсами автоматов), любая модель имеет два уровня (Рис. 3). Системным (внешним) уровнем является обыкновенная плоская АР-сеть. Но фишками в этой сети являются не обычные "активные ресурсы", а полноценные агенты, обладающие собственным поведением (конечные автоматы). Во время своей работы агенты потребляют и производят локальные ресурсы, являясь одновременно потенциальными ресурсами для своих соседей. При этом системную сеть можно рассматривать как "карту" связей (портов), описывающих всевозможные отношения, в которых могут находиться агенты. Агент использует эти порты для взаимодействия с системными ресурсами, находящимися в соседних узлах. В частности, он может естественным образом производить /

еаг?»

Обеденный стол (системная сеть)

Философ (объектный автомат рИ])

Рис. 3. Обедающие философы — представление в виде Р-сети

потреблять / копировать / перемещать других агентов, или даже самого себя.

Отметим, что, в отличие от ссылочной семантики для объектных сетей, в случае Р-сетей агенты не "размазаны" по системной сети, а находятся в конкретных узлах. Несмотря на существенно отличающийся синтаксис,

Теорема 4.20. Класс Р-сетей по выразительной мощности эквивалентен классу обыкновенных сетей Петри.

Представлены соответствующие алгоритмы трансляции.

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

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

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

В разделе 4.5 анализируется и развивается одна из сильных сторон Р-сетей — возможность удобного моделирования пространственной динамики.

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

CRDA классифицируются в зависимости от способа начальной разметки:

1. бесконечные CRDA: все клетки бесконечной решетки, кроме конечного множества, помечены одним и тем же мультимножеством ресурсов;

2. конечные CRDA: все клетки бесконечной решетки, кроме конечного множества, пусты.

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

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

Рассматриваются три ключевых класса иерархии, порождаемой топологией одномерной решётки:

1. сети, в которых есть только входные порты (1-dim iCRDA);

2. сети, в которых есть только выходные порты (1-dim oCRDA);

3. сети со всеми типами портов (1-dim CRD А).

Теорема 4.22. 1-dim iCRDA эквивалентны конечным автоматам. Теорема 4.23. 1) Сети Петри без коммуникаций с 1-dim oCRDA;

2) Сети Петри <£ 1-dim oCRDA;

3) 1-dim oCRDA с машины Тьюринга.

Теорема 4.24. 1-dim CRDA = машины Тьюринга.

Благодарности

Автор глубоко признателен своему научному консультанту проф. И. А. Ло-мазовой за плодотворное сотрудничество, интересные обсуждения и полезные советы. Автор также благодарен проф. В. А. Соколову и всему коллективу кафедры теоретической информатики ЯрГУ за поддержку и внимание.

Список публикаций

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

2. Башкин В. А. Сети активных ресурсов // Моделирование и анализ информационных систем, — 2007, — Т. 14, № 4, — С. 13-19.

3. Башкин В. А., Ломазова И. А. О поиске эквивалентных ресурсов в сложных системах II Известия ОрелГТУ. Серия "Фундаментальные и прикладные проблемы техники и технологии: информационные системы и технологии". - 2008. - Т. 1-2 / 269 (544).- С. 33-39.

4. Башкин В. А. Формализация семантики систем с ненадежными агентами Н Программирование — 2010. — Т. 36, № 4,— С. 3-15.

5. Башкин В. А. Верификация на основе моделей с одним неограниченным счетчиком // Информационные системы и технологии, — 2010,— Т. 4(60).-С. 5-12.

6. Башкин В. А. Построение приближений бисимуляции в односчетчиковых сетях // Моделирование и анализ информационных систем.— 2011.— Т. 18, №4.-С. 34-44.

7. Башкин В. А. Наследственные свойства модульных сетей // Моделирование и анализ информационных систем. — 2012.— Т. 19, № 6.— С. 9-20.

8. Башкин В. А. Об эффективном моделировании неограниченного ресурса при помощи односчетчиковых контуров // Моделирование и анализ информационных систем, - 2013.- Т. 20, № 2.- С. 138-155.

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

10. Bashkin V. A., Lomazova I. A. Resource similarities in Petri net models of distributed systems // Parallel Computing Technologies / Ed. by Victor E. Malyshkin. - Springer Berlin Heidelberg, 2003. - Vol. 2763 of Lecture Notes in Computer Science. — P. 35^8.

11. Bashkin V. A., Lomazova I. A. Similarity of generalized resources in Petri nets // Parallel Computing Technologies / Ed. by Victor Malyshkin. — Springer

Berlin Heidelberg, 2005,— Vol. 3606 of Lecture Notes in Computer Science. — P. 27-41.

12. Башкин В. А., Ломазова И. А. Моделирование мультиагентных систем с помощью обобщенных сетей активных ресурсов // Кибернетика и системный анализ.-2011.-Т. 2,-С. 31-39.

13. Bashkin V. A., Lomazova I. A. Resource driven automata nets // Fundamenta Informaticae. - 2011. - Vol. 109, no. 3. - P. 223-236.

14. Bashkin V. A., Lomazova I. A. Cellular resource driven automata nets // Fundamenta Informaticae. - 2012,- Vol. 120, no. 3-4. — P. 245-259.

15. Башкин В. А. Модульные сети активных ресурсов // Автоматика и вычислительная техника.— 2012, — Т. 1. — С. 5-18.

16. Bashkin V. A., Lomazova I. A., Novikova Y. A. Timed resource driven automata nets for distributed real-time systems modelling // Parallel Computing Technologies / Ed. by Victor E. Malyshkin. — Springer Berlin Heidelberg, 2013. — Vol. 7979 of Lecture Notes in Computer Science. — P. 13-25.

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

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

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

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

21. Башкин В. А. Свойства бисимуляции разметок в ограниченных сетях Петри // Моделирование и анализ информационных систем, — 2006.— Т. 13, № 1.— С. 35-40.

22. Bashkin V. A. Nets of active resources for distributed systems modeling // Joint Bulletin of NCC & IIS, Сотр. Science. - 2008. - Vol. 28. - P. 43-54.

23. Bashkin V. A. Formalization of semantics of systems with unreliable agents by means of nets of active resources // Programming and Computer Software. —

2010,- Vol. 36, no. 4,- P. 187-196.

24. Bashkin V. A., Lomazova I. A. Modelling multiagent systems with the help of generalized nets of active resources // Cybernetics and System Analyses.—

2011,- Vol. 47, no. 2,- P. 202-209.

25. Bashkin V. Approximating bisimulation in one-counter nets // Automatic Control and Computer Sciences. - 2012. - Vol. 46, no. 7. - P. 317-323.

26. Bashkin V. A. Modular nets of active resources // Automatic Control and Computer Sciences.-2012.-Vol. 46, no. l.-P. 1-11.

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

28. Bashkin V. A., Lomazova I. A. Resource bisimulations in Nested Petri Nets // Concurrency, Specification and Programming. Proc. of CS&P'2002. Vol.1.

Informatik-Bericht 161,— Humboldt-Universität zu Berlin, Berlin, 2002.— P. 39-52.

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

30. Bashkin V. A. Applications of marking bisimulation for adaptive workflow management // Concurrency, Spécification and Programming. Proc. of CS&P 2005 / Ed. by L. Czaja. - Warsaw University, Warsaw, 2005. — P. 41-49.

31. Башкин В. A. Моделирование очереди (FIFO) рекурсивными вложенными сетями Петри // Современные проблемы математики и информатики.— Ярославль: ЯрГУ, 2005. — Т. 7.

32. Башкин В. А., Ломазова И. А. Подобие обобщенных ресурсов в сетях Петри// Труды второй всероссийской конференции "Методы и средства обработки информации" (МСО-2005). — М. : Изд-во ВМК МГУ, 2005.- С. 330-336.

33. Башкин В. А., Ломазова И. А. Эквивалентность ресурсов в моделях потоков работ // Программные системы: теория и приложения. Труды международной конференции.— Т. 1.— Переславль-Залесский : ИПС РАН, 2006.— С. 323-338.

34. Башкин В. А., Ломазова И. А. О параметризованном построении подобия ресурсов в сетях Петри // Интеллектуальные системы и компьютерные науки. Труды ЕХ-ой Международной конференции,— Т. 1.— М. : Изд-во мехмата МГУ, 2006.-С. 56-58.

35. Башкин В. А. Расширение бисимуляции разметок ограниченных сетей Петри // Дискретные модели в теории управляющих систем. Труды VII-ой Международной конференции. — М. : Изд-во ВМиК МГУ, 2006.

36. Bashkin V. A., Lomazova I. A. Resource equivalence in workflow nets // Concurrency, Specification and Programming. Proc. of CS&P'2006. Vol.l.— Humboldt-Universität zu Berlin, Berlin, 2006, — P. 80-91.

37. Башкин В. А. О междисциплинарных связях курса "Сети Петри" // Преподавание математики в классическом университете: Тезисы докладов научно-методической конференции преподавателей математического факультета Яр-ГУ. — Ярославль : ЯрГУ, 2007. - С. 14-17.

38. Башкин В. А. Об одном способе моделирования мультиагентных систем с динамической структурой // Параллельные вычисления и задачи управления. Труды IV-й международной научной конференции РАСО'2008,— М. : ИПУ РАН, 2008,- С. 1462-1482.

39. Башкин В. А. Специальные виды бисимуляции разметок ограниченных сетей Петри // Материалы зимних научных чтений ФСИТ РГСУ (1-4 февраля 2006 года). — М. : Логос, 2008.

40. Bashkin V. А. On the single-periodic representation of reachability in one-counter nets // Concurrency, Specification and Programming. Proc. of CS&P 2009 / Ed. by L. Czaja, M. Szczuka. — Warsaw University, Warsaw, 2009, — P. 60-71.

41. Башкин В. А. Построение дерева достижимых состояний в односчетчико-вых сетях Петри // Компьютерные науки и технологии. Сборник трудов Первой Международной научно-технической конференции. — Т. 1.— Белгород, 2009.-С. 19-22.

42. Башкин В. А. Сети активных ресурсов как обобщение двойственных сетей Петри // Дискретные модели в теории управляющих систем. Труды VIII-ой Международной конференции. — М. : МАКС Пресс, 2009. — С. 23-28.

43. Башкин В. А., Ломазова И. А. Двухуровневое моделирование мультиагентных систем на основе обобщенных сетей активных ресурсов // Труды семи-

нара "Семантика, спецификация и верификация программ: теория и приложения". — Казань, 2010. — С. 32-36.

44. Башкин В. А. Глобальная верификация свойств достижимости систем с одним неограниченным ресурсом // Информационные технологии в науке, образовании и производстве. Материалы IV Международной научно-технической конференции.— Т. 2,— Орел, 2010.— С. 6-11.

45. Башкин В. А. Об использовании однопериодических базисов для глобальной символьной верификации // Труды семинара "Семантика, спецификация и верификация программ: теория и приложения". — Казань, 2010. — С. 26-31.

46. Bashkin V. A., Lomazova I. A. Resource Driven Automata Nets // Concurrency, Specification and Programming. Proc. of (CS&P 2010).— Berlin, Humboldt-Universitat zu Berlin, 2010,- Vol. 1. — P. 37-48.

47. Bashkin V. A. Approximating bisimulation in one-counter nets // Proc. of "Program semantics, specification and verification: theory and applications".— St.Petersburg, 2011,- P. 10-17.

48. Bashkin V. A., Lomazova I. A. Cellular resource-driven automata // Concurrency, Specification and Programming. Proc. of CS&P 2011 / Ed. by L. Czaja, M. Szczuka, A. Skowron, M. Kacprzak.— Poland, Bialystok University of Technology, 2011, —P. 29-41.

49. Bashkin V. A. On the modularity in Petri Nets of Active Resources // Proc. Of Petri Nets Compositions (Petri Nets 2011). Newcastle-upon-Tyne. — Vol. 726 of CEUR. — 2011. — P. 33—47.

50. Bashkin V. A. One-counter circuits // Concurrency, Specification and Programming. Proc. of CS&P'2012. Vol.1.— Humboldt-Universität zu Berlin, Berlin, 2012. - P. 25-36.

51. Bashkin V. A. On the hereditary properties of modular nets // Proc. of "Program semantics, specification and verification: theory and applications". — N.Novgorod, 2012.-P. 24-31.

52. Bashkin V. A., Lomazova I. A. Soundness of workflow nets with an unbounded resource is decidable // Joint Proc. of Petri Nets and Software Engineering (PNSE' 13) and Modeling and Business Environments (ModBE'13). Milano.— Vol. 989 of CEUR.- 2013,- P. 61-75.

53. Bashkin V. A. One-dimensional resource workflow nets // Proc. of "Program semantics, specification and verification: theory and applications".— Yekaterinburg, 2013.-P. 11-20.

54. Башкин В. А., Ломазова И. А. Эквивалентность ресурсов в сетях Петри.— М. : Научный мир, 2008.

55. Башкин В. А. Модели потоков работ. — Ярославль : ЯрГУ, 2009.

Печ. л. 2. Заказ 207. Тираж 100. Отпечатано в типографии Ярославского государственного технического университета г. Ярославль, ул. Советская, 14 а, тел. 30-56-63.

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

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

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

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

ДИССЕРТАЦИЯ на соискание ученой степени доктора физико-математических наук

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

05201450939

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

Ярославль - 2014

Содержание

Введение...................................... 4

Глава 1. Предварительные сведения ........................................14

1.1. Множества и отношения................................................14

1.2. Эквивалентность поведений......................26

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

1.4. Ресурсы в сетях Петри.........................43

Глава 2. Некоторые методы поиска бисимуляционно-эквивалентных ресурсов....................................70

2.1. Бисимуляция в ограниченных сетях .................70

2.2. Ограниченное подобие ресурсов...................79

2.3. Расслоенное подобие ресурсов....................82

2.4. Подобие обобщенных ресурсов....................88

2.5. Адаптивное управление процессами на основе подобия ресурсов . 98

Глава 3. Некоторые методы анализа сетей с одномерным ресурсом . . 103

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

3.2. Односчетчиковые контуры.......................115

3.3. Алгоритмы анализа...........................128

3.4. Правильная организованность.....................140

3.5. Потоки работ с ресурсом........................144

Глава 4. Модели с активными и обобщёнными ресурсами.......163

4.1. Сети активных ресурсов........................165

4.2. Модульные АР-сети ..........................171

4.3. Модифицированные АР-сети .....................187

4.4. Автоматы, управляемые ресурсами..................215

4.5. Клеточные сети с бесконечномерным ресурсом...........229

Заключение....................................242

Благодарности.................................243

Литература .................................... 244

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

щенных чисел Фробениуса.

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

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

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

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

Сети потоков работ (\УР-сети) представляют собой специальный подкласс сетей Петри, используемый для формализации управления технологическими процессами, бизнес-процессами, шеЬ-сервисами, распределенными вычислени-

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

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

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

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

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

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

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

Предложен новый формализм моделей распределенных систем, названный

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

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

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

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

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

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

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

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

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

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

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

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

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

8. Расширения формализма АР-сетей для моделирования тех или иных аспектов распределенных сист