Tulajdonság modellek

Ez az oldal a korábbi SCH wiki-ről lett áthozva. Az eredeti változata itt érhető el.

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

Elérhetőség

Elérhetőség Az Mn állapot egy M0 kezdőállapotból elérhető, ha létezik egy olyan tüzelési szekvencia, mely M0-ból Mn-be viszi át a tokeneloszlás vektort. Jelölés (% a tüzelési szekvencia): M0[% > Mn

• Tétel*: az elérhetőégi probléma megoldható, habár többnyire legalább exponenciális, ellenben nem találtak olyan algoritmust, ami az egyenlőségi problémát megoldaná, nevezetesen olyat, ami két PN lehetséges tüzelési sorozatainak azonosságát vizsgálná.

Korlátosság

• *Korlátosság*: Egy petri hálót k-korlátosnak mondanak, ha az egyes helyeken levő tokenek számának létezik egy k értékű felső korlátja adott M0 kezdőállapot esetén
• *Korlátosság<->Kapacitáskorlátos hely*: nem tölthető túl a hely erős tüzelési szabály Felírható ez a PN olyan alakra, hogy nincs kapacitáskorlát, mindezt pár plusz elemmel(hely+tranzíció/él) tudjuk megvalósítani.(pl korlátnak megfelelő mennyiségű token egy plussz helybe, és ez szintén csatlakozik a tranzícióba, illetve ha a place-ből kiveszünk valamennyi tokent, ugyanannyit kell vissza is tenni a "plusz" helynek-> a plusz hely a szabad kapacitásmennyiséget mutatja)
• Biztosság (biztonságosság): egy petri hálót biztosnak mondanak, ha 1-korlátos. Például az FSM struktúra (ebben csak egy token van).

Élő tulajdonság

Lx tartalmazza Lx-1-et. Egy petri háló Lx élő, ha minden tranzíciója Lx élő.

• L0 élő tranzíció (halott): ha t sohasem tüzelhető (nincs benne egy L(N,M0)-beli szekvenciában sem, másképp: nincs benne a fedési gráfban cimkeként)
• L1 élő tranzíció (potenciálisan tüzelhető): ha t legalább egy L(N,M0)-beli szekvenciában legalább egyszer benne van
• L2 élő tranzíció: ha t tetszőleges k pozitív egészre t legalább k-szor tüzelhető valamely L(N,M0)-beli tüzelési szekvenciában
• L3 élő tranzíció: ha t végtelen sokszor tüzelhető valamely L(N,M0)-beli tüzelési szekvenciában
• L4 élő tranzíció (élő): ha t tetszőleges M0-ból elérhető M állapot esetében L1 élő

Megfordíthatóság és visszafordítható állapot

• *Megfordíthatóság*: Egy petri háló akkor megfordítható, ha az M0-ból kiindulva tetszőleges köztes M eleme R(N,M0) álapotból M0-hoz visszatérhetünk, azaz a hálózat alkalmas ciklikus működésre
• *Visszatérő állapot*: Sokszor a háló nem megfordítható, mert az elején inicializáló szekvencia van. Ilyenkor visszatérő állapotnak nevezzük azt az M’ eleme R(N,M0) állapotot, amely M0 tetszőleges M eleme R(N,M0) követő állapotából elérhető

Fedhetőség

Egy petri háló M tokeneloszlása fedhető, ha létezik olyan M0-ból elérhető M’ eleme R(N,M0), hogy M’ >= M

Perzisztencia

Egy petri hálót perzisztensnek nevezünk, ha két tetszőleges engedélyezett tranzíció közül az egyik tüzelése sem tiltja le a másikat. Ebből következik, hogy ha egy tranzíció már engedélyezett, mindaddig engedélyezve marad, amíg nem tüzel

Fairség

• Két tüzelés akkor van egy korlátos fair (B-fair) relációban, ha annak a maximális száma korlátos, hogy az egyik hányszor tüzelhet anélkül, hogy a másik tüzelne. Egy petri hálót akkor nevezünk korlátos fair-nek, ha tetszőleges tranzíciópárja korlátos fair.
• Egy tüzelési szekvencia globálisan fair akkor, ha vagy véges, vagy a hálózat összes tranzíciója végtelen sokszor fordul elő benne.

=Elérhetőség_v

Az elérhetőségi analízis a a PN dinamikus tulajdonságainak vizsgálatát jelenti.	*IGAZ*	Lásd jegyzet.
Ha egy PN egy Mn tokeneloszlás elérhető az M0 kezdőállapotból, akkor a háló által modellezett rendszer működése során legalább egyszer iztosan eljut a fenti tokeneloszlásnak megfelelő Mn állapotba.	*HAMIS*	a PN nemdeterminisztikus volta miatt
Az elérhetőségi analízis megvalósítására a szélességi keresés célravezetőbb eszköz, mint a mélységi keresés.	*IGAZ*	nem korlátos elérhetőségi gráfban a mélységi keresés nem feltétlenül terminál még akkor sem, ha a keresett csomópont elérhető a kezdőállapotból.
Ha Mn tokeneloszlás elérhető az M0 kezdőállapotból, akkor ebből következik, hogy M0 tokeneloszlás is elérhető Mn állapotból.	*HAMIS*	ez csak élő PN esetében mondható ki.

Korlátosság_v

Ha egy Petri háló biztos, akkor egyúttal korlátos is

*IGAZ*

/DEF =Élőség_v Ha egy tranzíció L2-élő, akkor biztosan L1-élő is. *IGAZ* az Li élőség mindig maga után vonja az Li-k élőséget Ha egy (N, M0) Petri háló minden tranzíciója végtelen sokszor előfordul valamely tüzelési szekvenciában, akkor biztosan L3-élő, de nem biztosan L4-élő. *IGAZ* Az L3 élőség még mindig kezdőállapot függő, így az L4 élőség nem garantálható. Az állítás első része viszont pont L3 definíciója. Ha egy (N, M0) Petri háló minden tranzíciója végtelen sokszor előfordul valamely tüzelési szekvenciában, akkor biztosan nincs benne deadlock. *HAMIS* A deadlockmentesség csak az L4 élő Petri hálók esetén garantált, az állítás pedig nem garantálja ezt (lásd előző pont) Ha egy Petri háló elérhetőségi gráfja nem véges, akkor a háló biztosan L3-élő. *HAMIS* Attól, hogy az elérhetőségi gráf nem véges, még lehet, hogy egy tranzíciót egyáltalán nem sütünk el Egy élő PN TETSZŐLEGES kezdőállapotból elindítva Deadlock-mentes. *HAMIS* Mivel minden M(eleme)R(M0) állapotra visszatérő, így elérhetőségi gráfja erősen összekötött, azaz minden csomópontjában van legalább egy kimenő él, de semmit nem mond az M'(nemeleme)R(M0) állapotról. Egy PN L2 élő, ha egy adott kezdőállapotból indítva létezik L2 élő tüzelése. *HAMIS* Egy PN L2 élő, ha minden egyes tüzelése L2 élő. Megfordíthatóság_v Ha egy Petri háló megfordítható, akkor tetszőleges M R(N, M0) állapot visszatérő állapot *IGAZ* Ha minden elérhető állapot visszatérő, akkor minden állapotból magába M0-ba is vissza tudunk térni =Fedhetőség_v Egy Petri háló fedhetősége garantálja, hogy (ha M jelöli a t tranzíció tüzeléséhez szükséges minimális tokeneloszlást) ha t halott, akkor M lefedhető *HAMIS* Hát, t akkor és csak akkor halott, ha M nem fedhető le... Perzisztencia_v Egy perzisztens Petri háló két tetszőleges tranzíciója közül egyik sem tilthatja le a másikat *HAMIS* A kiemelt tetszőleges szó magában foglalja az az esetet is, amikor nem engedélyezett egyik vagy másik tranzíció, márpedig ekkor nincs rájuk megkötés, letilthatják egymást. A perzisztencia arra jellemző, hogy eredetileg párhuzamosnak szánt rendszerbeli működések nem zavarják-e egymást. *IGAZ* perzisztens hálóban az egyszerre engedélyezett tranzakciók tüzelése nem tilthatja le egymást, ezért párhuzamos működések valóban függetlenek egymástól Egy perzisztens PN-ben nem fordulhat elő, hogy két párhuzamosan engedélyezett tranzakció közül az egyik végtelen sokszor tüzeljen, anélkül, hogy a másik tüzelne. *HAMIS* ez a korlátos-fair (B-fair) PN-ek tulajdonsága. Fairség_v Ha egy PN korlátos-Fair (B-fair) tulajdonságú, akkor az általa modellezett rendszerben nem fordulhat elő „kiéheztetés”, azaz minden konkurrens tevékenység véges időn belül végrehajtódik *IGAZ* hiszen ha egy tranzakció tetszőleges párja B fair, akkor véges tüzelési szekvencia után tüzelni fog, hiszen bármely más tranzíció csak véges alkalommal tüzelhet anélkül, hogy a kiválasztott tranzakció tüzelne. Két párhuzamosan engedélyezett tranzíció B-fair relációban áll egymással, ha bármelyikük mindaddig engedélyezve marad, míg tüzel. *HAMIS* ez a perzisztencia (pontatlan) definíciója -- adamo - 2006.04.02.