|
|
| (124 intermediate revisions by 2 users not shown) |
| Line 1: |
Line 1: |
| '''Мрежите на Петри''' ({{lang-en|Petri net}}), още наричани '''позиционно-преходни мрежи''' (''place-transition nets'') задават един от няколкото езика за математическо моделиране и описание на дискретни разпределени системи. Мрежата на Петри е ориентиран двуделен (двуцветен) граф, чиито възли представляват:
| |
| * ''преходи'' (''transitions''), т.е. дискретни събития, които могат да се случат,
| |
| * ''позиции'' (''places''), т.е. условия, и
| |
| * ''насочени (ориентирани) дъги'', които описват кои позиции за кои преходи са пред- и/или пост-условия.
| |
|
| |
|
| Мрежите на Петри са дефинирани през 1962 година от [[Карл Адам Петри]].
| |
|
| |
| Подобно на индустриални стандарти като [[UML]]-диаграмите, [[Business Process Modeling Notation]] и [[Event-driven process chain]],появили се доста по-късно, мрежите на Петри предлагат графична нотация на постъпкови процеси, съдържащи избор, итерация и паралелно изпълнение. За разлика от тези стандарти, мрежите на Петри имат точна математическа дефиниция на семантиката на изпълнението си, с добре разработена математическа теория за анализ на процесите.
| |
|
| |
| == Неформално описание ==
| |
| Една мрежа на Петри се състои от позиции, преходи и насочени дъги. Една дъга свързва една позиция и един преход, но не и двойка позиции или двойка дъги. Позиция, от която започва дъга, се нарича входна позиция за прехода; а такава, в която влиза започнала от преход дъга, се нарича изходна позиция.
| |
|
| |
| Позициите могат да съдържат произволен неотрицателен брой ''ядра'' (''tokens''). Разпределението на ядрата по позиции на мрежата се нарича ''маркировка'' (''marking''). Маркировката отразява състоянието на системата във фиксиран момент от време. Тя се променя в някой следващ момент, в резултат от активиране на поне един преход. Един преход в мрежата на Петри се активира, когато се появи ядро в някоя от входните му позиции; когато преход се активира, ядрата от входните позиции на прехода преминават към изходните му позиции. Преминаването на ядра през прехода се извършва на една неделима стъпка.
| |
|
| |
| Мрежите на Петри са подходящ инструмент за моделиране на паралелни процеси и конкурентното поведение на разпределени системи.
| |
|
| |
| == Формално определение ==
| |
|
| |
| === Синтаксис ===
| |
|
| |
| '''[[Граф (математика)|Граф]] на мрежата на Петри''' е тройката <math>(S,T,W)\!</math>, при която
| |
| * <math>S</math> е крайно непразно [[множество]] от позиции,
| |
| * <math>T</math> е крайно непразно множество от преходи,
| |
| * сечението на множествата <math>S</math> и <math>T</math> е [[празно множество|празното множество]], т.е. никой от обектите в графа не може да е едновременно и позиция, и преход.
| |
| * <math>W: (S \times T) \cup (T \times S) \to \mathbb{N}</math> е [[мултимножество]] от насочени дъги, т.е. дефинира дъгите и им присвоява по едно неотрицателно [[цяло число]] <!-- arc multiplicity -->.
| |
|
| |
| The ''flow relation'' е множество от дъги: <math> F = \{ (x,y) \mid W(x,y) > 0 \}</math>. In many textbooks, arcs can only have multiplicity 1, and they often define Petri nets using <math>F</math> instead of <math>W</math>.
| |
|
| |
| Графът на мрежата на Петри е [[двуделен граф|двуделен]] [[мултиграф]] <math>(S \cup T, F)</math> с възли <math>S</math> и <math>T</math>.
| |
|
| |
| Множеството от входните позиции на преход е <math>{}^{\bullet}t = \{ s \in S \mid W(s,t) > 0 \}</math>; множеството от изходните позиции на преход е: <math>t^{\bullet} = \{ s \in S \mid W(t,s) > 0 \}</math>
| |
|
| |
| ''Маркировка'' на графа на мрежата на Петри е мултимножество от своите позиции, т.е. изображение от вида <math>M: S \to \mathbb{N}</math>. Казваме, че маркировката присвоява на всяка позиция определен брой ядра.
| |
|
| |
| '''Мрежа на Петри''' е четворката <math>(S,T,W,M_0)\!</math>, при която
| |
| * <math>(S,T,W)</math> е графът на мрежата на Петри;
| |
| * <math>M_0</math> е началната маркировка на графа.
| |
|
| |
| === Семантика на изпълнението ===
| |
|
| |
| Поведението на една мрежа на Петри се дефинира като релация на нейните маркировки, по следния начин:
| |
|
| |
| Маркировки могат да се добавят като към всяко мултимножество: <math>M + M' \ \stackrel{D}{=}\ \{ s \to M(s) + M'(s) \mid s \in S \}</math>
| |
|
| |
| Изпълнението на графа на мрежата на Петри <math>G = (S,T,W)\!</math> може да се определи като ''релацията преход'' <math>\to_{G}</math> между нейните маркировки по следния начин:
| |
| * за всяко <math>t</math> от <math>T</math>: <math> M \to_{G,t} M' \ \stackrel{D}{\Leftrightarrow}\ \exists M'': S \to \mathbb{N}:
| |
| M = M'' + \textstyle\sum_{s \in S} W(s,t) \ \wedge\
| |
| M' = M'' + \textstyle\sum_{s \in S} W(t,s)</math>
| |
| * <math> M \to_{G} M' \ \stackrel{D}{\Leftrightarrow}\ \exists t \in T: M \to_{G,t} M'</math>
| |
|
| |
| С други думи,
| |
| * активирането на преход <math>t</math> в една маркировка <math>M</math> поглъща <math>W(s,t)</math> ядра от всеки от неговите входни позиции <math>s</math>, и генерира <math>W(t,s)</math> ядра във всяка от изходните му позиции <math>s</math>
| |
| * преходът е ''в готовност'' (още се казва, че е ''достъпен'', т.е. може да бъде ''активиран'') в <math>M</math>, ако всичките му входни позиции съдържат ядра, т.е. само тогава когато <math>\forall s: M(s) \geq W(s,t)</math>, и всичките му изходни позиции са празни.
| |
|
| |
| Интересуваме се най-вече какво може да се случи когато преходите могат продължително време да се активират в произволен ред.
| |
|
| |
| Казваме, че една маркировка <math>M'</math> ''е достижима'' от маркировката <math>M</math> ''на един такт'' ако <math>M \to_G M'</math>; казваче, че е ''достижима от '' <math>M</math> ако <math>M {\to_G}^* M'</math>, където <math>{\to_G}^*</math> е [[транзитивно затваряне]] на <math>\to_G</math>; т.е. ако е достижима за 0 или повече такта (стъпки).
| |
|
| |
| За една (маркирана) мрежа на Петри <math>(S,T,W,M_0)\!</math>, се интересуваме от активациите, които могат да настъпят при дадена начална маркировка <math>M_0</math>. Множеството от ''достижимите маркировки'' е множеството <math>R(N) \ \stackrel{D}{=}\ \{ M' \mid M_0 {\to_{(S,T,W)}}^* M' \} </math>
| |
|
| |
| ''Графът на достижимостта'' на <math>N</math> е релацията на прехода <math>\to_G</math>, ограничена върху своите достижими маркировки <math>R(N)</math>. <!-- It is the [[state space]] of the net. -->
| |
|
| |
| ''Последователността от активациите'' за една мрежа на Петри с граф <math>G</math> и начална маркировка <math>M_0</math> е последователността от преходи <math>\vec \sigma = \langle t_{i_1} \ldots t_{i_n} \rangle</math>, за която <math>M_0 \to_{G,t_{i_1}} M_1 \wedge \ldots \wedge M_{n-1} \to_{G,t_{i_n}} M_n</math>. Множеството от последователности на активациите се означава с <math>L(N)</math>.
| |
|
| |
| === Формулировка чрез вектори и матрици ===
| |
| Маркировките на една мрежа на Петри <math>(S,T,W,M_0)\!</math> могат да бъдат разгледани като [[вектор]]и от неотрицателни цели числа с дължина <math>|S|</math>.
| |
|
| |
| Релацията на прехода на мрежата може да се опише като двойка [[матрица|матрици]] с размери <math>|S|</math> на <math>|T|</math>:
| |
| * <math>W^-</math>, определена с <math>\forall s,t: W^-[s,t] = W(s,t)</math>
| |
| * <math>W^+</math>, определена с <math>\forall s,t: W^+[s,t] = W(t,s).</math>
| |
| Тогава, тяхната разлика <math> W^T = W^+ - W^-</math> може да се използва за описание на достижимите маркировки в термините на умножението на матрици.
| |
|
| |
| За всяка последователност от преходи <math>w</math>, с <math>o(w)</math> се означава векторът, който прави съответствието между всеки преход и броя на срещанията му в <math>w</math>. Тогава,
| |
| * <math>R(N) = \{ M \mid \exists w: M = M_0 + W^T \cdot o(w) \wedge w \!</math> е последователността от активации на <math>N \}\!</math>.
| |
|
| |
| За отбелязване е изискването, че <math>w</math> е определена последователност от активации, понеже разрешаването на произволни последонателности от преходи ще генерира по-голямо множество.
| |
|
| |
| [[Image:detailed petri net.png|frame|(b) Petri net Example]] <math>W^{+}=\begin{bmatrix} * & t1 & t2 \\ p1 & 0 & 1 \\ p2 & 1 & 0 \\ p3 & 1& 0 \\ p4 & 0 & 1 \end{bmatrix} </math>
| |
|
| |
| <math> W^{-}=\begin{bmatrix} * & t1 & t2 \\ p1 & 1 & 0 \\ p2 & 0 & 1 \\ p3 & 0 & 1 \\ p4 & 0 & 0 \end{bmatrix} </math>
| |
|
| |
| <math>W^T=\begin{bmatrix} * & t1 & t2 \\ p1 & -1 & 1 \\ p2 & 1 & -1 \\ p3 & 1 & -1 \\ p4 & 0 & 1 \end{bmatrix}</math>
| |
|
| |
| <math>M_{0}=\begin{bmatrix} 1 & 0 & 2 & 1 \end{bmatrix}</math>
| |
|
| |
| == Mathematical properties of Petri nets ==
| |
|
| |
| One thing that makes Petri nets interesting is that they provide an interesting balance between modeling power and analyzability: many things one would like to know about concurrent systems can be automatically determined for Petri nets, although some of those things are very expensive to determine in the general case. Several subclasses of Petri nets have been studied that can still model interesting classes of concurrent systems, while these problems become easier.
| |
|
| |
| An overview of such [[decision problem]]s, with decidability and complexity results for Petri nets and some subclasses, can be found in
| |
| Esparza and Nielsen (1995)<ref>[http://citeseer.ist.psu.edu/226920.html ''Decidability issues for Petri nets - a survey'', by Javier Esparza and Mogens Nielsen, in: ''Bulletin of the EATCS'', 1994. Revised, 1995.]</ref>.
| |
|
| |
| === Reachability ===
| |
| The [[reachability]] problem for Petri nets is to decide, given a Petri net <math>N</math> and a marking <math>M</math>, whether <math>M \in R(N)</math>.
| |
|
| |
| Clearly, this is a matter of walking the reachability graph defined above, until either we reach the requested marking or we know it can no longer be found. This is harder than it may seem at first: the reachability graph is generally infinite, and it is not easy to determine when it is safe to stop.
| |
|
| |
| In fact, this problem was shown to be [[EXPSPACE]]-hard<ref>Lipton, R. [http://citeseer.ist.psu.edu/contextsummary/115623/0 "The Reachability Problem Requires Exponential Space"], Technical Report 62, Yale University, 1976]</ref> years before it was shown to be decidable at all (Mayr, 1981). Papers continue to be published on how to do it efficiently<ref>P. Küngas. [http://www.idi.ntnu.no/%7Epeep/papers/SARA2005Kung.ps Petri Net Reachability Checking Is Polynomial with Optimal Abstraction Hierarchies]. In: ''Proceedings of the 6th International Symposium on Abstraction, Reformulation and Approximation'', SARA 2005, Airth Castle, Scotland, UK, July 26-29, 2005]</ref>
| |
|
| |
| While reachability seems to a 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 [[Method of analytic tableaux|tableau method]] to prove that such states cannot be reached. LTL uses the [[semi-decision procedure|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.
| |
|
| |
| === Liveness ===
| |
| Petri nets can be described as having different levels of liveness <math>L_0 - L_4</math>. While the levels of liveness are defined on transitions within the Petri net, the Petri net itself is considered <math>L_k</math> live if and only if every transition within it is <math>L_k</math> live.
| |
|
| |
| A Petri net <math>(N, M_0)</math>'s transition <math>t</math> is
| |
| * <math>L_0</math> live, or ''dead'', [[if and only if]] it can not be fired, i.e. it is not in any firing sequence <math>\vec \sigma</math> where <math>\vec \sigma \in L(N,M_0)</math>
| |
| * <math>L_1</math> live if and only if it can possibly be fired, i.e. it is in a firing sequence <math>\vec \sigma</math> where <math>\vec \sigma \in L(N,M_0)</math>
| |
| * <math>L_2</math> live if and only if for any k positive whole number, t can be fired at least k times in a firing sequence <math>\vec \sigma</math> where <math>\vec \sigma \in L(N,M_0)</math>
| |
| * <math>L_3</math> live if and only if there exists a firing sequence <math>\vec \sigma \in L(N,M_0)</math> where <math>t</math> is fired infinitely
| |
| * <math>L_4</math> live or simply ''live'' if and only if in any reachable state M (i.e. <math>\forall M \in R(N,M_0)</math>), <math>t</math> is <math>L_1</math> live
| |
|
| |
| Note that these are increasingly stringent requirements such that if a transition is <math>L_3</math> live for example, it is automatically <math>L_1</math> and <math>L_2</math> live as well. As an example, (b) Example Petri net is live with the given initial state, but with a different (e.g. totally empty) initial state, all of its transitions are dead.
| |
|
| |
| In computer programming and other applications, the property of [[liveness]] of a Petri net is used to model that the system can never lock up.
| |
|
| |
| === Boundedness ===
| |
| [[Image:Reachability graph for petri net.png|left|frame|Reachability graph of (a) Petri net Example if the net is 2-bounded. In this case, it can only have a maximum of 9 (or <math>3^2</math>) states.]]
| |
|
| |
| A Petri net is inherently <math>k</math>-bounded if in no reachable state can at any place contain more than <math>k</math> tokens. A Petri net is ''safe'' if it is 1-bounded. Naturally, the initial <math>M_{0}</math> marking is also restricted by the boundedness. Note that a Petri net is inherently bounded if and only if all its reachability graphs (i.e reachability graphs with all possible starting states) all have a finite number of states.
| |
|
| |
| Formally, <math>K : S \to \mathbb{N^+}</math> is a set of ''capacity restrictions'', which assigns to each place <math>s \in S</math> some positive number <math>n \in \mathbb{N^+}</math> denoting the maximum number of tokens that can occupy that place. A net in which each of its places has some capacity <math>k</math>, is known as an 'inherently <math>k</math>-bounded' Petri net.
| |
|
| |
| Boundedness is decidable by looking at [[Covering Problem|covering]], by constructing the [[Richard Karp|Karp]]-Miller Tree. In computer programming and other applications, the property of [[boundedness]] of a Petri net is used to model limits on available system resources such as CPUs and I/O buses.
| |
|
| |
| [[Image:Place transformation petri net.png|thumb|right|299px|Example ''place-transformation''. The grey place that was originally inherently 2-bounded has been transformed into two places: a grey original, and a counter place]]
| |
| Boundedness of a certain place in an inherently bounded net can be mimicked in a non-inherently bounded net by doing a ''place-transformation'', where a new place (called ''counter-place'') is created, and all transitions that put x tokens to the original place take x tokens from the counter-place, and all transitions that take away x tokens from the original place put x tokens to the counter-place. The number of tokens in <math>M_{0}</math> must now satisfy the equation place+counter-place=boundedness. Thus, doing a place-transformation for all places in a bounded net, and restricting the starting state <math>M_{0}</math> to conform to the above noted equality, a bounded net can easily be transformed to a non-bounded net. Therefore any analysis that is used on inherently non-bounded nets can be used on bounded nets (but not the other way around).
| |