Algebrai Petri-háló

Az algebrai Petri-háló ( angolul  algebraic Petri net, APN ) a hagyományos Petri-hálók kiterjesztése , amelyben a közönséges markereket algebrai adattípusok elemei helyettesítik [1] . Ez a formalizmus sok tekintetben hasonlít a színes Petri-hálókhoz [2] , azonban az algebrai hálók esetében az adattípusok szemantikáját egy olyan axiómarendszer adja meg, amely lehetővé teszi a típusok feletti bizonyítások és számítások elvégzését.

Először Jacques Waterren vezette be 1985-ben [3] , Wolfgang Reisig továbbfejlesztette [4] .

A formalizmus két összetevőből áll:

• a Petri háló által adott vezérlő rész;
• egy vagy több algebrai adattípus által meghatározott adat.

Maguk az algebrai adattípusok két részre oszthatók:

• egy aláírás , amely érvényes konstansokat és műveleteket határoz meg a kifejezések algebrájában .
• axiomatizáció , amely meghatározza az aláírás által meghatározott műveletek szemantikáját.

A vezérlő rész a következőket tartalmazza:

• több markerkészletet tartalmazó pozíciók ; a markerek egy szignatúrával felépített terminalgebra elemei, minden pozíció egy és csak egy multihalmazt tartalmaz, a pozíciót a hozzárendelt multihalmaz írja be;
• az íveket definiált vagy szabad kifejezések több halmaza is felcímkézheti, csakúgy, mint a pozíciók esetében, a terminusok az aláírás algebrai típusaiból vannak definiálva;
• Az átmenetek olyan események, amelyek minden alkalommal elindulnak, amikor elegendő marker van a bemeneti pozíciókban ahhoz, hogy a markert az egyes bemeneti ívek mentén mozgatják, és ezzel egyidejűleg teljesül az átmenet aktiválási (védelmi) feltétele.

Az esemény elindításakor az előállított markerek a kimeneti ívek célpozícióira kerülnek. A műveletek szemantikájának meghatározásához ellenőrizze, hogy a megadott feltételek teljesülnek-e, és számítsa ki a kimeneti tagokat, általában terminus átírási technikákat alkalmaznak [5] .

Az algebrai Petri-hálók szolgáltak alapul ugyanazon formalizmus összetettebb változatainak kidolgozásához, különösen a CO-OPN ( Concurrent Object-Oriented Petri Nets ) kidolgozásához.

Példa

Példa egy algebrai Petri-hálóra, amelyet az étkezési filozófusok problémájának modellezésére terveztek :

Két algebrai adattípust használnak. Az egyik ( ) a villák algebráját, a másik ( ) a filozófusok algebráját Forkhatározza meg . Mivel minden filozófus el tudja venni a bal villát anélkül, hogy a jobbat venné, ennek a modellnek a futtatása holtponthozPhilosopher vezethet . A modell elején csak az átmenet lehetséges . Ha legalább egy aktiválva van, az átmenetek és az átmenetek is engedélyezettekké válnak . goEatgoEattakeLtakeR

Jegyzetek

1. ↑ Ehrig, Hartmut. Az 1. algebrai specifikáció alapjai : Egyenletek és kezdeti szemantika  . - Berlin: Springer Berlin Heidelberg, 1985. - 321 p. - ISBN 978-3-642-69962-7 , 3-642-69962-6, 978-3-642-69964-1, 3-642-69964-2. Archiválva : 2020. szeptember 4. a Wayback Machine -nél
2. ↑ Jensen K. Színes Petri-hálók - Berlin: Springer-Verlag, 1997. - 236 p.
3. ↑ Vautherin J. Párhuzamos rendszerek specifikációi színes Petrinettel és algebrai specifikációkkal. European Workshop on Applications and Theory of Petri Nets - Berlin, NY: Springer-Verlag, 1987. - P. 293-308.
4. ↑ Reisig W. Petri-hálók és algebrai specifikációk // Elmélet. Comput. sci. - 1991. - 1. évf. 80. - 1. sz. - P. 1-34.
5. ↑ Dick AJ, Watson P. Sorrend szerint rendezett kifejezések átírása // Comput. J. - 1991. - 1. évf. 34. - 1. sz. - P. 16-19.