Мрежите на Петри (на английски: Petri net) задават един от няколкото езика за математическо моделиране и описание на дискретни разпределени системи. Мрежата на Петри е ориентиран двуделен (двуцветен) граф, чиито възли представляват:

  • преходи (transitions), т.е. дискретни събития, които могат да настъпят,
  • позиции (places), т.е. условия, и
  • насочени (ориентирани) дъги, които описват кои позиции за кои преходи са пред и/или пост-условия.

Мрежите на Петри са дефинирани през 1962 година от Карл-Адам Петри.

Подобно на индустриални стандарти като UML-диаграмите, Business Process Modeling Notation и Event-driven process chain, появили се доста по-късно, мрежите на Петри предлагат графична нотация на постъпкови процеси, съдържащи избор, итерация и паралелно изпълнение. За разлика от тези стандарти, мрежите на Петри имат точна математическа дефиниция на семантиката на изпълнението си, с добре разработена математическа теория за анализ на процесите.

Неформално описание редактиране

Една мрежа на Петри се състои от позиции, преходи и насочени дъги. Една дъга свързва една позиция и един преход, но не и двойка позиции или двойка преходи. Позиция, от която започва дъга, се нарича входна позиция за прехода; а такава, в която влиза започнала от преход дъга, се нарича изходна позиция.

Позициите могат да съдържат произволен брой ядра (tokens). Разпределението на ядрата по позиции на мрежата се нарича маркировка (marking). Тя отразява състоянието на системата във фиксиран момент от време и се променя в някой следващ момент, в резултат от активиране на поне един преход. Преход в мрежата на Петри се активира, когато се появи ядро в някоя от входните му позиции; когато преход се активира, ядрата от входните позиции на прехода преминават към изходните му позиции. Преминаването на ядра през прехода се извършва на една (неделима) стъпка.

Мрежите на Петри са подходящ инструмент за моделиране на паралелни процеси и на конкурентното поведение на разпределени системи.

Формално определение редактиране

Синтаксис редактиране

Граф на мрежата на Петри е тройката  , при която

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

Множеството от входните позиции на преход е  ; множеството от изходните позиции на преход е:  

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

Мрежа на Петри е четворката  , при която

  •   е графът на мрежата на Петри;
  •   е началната маркировка на графа.

Семантика на изпълнението редактиране

Поведението на една мрежа на Петри се дефинира като релация на нейните маркировки, по следния начин:

Маркировки могат да се добавят като към всяко мултимножество:  

Изпълнението на графа на мрежата на Петри   може да се определи като релацията преход   между нейните маркировки по следния начин:

  • за всяко   от  :  
  •  

С други думи,

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

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

Казваме, че една маркировка   е достижима от маркировката   на един такт ако  ; казваче, че е достижима от   ако  , където   е транзитивно затваряне на  ; т.е. ако е достижима за 0 или повече такта (стъпки).

За една (маркирана) мрежа на Петри  , се интересуваме от активациите, които могат да настъпят при дадена начална маркировка  . Множеството от достижимите маркировки е множеството  

Графът на достижимостта на   е релацията на прехода  , ограничена върху своите достижими маркировки  .

Последователността от активациите за една мрежа на Петри с граф   и начална маркировка   е последователността от преходи  , за която  . Множеството от последователности на активациите се означава с  .

Формулировка чрез вектори и матрици редактиране

Маркировките на една мрежа на Петри   могат да бъдат разгледани като вектори от неотрицателни цели числа с дължина  .

Релацията на прехода на мрежата може да се опише като двойка матрици с размери   на  :

  •  , определена с  
  •  , определена с  

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

За всяка последователност от преходи  , с   се означава векторът, който прави съответствието между всеки преход и броя на срещанията му в  . Тогава,

  •   е последователността от активации на  .

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

 
Пример за мрежа на Петри

 

 

 

 

Математически свойства на мрежите на Петри редактиране

Едно от нещата, които правят мрежите на Петри интересни за изследване е, че те предоставят интересен баланс между моделиращата сила и анализируемостта: много неща, които е желателно да се знаят за конкурентните системи могат автоматично да се определят за мрежите на Петри, въпреки че в общия случай някои от тези неща са много ресурсоемки („скъпи“) за определяне. Изучавани са няколко подкласа от мрежи на Петри, които продължават да могат да моделират интересни класове от конкурентни системи, докато проблемите, които възникват в процеса на работа, са по-прости.

Достижимост редактиране

Проблемът за достижимостта при мрежите на Петри е да се определи за дадена мрежа на Петри   и маркировка  , дали  .

