Invariánsok és alkalmazásaik

A VIK Wikiből
(FormModInvar szócikkből átirányítva)

Ez az oldal a korábbi SCH wikiről lett áthozva.

Ha úgy érzed, hogy bármilyen formázási vagy tartalmi probléma van vele, akkor, kérlek, javíts rajta egy rövid szerkesztéssel!

Ha nem tudod, hogyan indulj el, olvasd el a migrálási útmutatót.


T-invariánsok

WT %T = 0 A %T tüzelési szekvencia nem változtatja meg a tokeneloszlást. Emiatt ciklus lesz az állapottérben.  ha egy PN élő, akkor létezik benne olyan tüzelési szekvencia amely T invariáns, és minden tranzíciót tartalmaz legalább egyszer. (ha nincs ilyen, nem élő a PN.)

P-invariánsok

W %P = 0 a %P által kijelölt helyeken a tokenek (súlyozott) száma nem változik, azaz a tokenek a helyek egy részhalmazában keringenek


Az invariánsok meghatározása

Nyilvánvaló módon akár a T akár a P-invariánsok egy-egy lineáris vektorteret alkotnak, hiszen az invariánsok tetszőleges lineáris kombinációja maga is egy invariáns lesz.

Martinez-Silva algoritmus

Alkalmazások

Predikátumok vizsgálata Invariánsokkal.

Közelítő megoldások

Kérdések és válaszok

=T-invariáns

A T invariáns azt mutatja meg, hogy a rendszerben nem fogynak el a tokenek a működés során: HAMIS a fenti tulajdonság a P invariánsra jellemző! A T invariánsok a rendszer egyes részeinek ciklikus működésének lehetőségét jelöli meg. Ettől még azonban lehetséges olyan működési mód akár ugyanezen részrendszerre, hogy a tokenek bizony elfogynak frankón!
Ciklikus működésű rendszerben mindenképp van T invariáns. IGAZ a T inv. Definíciójából adódik.
Egy T invariáns nem lehet minimális, ha létezik egy másik T invariáns, ami ugyanannyi tranzíciót tartalmaz. HAMIS Létezhet másik, azonos részhalmazú T invariáns is a rendszerben, de annak tüzelési számai nem lehetnek kisebbek.

P-invariáns

Ha egy PN van konzervatív komponens, akkor ebből még nem következik, hogy létezik benne P invariáns. HAMIS Egy PN (részlegesen) konzervatív, ha van benne P inv. .
Ha egy WT %; szomszédossági mátrixszal rendelkező PN létezik olyan %T súlyvektor hogy legalább egy token eloszlásra igyaz az összefüggés: W%T = 0 akkor a %T súlyvektort hely invariánsnak nevezzük. HAMIS minden a kezdőállapotból elérhető eloszlásra teljesülnie kell a fenti egyenlőségnek.ahhoz, hogy P invariánsnak hívhasuk
A P invariáns segít annak ellenőrzésében, hogy a modellezett rendszerben lévő folyamatok megfelelően kapcsolódnak-e az általuk használt erőforrásokhoz. IGAZ a P invariáns azt mutatja+, hogy a rendszerben az erőforrások nem fogynak el a működés során és így jól használható pl. hozzáférési protokollok helyességének bizonyításában.
Nem véges elérhetőségi gráffal rendelkező rendszerben csak akkor van P invariáns, ha van ciklikus működésű komponense. HAMIS lehet olyan rendszert találni, amiben nincs T invariáns, de tutkón van P invariáns.

Alkalmazások_v

Ha egy negálatlan klózrendszer megoldható (kielégíthető), akkor PN modelljében egy T invariánsnak megfelelő tüzelési szekvencia végrehajtható. *IGAZ* A model kialakítása úgy történt, hogy a klózrendszer megoldása egy olyan tüzelési szekvenciának feleljen meg, ami T invariáns.
T invariánsokka tetszőleges, negálatlan elsőrendű logikai formulákból álló rendszert analizálhatunk. *IGAZ* Lásd jegyzet.
Egy logikai program Petri hálós modelljében a P és T invariánsok megegyeznek. *HAMIS* A P invariánsokról szó se volt :)
Murata algoritmus negálásmentes klózok esetén Tinvariánsokra, negált klózokat tartalmazó logikai program esetén P invariánsokra működik. *HAMIS* A Murata algoritmus működésének feltétele, hogy a klózrendszer negálatlan legyen.


-- adamo - 2006.04.02. -- szamosa - 2007.05.27.