|
|
| (123 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>
| |
|
| |
| == Математически свойства на мрежите на Петри ==
| |
|
| |
| Едно от нещата, които правят мрежите на Петри интересни за изследване е, че те предоставят интересен баланс между моделиращата сила и анализируемостта: много неща, които е желателно да се знаят за конкурентните системи могат автоматично да се определят за мрежите на Петри, въпреки че в общия случай някои от тези неща са много ресурсоемки ("скъпи") за определяне. Изучавани са няколко подкласа от мрежи на Петри, които продължават да могат да моделират интересни класове от конкурентни системи, докато проблемите, които възникват в процеса на работа, са по-прости.
| |
|
| |
| === Достижимост ===
| |
| Проблемът за [[достижимост]]та при мрежите на Петри е да се определи за дадена мрежа на Петри <math>N</math> и маркировка <math>M</math>, дали <math>M \in R(N)</math>.
| |
|
| |
| Очевидно, проблемът се свежда до обхождането на гореописания граф на достижимостта до момента, в който или достигнем желаната маркировка, или знаем, че тя повече не може да бъде достигната. Тази задача е по-трудна, отколкото на пръв поглед изглежда: в общия случай графът на достижимостта е безкраен и не е лесно да се определи кога търсенето да спре.
| |
|
| |
| През 1976 година е доказано, че този проблем е с [[експоненциална сложност]]<ref>Lipton, R. [http://citeseer.ist.psu.edu/contextsummary/115623/0 "The Reachability Problem Requires Exponential Space"], Technical Report 62, Yale University, 1976]</ref>, пет години преди да е доказано, че той изобщо е разрешим (Mayr, 1981). Продължават да се публикуват статии, които дискутират как да се намери по-ефективно решение.<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>
| |
|
| |
| При все, че достижимостта изглежда добър инструмент за откриване на грешни състояния, конструираният граф обикновено има твърде много състояния, които трябва да се проверяват, за да е удачен за практически нужди. За да се разреши този проблем, обикновено се прибягва към [[линейна темпорална логика]] за доказване кои състояния са недостижими, като открива набора от необходими условия за достигане на дадено състоянието и после доказна, че тези условия не могат да бъдат удовлетворени.
| |
|
| |
| === 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.
| |
|
| |
| === Ограниченост ===
| |
| [[Image:Reachability graph for petri net.png|left|frame|Граф на достижимостта на (a) мрежа на Петри. Пример ако мрежата е 2-ограничена. В този случай тя може да има най-много 9 (т.е. <math>3^2</math>) състояния.]]
| |
|
| |
| 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).
| |