Algebraiskt Petri Net

Algebraic Petri net ( engelska  algebraic Petri net, APN ) är en förlängning av konventionella Petri-nät , där vanliga markörer ersätts med element av algebraiska datatyper [1] . Denna formalism liknar på många sätt färgade petrinät [2] , men i fallet med algebraiska nät ges semantiken för datatyper av ett system av axiom som gör att man kan utföra bevis och beräkningar över typer som använder den.

Först introducerad av Jacques Waterren 1985 [3] , förbättrad av Wolfgang Reisig [4] .

Formalism inkluderar två komponenter:

• kontrolldelen som ges av Petri-nätet;
• en bit data specificerad av en eller flera algebraiska datatyper.

De algebraiska datatyperna i sig kan delas in i två delar:

• en signatur som definierar giltiga konstanter och operationer i termalgebra .
• axiomatisering som definierar semantiken för de operationer som definieras av signaturen.

Kontrolldelen inkluderar:

• positioner som innehåller flera uppsättningar av markörer; markörer är element i en termalgebra konstruerad med en signatur, varje position innehåller en och endast en multiuppsättning termer, positionen skrivs av multiuppsättningen som tilldelats den;
• bågar kan märkas med flera uppsättningar av definierade eller fria termer, precis som för positioner definieras termer från algebraiska typer av signaturen;
• övergångar är händelser som utlöses varje gång det finns tillräckligt med markörer vid ingångspositionerna för att flytta markören längs var och en av ingångsbågarna och samtidigt är aktiverings- (skydds)villkoret för övergången uppfyllt.

I det ögonblick som händelsen avfyras, flyttas de producerade markörerna till målpositionerna för utgångsbågarna. För att bestämma operationernas semantik, kontrollera om de angivna villkoren är uppfyllda och beräkna utdatatermerna, som regel används termomskrivningstekniker [ 5] .

Algebraiska Petri-nät fungerade som grunden för utvecklingen av mer komplexa varianter av samma formalism, särskilt CO-OPN ( Concurrent Object-Oriented Petri Nets ).

Exempel

Ett exempel på ett algebraiskt petrinät utformat för att modellera middagsfilosofernas problem :

Två algebraiska datatyper används. En av dem ( Fork) definierar gafflarnas algebra, den andra ( ) definierar Philosopherfilosofernas algebra. Eftersom alla filosofer kan ta vänster gaffel utan att ta den högra, kan körning av denna modell leda till dödläge . I början av modellen är endast övergången möjlig goEat. Om minst en goEathar aktiverats, övergångarna takeLoch blir också tillåtna takeR.

Anteckningar

1. ↑ Ehrig, Hartmut. Grunderna i algebraisk specifikation 1 : Ekvationer och initial semantik  . - Berlin: 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. Arkiverad 4 september 2020 på Wayback Machine
2. ↑ Jensen K. Colored Petri Nets - Berlin: Springer-Verlag, 1997. - 236 s.
3. ↑ Vautherin J. Parallella systemspecifikationer med färgade petrinetter och algebraiska specifikationer. European Workshop on Applications and Theory of Petri Nets - Berlin, NY: Springer-Verlag, 1987. - P. 293-308.
4. ↑ Reisig W. Petri nät och algebraiska specifikationer // Theor. Comput. sci. - 1991. - Vol. 80. - Nr 1. - P. 1-34.
5. ↑ Dick AJ, Watson P. Ordningssorterad termomskrivning // Comput. J. - 1991. - Vol. 34. - Nr 1. - P. 16-19.