Zadání

13. Vlastnosti různých Petriho sítí

Vypracování

Klíčové pojmy

  • Petriho síť, označkování, přechodový systém Petriho sítě
  • dosažitelné označkování, živost přechodu
  • problémy
    • dosažitelnost, sub-marking reachability, zero-reachability, single-place zero-reachability
    • pokrytelnost
    • ohraničenost, k-ohraničenost místa/sítě
    • inkluze/rovnost množin dosažitelných označkování
    • živost přechodu/sítě, uváznutí
  • strom pokrytelnosti
  • redukce problémů
  • ekvivalence
    • trace-ekvivalence, bisimulace
    • nerozhodnutelnost skrz redukci z problému zastavení Minského stroje
  • model checking Petriho sítí, nerozhodnutelnost
  • klasické techniky - incidenční matice, Parikův obraz
  • S-invarianty
  • T-invarianty
  • S-systémy
  • T-systémy
  • Free-choice systémy

Nejaké moje čmáraniny

N=(P,T,F). P- miesta, T-prechody, F- sipky s pocetnostou.
Označkovanie: priradenie tokenov miestam
Prechodový system: (S, A, sipka). S= markingy. Vzdy cez prechody. Prechody su oznackovane, nie nutne odlisne. Funkcia l:T→A.
Zivost: Dane: N, M, t. Z kazdeho dosiahnutelneho markingu M’ sa da dostat do markingu, kde je prechod uskutocnitelny.

Problemy:
- DOSIAHNUTELNOST: Je pre N a M dosiahnutelne M’
- POKRYTELNOST: Mam N, M, M’. Existuje M’’ take, ze v kazdom mieste ma aspon tolko tokenov ako M’ a je dosiahnutelne z M.
- OHRANICENOST MIESTA: N, M, p. Existuje prirodzene cislo k, tz pre kazdy M’ dosiahnutelny z M je M’(p)⇐k?
- k-OHRANICENOST (k je dane na vstupe, nie kvantifikovane), OHR. SIETE, k-OHR. SIETE
- ZIVOST PRECHODU: N, M, t. Je prechod t zivy?
- UVIAZNUTIE: Existuje dosiahnutelne znackovanie, kde nie je uskutocnitelny ziaden prechod?

Strom pokrytelnosti: N, M. dosiahnutelne markingy. Kontrola, ci uz neboli. Omegy ak to moze ist donekonecna.

Dicksonovo lemma o neklesajucich podpostupnostiach v (N U infty)^k. Strom pokrytelnosti v konecnom case.

- Trace ekvivalencia: 2 markingy su TE, ak sa z nich vieme hybat pod rovnakymi postupnostami labelov.
- Bisimulacna ekvivalencia: 2 markingy su BE, ak v jednom prechode sa viem v 1 markingu dostat do ineho markingu, tak v 2. markingu sa viem dostat (pod prechodom s tym istym labelom) do markingu, ktory je BE s (inym markingom).

Minskeho stroj (MS): postupnost operacii l1, …., lm, kde
li je Com i pre i < m
lm : halt
Com je Typ I alebo Typ II.
Typ I: inc cj
Typ II: if cj=0 then goto lk else dec cj, goto ln.

VETA: Nech dvojvlnka je relacia na markingoch mnozinovo medzi BE a TE. Problem, ci dve oznackovania M1, M2 su v dvojvlnke je NEROZHODNUTELNY.
DOKAZ: Cez Minskeho stroj. Lubovolnemu MS najdeme PS, jej olabelovanie a 2 markingy, tz:
MS zastavi ⇔ M1 BE M2
MS nezastavi ⇔ M1 \not TE M2

VETA: Nerozhodnutelnost Model Checkingu pre LTL^F a ET a vsetky „tazsie“ logiky
DOKAZ: (Idea pre LTL^F): Redukcia. Dostanem lubovolny MS. Z neho skontruujem Petriho siet a jej marking. Vytvorim formulu, ktora pre beh plati prave vtedy, ked simulovany MS zastavi. Model checking je preto nerozhodnutelny.

——– ODTERAZ predpoklady:
- F → {0,1}.
- Slabo suvisly graf
——–

INCIDENCNA MATICA: N: PxT → {-1,0,1}. Efekt prechodu t na miesto p. N(p,t):=F(t,p)-F(p,t)

S-INVARIANT

Definicia: I \in Q^|P| ak IN = nulovy vektor.
Neformalne: vektor vah jednotlivych miest, aby vazeny sucet vsetkych dosiahnutelnych markingov bol rovnaky. Plati pre vsetky mozne inicialne markingy.
Alternativne definicia: Pre kazdy prechod siete je sucet I(p) cez vstupy (miesta p) do prechodu t = sucet I(p) cez vystupy z prechodu t.

Semipozitivny: nenulovy a I(p)>=0 pre vsetky p in P
Pozitivny: I(p)>0 pre vsetky p.

VETA: N, M0 je ziva → IM > 0
VETA: Pozitivny S-invariant → ohranicenost pre vsetky pociatocne markingy

T-INVARIANT

J in Q^|T| je T-invariant ak NJ = nulovy vektor
- Semipozitivny, pozitivny podobne ako s-invariant
- Podobna alternativna definicia

VETA: N, M0 je ziva a ohranicena → existuje pozitivny T-invariant
VETA: N, M0 ziva a ohranicena → ma silne suvisly graf (zjavne nezmysel, ak graf nemusi byt slabo suvisly. Lenze to musi, vid „ODTERAZ predpoklady“)

S-SYSTEM

Kazdy prechod ma 1 vstup a 1 vystup

VETA: Vsetky oznackovania z daneho oznackovania maju rovnaky pocet tokenov.
VETA: S-SYSTEM s M0. Je zivy ↔ graf je silne suvisly a existuje p, ktore ma v M0 aspon 1 token
TVRDENIE: S-SYSTEM so SSG: vsetky tokeny je mozne presunut naraz do 1 miesta. Vyplyvaju z toho nejake vety.

T-SYSTEM
Kazde miesto dava do 1 prechodu a berie z 1 prechodu
- CYKLUS
VETA: T-SYSTEM N, marking M0, gama cyklys: pre kazdy dosiahnutelny marking M: M0(g)=M(g).
VETA: T-system je zivy ↔ kazdy cyklus je oznackovany
VETA: Zivy T-system s M0 je b-ohraniceny prave vtedy ak kazde miesto p in P lezi na nejakom cykle gama takom, ze M0(gama)⇐b.

FREE CHOICE SYSTEM
F(s,t)=1 ⇒ (forall s‘ in *t)(forall t‘ in s*): F(s‘,t‘)=1.
- CLUSTER: miesta skadial sa ide a prechody, kam sa ide.
- SIFON: mnozina miest. Ak je prazdny, uz zostane prazdny.
- PASCA: mnozina miest. Ak obsahuje token, uz vzdy bude obsahovat token.

Předměty

Zdroje

mgr-szz/in-tei/13-tei.txt · Poslední úprava: 2014/10/27 09:07 (upraveno mimo DokuWiki)
Nahoru
CC Attribution-Noncommercial-Share Alike 3.0 Unported
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0