===== 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 =====
  * [[https://is.muni.cz/auth/predmet/fi/IA023|IA023 Petriho sítě]]

===== Zdroje =====
  * http://www.fi.muni.cz/usr/kucera/teaching.html