Analitikusan vizsgálható Petri háló alosztályok

A VIK Wikiből
(FormModPetriAlosztAnal 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.



Állapotgép (SM - State Maschine)

Véges állapotú gép (Finite State Machine) Olyan petri háló, amiben minden tranzíció egy bemenő és egy kimenő helyhez kapcsolódik. van konfliktus, de nincs szinkronizáció

Jelölt gráf (MG - Marked Graph)

Egy jelölt gráf egy olyan rendes petri háló mely minden egyes P helyének pontosan egy be és kimenő tranzíciója van van szinkronizáció, de nincs konfliktus

Szabad választású Petri háló (FC - ?)

Egy szabad választású petriháló (FC) olyan rendes petriháló, hogy bármely helyéről minden kiinduló él vagy az adott helyről kiinduló egyetlen kimenő él, vagy egy tranzíció egyetlen bemenő éle  van konkurencia és konfliktus, de nincs egyszerre kettő.(azaz nincs konfúzió)  dekomponálható FSM, és MG komponensekre EFC: lehet többszörös szinkronizáció(lásd ábra lentebb)

Asszimmetrikus választású Petri háló (AC - ?)

): Az aszimmetrikus választású petri háló (AC) egy olyan petri háló, hogy minden p1,p2 helypárosra, ha p1-nek és p2-nek vannak közös leszármazottai (ugyanaz a tranzakció mindkettőtől vesz tokent), akkor p1 leszármazottai részhalmaza p2 leszármazottainak, vagy fordítva.

Kapcsolatok

Ezen a helyen volt linkelve a aloszt.PNG nevű kép a régi wiki ezen oldaláról. (Kérlek hozd át ezt a képet ide, különben idővel el fog tűnni a régi wikivel együtt)

Élőségi és biztonságossági kritériumok

SM és MG tételek

  1. Egy ( N, M0) állapotgép a.cs.a. élõ, ha N erõsenösszefüggõ és M0-ban van legalább egy token
    • triviális, hiszen minden tüzelés csak egy tokent mozgat
  1. Egy ( N, M0) állapotgép a.cs.a. biztos, ha M0-ban van legfeljebb egy token
  2. Egy élõ ( N, M0) állapotgép a.cs.a. biztos, ha M0-ban pontosan egy token van
  3. Egy ( G, M0) jelölt gráfban a tokenek száma minden C irányított körben állandó
    • közönséges Petri háló: egyszeres élek; a körben minden csomóponthoz egy bemenõ és egy kimenõ él
  1. Egy ( G, M0) jelölt gráf a.cs.a. élõ, ha M0 állapotban minden G-beli irányított körben van legalább egy token
  2. Egy ( G, M0) jelölt gráfban egy élt jelölõ tokenek maximális száma egyenlõ az élt tartalmazó irányított körön az M0 állapotban levõ tokenek minimális számával
  3. Egy élõ ( G, M0) jelölt gráf a.cs.a. biztos, ha minden él (hely) olyan C irányított körben van, amelyre M0( C) = 1
  4. Egy G irányított gráfban a.cs.a. létezik élõ és biztos jelölt gráfot létrehozó M0 állapot, ha G erõsen összefüggõ gráf
    • a feltétel triviálisan szükséges
    • elégséges is, hiszen van legalább egy irányított kör, és minden irányított körbe elég egy tokent tenni
    • Visszacsatoló élhalmaz (Feedback Arc Set, FAS)
      • Egy E’ élhalmaz visszacsatoló élhalmaz, ha elhagyásával a G erõsen összefüggõ gráf irányított kör mentessé válik, azaz a G’ = ( V, E – E’) körmentes
      • minimális FAS: egyetlen valódi részhalmaza sem FAS
      • minimum FAS: egyetlen más FAS sem tartalmaz kevesebb élt
  1. Egy erõsen összekötött élõ ( G, M0) jelölt gráf a.cs.a. biztos, ha az M0 kezdõállapotból elérhetõ minden M∈ R( G, M0) állapotban a jelölt élek halmaza minimális visszacsatoló élhalmaz
  2. Egy ( N, M0) szabad választású háló a.cs.a. élõ, ha minden N–beli szifon (lsd.KÉP) tartalmaz jelölt csapdát (lsd.KÉP)
  3. Egy élõ ( N, M0) szabad választású háló a.cs.a. biztos, ha N lefedhetõ egy tokent
  4. Ha ( N, M0) élõ és biztos szabad választású háló, akkor N lefedhetõ erõsen összekötött MG komponensekkel. Létezik olyan M∈ R( N, M0), hogy minden ( N1, M1) komponens élõ és biztos MG háló, ahol M1 az N1-re vett rész tokeneloszlás


-- adamo - 2006.04.02.