Очевидно, проблемът се свежда до обхождането на гореописания граф на достижимостта до момента, в който или се достигне желаната маркировка, или става ясно, че тя повече не може да бъде достигната. Тази задача е по-трудна, отколкото на пръв поглед изглежда: в общия случай графът на достижимостта е безкраен и не е лесно да се определи кога търсенето да спре.

През 1976 година е доказано, че този проблем е с експоненциална сложност[1], пет години преди да е доказано, че той изобщо е разрешим (Mayr, 1981). Продължават да се публикуват статии, които дискутират как да се намери по-ефективно решение.[2]

Въпреки че достижимостта изглежда добър инструмент за откриване на грешни състояния, конструираният граф обикновено има твърде много състояния, които трябва да се проверяват, за да е удачен за практически нужди. За да се разреши този проблем, обикновено се прибягва към линейна темпорална логика за доказване кои състояния са недостижими, като открива набора от необходими условия за достигане на дадено състоянието и после доказва, че тези условия не могат да бъдат удовлетворени.

Живост редактиране

На мрежите на Петри могат да се присвоят различни степени на „живост“ (liveness)  . Докато степените на живост се дефинират над преходите на мрежата, тя самата се смята за   „жива“ тогава и само тогава, когато всеки преход в нея е   жив.

Един преход   на мрежа на Петри   е:

  •   не е жив, или с други думи „мъртъв“, тогава и само тогава, когато той не може да бъде активиран, т.е. не принадлежи на нито една серия от активации  , където  ,
  •   жив, тогава и само тогава, когато е възможно той да бъде активиран, понеже принадлежи на една серия от активации  , където  ,
  •   жив, тогава и само тогава, когато за произволно положително цяло число  , преходът   може да се активира поне k пъти в една серия от активации  , където  ,
  •   жив, тогава и само тогава, когато съществува серия от активации   където преходът   се активира неограничен брой пъти,
  •   жив, или с други думи „жив“, тогава и само тогава, когато във всяко достижимо състояние M (т.е.  ), преходът   е   жив.

Трябва да се отбележи, че строгостта на тези изисквания нараства постъпково, и в този смисъл ако един преход е   жив, то той автоматично е и   жив и   жив.

Ограниченост редактиране

 
Граф на достижимостта на (a) мрежа на Петри. Пример ако мрежата е 2-ограничена. В този случай тя може да има най-много 9 (т.е.  ) състояния.

Една мрежа на Петри се нарича  -ограничена, ако в никое от нейните достижими състояния не могат по едно и също време в една позиция да се съдържат повече от   ядра. Една мрежа на Петри се нарича сигурна, ако е 1-ограничена, т.е. е сигурно, че между ядрата в позицията няма да настъпят конфликти за ресурси и др. Началната маркировка  , естествено, също е ограничена. Една мрежа на Петри е ограничена тогава и само тогава, когато всичките ѝ графи на достижимостта (т.е. графите на достижимост с всички възможни начални състояния) вкупом притежават краен брой състояния.

Формално,   е множеството от ограничения на капацитета, които присвояват на всяка позиция   някакво цяло положително число  , означаващо максималния брой ядра, които едновременно могат да се съдържат в позицията. В класическата мрежа на Петри са дефинирани само капацитети на позициите; едва в обобщената мрежа на Петри на Генрих и Лаутенбах (H. J. Genrich, K. Lautenbach) са въведени и капацитети на позициите.

Източници редактиране

  1. Lipton, R. "The Reachability Problem Requires Exponential Space", Technical Report 62, Yale University, 1976]
  2. P. Küngas. Petri Net Reachability Checking Is Polynomial with Optimal Abstraction Hierarchies Архив на оригинала от 2012-02-09 в Wayback Machine.. In: Proceedings of the 6th International Symposium on Abstraction, Reformulation and Approximation, SARA 2005, Airth Castle, Scotland, UK, July 26 – 29, 2005]
    Тази страница частично или изцяло представлява превод на страницата Petri net в Уикипедия на английски. Оригиналният текст, както и този превод, са защитени от Лиценза „Криейтив Комънс – Признание – Споделяне на споделеното“, а за съдържание, създадено преди юни 2009 година – от Лиценза за свободна документация на ГНУ. Прегледайте историята на редакциите на оригиналната страница, както и на преводната страница, за да видите списъка на съавторите. ​

ВАЖНО: Този шаблон се отнася единствено до авторските права върху съдържанието на статията. Добавянето му не отменя изискването да се посочват конкретни източници на твърденията, които да бъдат благонадеждни.​