Введение
Сеть Петри, также известная как сеть «место/переход» (PT net), является одним из нескольких языков математического моделирования для описания распределённых систем. Это класс дискретных динамических систем, управляемых событиями. Сеть Петри – это ориентированный двудольный граф, имеющий два типа элементов: места и переходы. Элементы «место» изображаются белыми кругами, а элементы «переход» – прямоугольниками. Место может содержать любое количество маркеров, изображаемых чёрными кругами. Переход активируется, если все места, связанные с ним в качестве входов, содержат хотя бы один маркер. Некоторые источники утверждают, что сети Петри были изобретены в августе 1939 года Карлом Адамом Петри в возрасте 13 лет для описания химических процессов. Подобно отраслевым стандартам, таким как диаграммы деятельности UML, модель и нотация бизнес-процессов (BPMN) и цепочки событийных процессов, сети Петри предлагают графическую нотацию для пошаговых процессов, включающих выбор, итерацию и параллельное выполнение. В отличие от этих стандартов, сети Петри имеют точное математическое определение семантики выполнения и хорошо развитую математическую теорию для анализа процессов.
A Petri net, also known as a place/transition net (PT net), is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes. Like industry standards such as UML activity diagrams, Business Process Model and Notation, and event driven process chains, Petri nets offer a graphical notation for stepwise processes that include choice, iteration, and concurrent execution. Unlike these standards, Petri nets have an exact mathematical definition of their execution semantics, with a well developed mathematical theory for process analysis.
Исторический фон
Немецкий ученый-компьютерщик Карл Адам Петри, именем которого названы эти структуры, всесторонне проанализировал сети Петри в своей диссертации 1962 года «Kommunikation mit Automaten».
Основы сети Петри
Сеть Петри состоит из мест, переходов и дуг. Дуги соединяют место с переходом или наоборот, но никогда не соединяют места между собой или переходы между собой. Места, из которых дуги ведут к переходу, называются входными местами этого перехода; места, в которые дуги ведут от перехода, называются выходными местами перехода. Графически, места в сети Петри могут содержать дискретное количество маркеров, называемых токенами. Любое распределение токенов по местам представляет собой конфигурацию сети, называемую маркировкой. В абстрактном смысле, относящемся к диаграмме сети Петри, переход может быть выполнен (сработать), если он активирован, то есть во всех его входных местах достаточно токенов; при выполнении перехода необходимые входные токены потребляются, а в его выходных местах создаются новые токены. Выполнение перехода является атомарным, то есть представляет собой единый, неделимый шаг. Если не определена политика выполнения (например, строгий порядок переходов, определяющий приоритет), выполнение сети Петри является недетерминированным: когда одновременно активировано несколько переходов, они могут быть выполнены в любом порядке. Поскольку выполнение перехода недетерминировано, и в сети может присутствовать несколько токенов в любом месте (даже в одном и том же), сети Петри хорошо подходят для моделирования параллельного поведения распределенных систем.
Формальное определение и основная терминология
Сети Петри – это системы переходов состояний, расширяющие класс сетей, называемых элементарными сетями. Определение 1. Сеть – это кортеж, где P и T – непересекающиеся конечные множества мест и переходов соответственно. F – это множество (направленных) дуг (или отношений потока). Определение 2. Для сети N = (P, T, F) конфигурация – это множество C, такое что C ⊆ P.
and are disjoint finite sets of places and transitions, respectively. is a set of (directed) arcs (or flow relations). Definition 2. Given a net N = (P, T, F), a configuration is a set C so that C ⊆ P.
Определение 3. Элементарная сеть – это сеть вида EN = (N, C), где N = (P, T, F) – сеть, а C – конфигурация, такая что C ⊆ P. Определение 4. Сеть Петри – это сеть вида PN = (N, M, W), расширяющая элементарную сеть, где N = (P, T, F) – сеть, M: P → Z – мультимножество мест, где Z – счетное множество. M расширяет понятие конфигурации и обычно описывается со ссылкой на диаграммы сети Петри как маркировка. W: F → Z – мультимножество дуг, так что число (или вес) для каждой дуги является мерой кратности дуги. Если сеть Петри эквивалентна элементарной сети, то Z может быть счетным множеством {0,1}, а элементы из P, отображаемые в 1 посредством M, образуют конфигурацию. Аналогично, если сеть Петри не является элементарной сетью, то мультимножество M может интерпретироваться как представление не-одиночного набора конфигураций. В этом смысле M расширяет понятие конфигурации для элементарных сетей на сети Петри. На диаграмме сети Петри (см. верхнюю фигуру справа) места обычно изображаются кругами, переходы – длинными узкими прямоугольниками, а дуги – односторонними стрелками, показывающими соединения мест с переходами или переходов с местами. Если бы диаграмма представляла элементарную сеть, то места в конфигурации обычно изображались бы как круги, каждый из которых содержит одну точку, называемую токеном. На приведенной диаграмме сети Петри (см. справа) круги мест могут содержать более одного токена, чтобы показать, сколько раз место встречается в конфигурации. Конфигурация токенов, распределенных по всей диаграмме сети Петри, называется маркировкой. На верхнем рисунке (см. справа) место p1 является входным местом для перехода t, в то время как место p2 является выходным местом для того же перехода. Пусть PN0 (на верхнем рисунке) будет сетью Петри с маркировкой M0, а PN1 (на нижнем рисунке) – сетью Петри с маркировкой M1. Конфигурация PN0 позволяет выполнить переход t, поскольку все входные места содержат достаточное количество токенов (показаны на рисунках в виде точек), "равное или большее" кратности соответствующих дуг к t. Переход будет выполнен один раз и только один раз, когда он станет возможным. В этом примере выполнение перехода t генерирует отображение, которое имеет маркировку M1 в образе M0 и приводит к сети Петри PN1, показанной на нижнем рисунке. На диаграмме правило выполнения перехода можно охарактеризовать вычитанием из его входных мест числа токенов, равного кратности соответствующих входных дуг, и добавлением нового числа токенов в выходные места, равного кратности соответствующих выходных дуг. Примечание 1. Точное значение выражения "равное или большее" будет зависеть от точных алгебраических свойств сложения, применяемых к Z в правиле выполнения, где незначительные изменения алгебраических свойств могут привести к другим классам сетей Петри; например, алгебраическим сетям Петри. Следующее формальное определение основано на существующих альтернативных определениях.
N = (P, T, F) is a net. C is such that C ⊆ P is a configuration. Definition 4. A Petri net is a net of the form PN = (N, M, W), which extends the elementary net so that
N = (P, T, F) is a net. M : P → Z is a place multiset, where Z is a countable set. M extends the concept of configuration and is commonly described with reference to Petri net diagrams as a marking. W : F → Z is an arc multiset, so that the count (or weight) for each arc is a measure of the arc multiplicity. If a Petri net is equivalent to an elementary net, then Z can be the countable set {0,1} and those elements in P that map to 1 under M form a configuration. Similarly, if a Petri net is not an elementary net, then the multiset M can be interpreted as representing a non singleton set of configurations. In this respect, M extends the concept of configuration for elementary nets to Petri nets. In the diagram of a Petri net (see top figure right), places are conventionally depicted with circles, transitions with long narrow rectangles and arcs as one way arrows that show connections of places to transitions or transitions to places. If the diagram were of an elementary net, then those places in a configuration would be conventionally depicted as circles, where each circle encompasses a single dot called a token. In the given diagram of a Petri net (see right), the place circles may encompass more than one token to show the number of times a place appears in a configuration. The configuration of tokens distributed over an entire Petri net diagram is called a marking. In the top figure (see right), the place p1 is an input place of transition t; whereas, the place p2 is an output place to the same transition. Let PN0 (top figure) be a Petri net with a marking configured M0, and PN1 (bottom figure) be a Petri net with a marking configured M1. The configuration of PN0 enables transition t through the property that all input places have sufficient number of tokens (shown in the figures as dots) "equal to or greater" than the multiplicities on their respective arcs to t. Once and only once a transition is enabled will the transition fire. In this example, the firing of transition t generates a map that has the marking configured M1 in the image of M0 and results in Petri net PN1, seen in the bottom figure. In the diagram, the firing rule for a transition can be characterised by subtracting a number of tokens from its input places equal to the multiplicity of the respective input arcs and accumulating a new number of tokens at the output places equal to the multiplicity of the respective output arcs. Remark 1. The precise meaning of "equal to or greater" will depend on the precise algebraic properties of addition being applied on Z in the firing rule, where subtle variations on the algebraic properties can lead to other classes of Petri nets; for example, algebraic Petri nets. The following formal definition is loosely based on Many alternative definitions exist.
Изменения в определении
Общая вариация состоит в запрете кратных дуг и замене множества дуг W простым набором, называемым отношением потока. Это не снижает выразительную силу, поскольку оба представления могут быть преобразованы друг в друга. Другая распространенная вариация, например, в Desel и Juhás (2001), заключается в разрешении определять пропускную способность для мест. Это рассматривается в разделе "Расширения" ниже.
Теоретическая формулировка категорий
Месэгуер и Монтанари рассматривали особый вид симметричных моноидальных категорий, известных как категории Петри.
Математические свойства сетей Петри
Одна из причин, по которой сети Петри представляют интерес, заключается в том, что они обеспечивают баланс между выразительностью моделирования и возможностью анализа: многие характеристики, которые хотелось бы знать о параллельных системах, могут быть автоматически определены для сетей Петри, хотя определение некоторых из них в общем случае может быть очень затратным. Исследовано несколько подклассов сетей Петри, которые по-прежнему способны моделировать интересные классы параллельных систем, при этом указанные определения становятся более простыми. Обзор таких задач принятия решений, с результатами о разрешимости и сложности для сетей Петри и некоторых их подклассов, можно найти в работе Esparza и Nielsen (1995).
Доступность
Проблема достижимости для сетей Петри состоит в том, чтобы определить, для заданной сети Петри N и маркировки M, возможно ли достичь этой маркировки. Это сводится к обходу графа достижимости, определенного выше, до тех пор, пока не будет достигнута требуемая маркировка или пока не станет ясно, что дальнейший поиск невозможен. Это сложнее, чем кажется на первый взгляд: граф достижимости обычно бесконечен, и нелегко определить, когда можно безопасно остановиться. Фактически, было показано, что эта проблема является EXPSPACE-сложной за годы до того, как было доказано, что она вообще разрешима (Mayr, 1981). Статьи, посвященные эффективному решению этой проблемы, продолжают публиковаться. В 2018 году Czerwiński et al. улучшили нижнюю оценку сложности и показали, что проблема не является элементарной. В 2021 году, независимо друг от друга, Jerome Leroux и Wojciech Czerwiński с Łukasz Orlikowski показали, что эта проблема не является примитивно рекурсивной. Эти результаты, таким образом, устраняют давний пробел в оценке сложности. Хотя проверка достижимости представляется полезным инструментом для обнаружения ошибочных состояний, для практических задач построенный граф обычно содержит слишком много состояний для вычисления. Чтобы смягчить эту проблему, линейная временная логика часто используется в сочетании с табличным методом для доказательства недостижимости таких состояний. Линейная временная логика использует технику полурешения для определения возможности достижения состояния, находя набор необходимых условий для его достижения, а затем доказывая, что эти условия не могут быть выполнены.
It is a matter of walking the reachability graph defined above, until either the requested marking is reached or it can no longer be found. This is harder than it may seem at first: the reachability graph is generally infinite, and it isn't easy to determine when it is safe to stop. In fact, this problem was shown to be EXPSPACE hard years before it was shown to be decidable at all (Mayr, 1981). Papers continue to be published on how to do it efficiently. In 2018, Czerwiński et al. improved the lower bound and showed that the problem is not ELEMENTARY. In 2021, this problem was shown to be non primitive recursive, independently by Jerome Leroux
and by Wojciech Czerwiński and Łukasz Orlikowski. These results thus close the long standing complexity gap. While reachability seems to be a good tool to find erroneous states, for practical problems the constructed graph usually has far too many states to calculate. To alleviate this problem, linear temporal logic is usually used in conjunction with the tableau method to prove that such states cannot be reached. Linear temporal logic uses the semi decision technique to find if indeed a state can be reached, by finding a set of necessary conditions for the state to be reached then proving that those conditions cannot be satisfied.
Живость
Сети Петри могут обладать различной степенью живости. Сеть Петри называется живой, если и только если все ее переходы живые, где переход считается мертвым, если он никогда не может быть выполнен, то есть он не входит ни в одну последовательность выполнения. Переход считается потенциально выполнимым (live), если и только если он может быть выполнен, то есть он входит в некоторую последовательность выполнения. Переход считается живым, если он может быть выполнен произвольно часто, то есть для каждого положительного целого числа k он встречается по крайней мере k раз в некоторой последовательности выполнения. Переход считается живым, если он может быть выполнен бесконечно часто, то есть существует фиксированная (необходимо бесконечная) последовательность выполнения, в которой для каждого положительного целого числа k переход встречается по крайней мере k раз. Переход считается живым (live), если он может быть выполнен всегда, то есть он живой в каждой достижимой разметке.
dead, if it can never fire, i. e. it is not in any firing sequence in
live (potentially fireable), if and only if it may fire, i. e. it is in some firing sequence in
live if it can fire arbitrarily often, i. e. if for every positive integer k, it occurs at least k times in some firing sequence in
live if it can fire infinitely often, i. e. if there is some fixed (necessarily infinite) firing sequence in which for every positive integer k, the transition occurs at least k times,
live (live) if it may always fire, i. e. it is live in every reachable marking in
Обратите внимание, что эти требования становятся все более строгими: живость подразумевает более высокую степень живости. Эти определения соответствуют обзору Мураты, который дополнительно использует термин "живой" для обозначения "мертвого" перехода.
These definitions are in accordance with Murata's overview, which additionally uses live as a term for dead.
Ограниченность
Место в сети Петри называется k-ограниченным, если оно не содержит более k токенов во всех достижимых маркировках, включая начальную маркировку; оно называется безопасным, если оно 1-ограничено; оно ограничено, если оно k-ограничено для некоторого k.
(Маркированная) сеть Петри называется k-ограниченной, безопасной или ограниченной, если все её места ограничены. Сеть Петри (граф) называется (структурно) ограниченной, если она ограничена для каждой возможной начальной маркировки. Сеть Петри ограничена тогда и только тогда, когда её граф достижимости конечен. Ограниченность определяется путем рассмотрения покрытий, а также построением дерева Карпа–Миллера. Может быть полезно явно установить ограничение на места в заданной сети. Это можно использовать для моделирования ограниченных системных ресурсов. Некоторые определения сетей Петри явно допускают это как синтаксическую особенность. Формально, сети Петри с емкостями мест могут быть определены как кортежи , где – сеть Петри, – назначение емкостей (некоторым или всем) местам, а отношение переходов является обычным, но ограничено маркировками, в которых каждое место с емкостью содержит не более указанного числа токенов. Например, если в сети N обоим местам присвоена емкость 2, мы получаем сеть Петри с емкостями мест, скажем N2; её граф достижимости изображен справа. Альтернативно, места можно сделать ограниченными путем расширения сети. В частности, место можно сделать k-ограниченным, добавив "счетное место" с потоком, противоположным потоку исходного места, и добавив токены так, чтобы общее количество токенов в обоих местах стало равно k.
a place can be made k bounded by adding a "counter place" with flow opposite to that of the place, and adding tokens to make the total in both places k.
Дискретные, непрерывные и гибридные сети Петри
Помимо дискретных событий, существуют сети Петри для непрерывных и гибридных дискретно-непрерывных процессов, а также для автоматов, связанных с дискретными, непрерывными и гибридными системами.