Algebraiskt petrinät
Ett algebraiskt Petri-nät ( APN ) är en utveckling av det välkända Petri-nätet där delar av användardefinierade datatyper (kallade algebraiska abstrakta datatyper (AADT)) ersätter svarta tokens. Denna formalism kan jämföras med färgade petrinät (CPN) i många aspekter. Men i APN-fallet ges semantiken för datatyperna av en axiomatisering som möjliggör bevis och beräkningar på den.
Algebraiska petrinät uppfanns av Jacques Vautherin 1985 i hans doktorsavhandling och förbättrades senare av Wolfang Reisig.
Formalismen har två aspekter:
- Styrdelen som hanteras av ett Petri-nät.
- Datadelen som hanteras av en eller flera AADT.
AADT kan delas upp i två delar:
- Signaturen (Sort och Ops i exemplet nedan) som ger de giltiga konstanterna och operationerna för termen algebra .
- Axiomatiseringen (Axiom i exemplet nedan) som ger semantiken för de operationer som beskrivs i signaturdelen.
Följande bild beskriver en algebraisk Petri net-modell av " middagsfilosofernas problem ". Det finns två AADT i denna modell, en för gafflarnas algebra, en för filosofernas algebra. Observera att filosoferna AADT använder gaffeln AADT. Eftersom alla filosofer kan ta sin vänstra gaffel utan att ta sin högra gaffel, kan exekvering av denna modell resultera i ett dödläge .
Kontrolldelen består av:
- Platser innehåller multiset (påsar) med tokens. Dessa symboler är delar av en termalgebra som bygger på signaturen för AADT (i exemplet termer som representerar antingen en filosof eller en gaffel). Varje plats innehåller en och endast en multiuppsättning termer, platsen skrivs av sin multiuppsättning.
- Bågar kan märkas med flera uppsättningar av antingen slutna eller fria termer. Återigen är termer byggda från AADT-signaturen.
- Övergångar är händelser som kan utlösas närhelst det finns tillräckligt med resurser (nämligen tillräckligt med tokens på inmatningsplatserna för att tillfredsställa alla ingångsbågar) och skyddet (avfyrningsvillkoren) för övergången håller. Sedan placeras de producerade tokens på målplatserna för utgångsbågarna. Vanligtvis används termomskrivning för den operativa semantiken för att kontrollera om villkoren håller och för att beräkna utdatatermer.
I exemplet nedan är endast transition goEat avfyrbar i början. En goEat har avfyrats, takeL och takeR är också aktiverade och kan därmed också avfyras.
Algebraiska petrinät är den grundläggande formalismen för mer avancerade sådana som CO-OPN .
Vidare läsning
- Vautherin, Jacques (1985). Un Modèle Algébrique, Basé sur les Réseaux de Petri, pour l'Etude des Systèmes Paralleles . Dessa de Docteur Ingenieur, Univ. de Paris-Sud, Centre d'Orsay.
- Jensen, Kurt. Färgade Petri Nät . Springer Verlag. ISBN 3-540-62867-3 .