Algebraická Petriho síť

Algebraická Petriho síť ( anglicky  algebraic Petri net, APN ) je rozšířením konvenčních Petriho sítí , ve kterých jsou běžné značky nahrazeny prvky algebraických datových typů [1] . Tento formalismus je v mnohém podobný barevným Petriho sítím [2] , nicméně v případě algebraických sítí je sémantika datových typů dána systémem axiomů , který umožňuje provádět důkazy a výpočty nad typy pomocí něj.

Poprvé představen Jacquesem Waterrenem v roce 1985 [3] , vylepšen Wolfgangem Reisigem [4] .

Formalismus zahrnuje dvě složky:

• ovládací část daná Petriho sítí;
• část dat specifikovaná jedním nebo více algebraickými datovými typy.

Samotné algebraické datové typy lze rozdělit do dvou částí:

• podpis , který definuje platné konstanty a operace v algebře pojmů .
• axiomatizace , která definuje sémantiku operací definovaných podpisem.

Ovládací část obsahuje:

• pozice obsahující více sad markerů; markery jsou prvky algebry termínů konstruované pomocí signatury, každá pozice obsahuje jednu a pouze jednu multimnožinu termínů, pozice je typována multimnožinou, která je jí přiřazena;
• oblouky mohou být označeny více sadami definovaných nebo volných termínů, stejně jako pro pozice jsou termíny definovány z algebraických typů podpisu;
• přechody jsou události, které se spustí pokaždé, když je na vstupních pozicích dostatek značek k posunutí značky podél každého ze vstupních oblouků, a zároveň je splněna podmínka aktivace (ochrany) přechodu.

V okamžiku spuštění události se vyrobené markery přesunou do cílových pozic výstupních oblouků. Pro určení sémantiky operací zkontrolujte, zda jsou splněny zadané podmínky a vypočítejte výstupní členy, zpravidla se používají techniky přepisování termínů [5] .

Algebraické Petriho sítě posloužily jako základ pro vývoj složitějších variant stejného formalismu, zejména CO-OPN ( Concurrent Object-Oriented Petri Networks ).

Příklad

Příklad algebraické Petriho sítě navržené k modelování problému jídelních filozofů :

Používají se dva algebraické datové typy. Jedna z nich ( Fork) definuje algebru forků, druhá ( ) definuje Philosopheralgebru filozofů. Protože všichni filozofové mohou vzít levou vidličku, aniž by zvolili pravou, může spuštění tohoto modelu vést k uváznutí . Na začátku modelu je možný pouze přechod goEat. goEatPokud byl aktivován alespoň jeden , přechody takeLa také budou povoleny takeR.

Poznámky

1. ↑ Ehrig, Hartmut. Základy algebraické specifikace 1 : Rovnice a počáteční sémantika  . - Berlín: Springer Berlin Heidelberg, 1985. - 321 s. - ISBN 978-3-642-69962-7 , 3-642-69962-6, 978-3-642-69964-1, 3-642-69964-2. Archivováno 4. září 2020 na Wayback Machine
2. ↑ Jensen K. Colored Petri Nets - Berlín: Springer-Verlag, 1997. - 236 s.
3. ↑ Vautherin J. Specifikace paralelních systémů s barevnými Petrinety a algebraické specifikace. Evropský seminář o aplikacích a teorii Petriho sítí - Berlín, NY: Springer-Verlag, 1987. - S. 293-308.
4. ↑ Reisig W. Petriho sítě a algebraické specifikace // Teor. Počítat. sci. - 1991. - Sv. 80. - č. 1. - S. 1-34.
5. ↑ Dick AJ, Watson P. Přepisování termínů podle pořadí // Výpočet. J. - 1991. - Sv. 34. - č. 1. - S. 16-19.