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

• 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

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.

• IA023 Petriho sítě

• http://www.fi.muni.cz/usr/kucera/teaching.html