S04-1 Párhuzamos folyamatok modellezése Petri hálók segítségével

1. Petri hálók definíciója és működési szabálya
2. Párhuzamos folyamatok legfontosabb viselkedési tulajdonságai (elevenség, biztonságosság, korlátosság) és azok vizsgálatára szolgáló eszközök (elérési, fedési fa).
3. Petri doboz alkalmazása párhuzamos folyamatok modelljének felépítésében.
4. Párhuzamos és elosztott rendszerek szemantikai leírása lehetséges formáinak (műveleti, leíró, axiomatikus) bemutatása egy konkrét példán keresztül.

Petri hálók definíciója és működési szabálya

Páros gráf: olyan gráf, amelyben a csúcsok két diszjunkt halmazba sorolhatóak oly módon, hogy az azonos halmazba tartozó csúcsok között nem vezet él.

Petri háló: (N, \(M_0\)) rendezett pár, ahol:

• N = (P, T, R, v) a tartó gráf, irányított, páros gráf, amelynek az élei súlyozottak
• P, T: a csúcsok véges halmazai. P a helyek halmaza, T az átmenetek halmaza
• P \(\cup\) T \(\not=\) \(\oslash\)
• P \(\cap\) T = \(\oslash\)
• R - az éleket megadó reláció: R \(\subseteq\) (P × T) \(\cup\) (T × P)
• v: R → \(N_0\) - az élek súlyait megadó függvény
• A helyek kezdeti súlyozását (kezdőállapot) az \(M_0\) adja meg
  • \(M_0\): P → \(\mathbb{N}_0\)
  • A helyek súlyozását (állapot) általában rendezett n-esként adjuk meg, pl.: \(M_0\) = (1, 0, …, 2)

Normális háló: minden él súlya 1.

Kapacitás korlát:

A háló egyes helyeinek súlya nem haladhat meg egy előre megadott értéket: \(k: P \rightarrow \mathbb{N}_0\)

• Szigorú működési szabály: a kapacitáskorlát túllépése esetén az átmenet nem megengedett
• Gyenge működési szabály: a felesleg elnyelődik

Jelölések:

• p helyet megelőző átmenetek halmaza: \(\bullet\)p = \(R^{(-1)}\)(p)
• t átmenetet megelőző helyek halmaza: \(\bullet\)t = \(R^{(-1)}\)(t)
• Adott csúcs utódja(i): p\(\bullet\) = R(p), t\(\bullet\) = R(t)

Működési szabály:

1. t átmenet aktivizálható, ha \(\forall\)p \(\in\) \(\bullet\)t: M(p) \(\ge\) v(p, t),
   vagyis minden őt megelőző hely súlya legalább akkora, mint az őket összekötő él súlya
2. t átmenet után az új M' súlyozás: \(\forall\)p \(\in\) P: M'(p) = M(p) + v(t,p) - v(p,t),
   vagyis az átmenetbe vezető élek súlyával csökken a kiinduló helyek súlya, és az átmenetből vezető élek súlyával nő a cél helyek súlya (ha egy hely nem kapcsolódik az adott átmenethez, akkor a súlya a régi marad)

Viselkedési tulajdonságok

Jelölések:

• \(\varsigma\) = \(t_1, t_2, .., t_n\) akciósorozat: a háló által végrehajtott átmenetek sorozata
• \(M_0\) [\(\varsigma\)> \(M_n\) : az \(M_0\) súlyozásból a \(\varsigma\) akciósorozattal az \(M_n\) súlyozásba jutunk. pl.: \(M_0 [t_1> M_1 [t_2> M_2 ... M_{n-1} [t_n> M_n\)
• \(L(N,M_0):\) azon akciósorozatok halmaza, amely az N-ben elérhető az \(M_0\) súlyozásból
• R(N, \(M_0\)) : N hálóban az \(M_0\) kezdő súlyozásból elérhető súlyozások halmaza
• \(\sharp\)(\(\varsigma\), t): \(\varsigma\)-ban t átmenet előfordulásának száma

K – korlátosság (k \(\in \mathbb{N}\)):

Az (N, \(M_0\)) Petri háló k - korlátos, ha \(\forall\)M \(\in\) R(N,\(M_0\)) : \(\forall\)p \(\in\) P : M(p) \(\leq\) k

Biztonságos:

Egy Petri háló biztonságos, ha 1 - korlátos

Elevenség:

Legyen t \(\in\) T. \(M_0\) kezdősúlyozástól függően az N Petri hálóban a t átmenet eleven

• \(L_0\) szinten (holt): \(\forall\)\(\varsigma\) \(\in\) L(N, \(M_0\)) : t \(\not\in\) \(\varsigma\)
  (Nem lehet egyszer se végrehajtani az átmenetet)
• \(L_1\) szinten (aktivizálható): \(\exists\)\(\varsigma\) \(\in\) L(N, \(M_0\)) : t \(\in\) \(\varsigma\)
  (Végrehajtható az átmenet)
• \(L_2\) szinten: \(\forall\)k \(\in \mathbb{N}\) : \(\exists\)\(\varsigma\) \(\in\) L(N,\(M_0\)) : #(\(\varsigma\), t) \(\geq\) k
  (Bármely korlátnál többször végrehajtható az átmenet)
• \(L_3\) szinten: \(\exists\)\(\varsigma\) \(\in\) L(N, \(M_0\)) : #(\(\varsigma\), t) = \(\infty\)
  (Van olyan végrehajtás, melyben tetszőlegesen sokszor végrehajtható az átmenet)
• \(L_4\) szinten: \(\forall\)M \(\in\) R(\(M_0\))-ra a t L1 szinten eleven
  (Minden elérhető állapotban az átmenet aktivizálható)

Szigorúan \(L_k\) eleven: \(L_k\) eleven, de nem \(L_{k+1}\)

Petri háló \(L_k\) eleven: (N, \(M_0\)) \(\forall\)t \(\in\) T : t \(L_k\) eleven

Lefedhetőség:

(N, \(M_0\)) Petri háló esetén az M súlyozás lefedhető, ha \(\exists\)M' \(\in\) R(\(M_0\)) : \(\forall\)p \(\in\) P : M'(p) \(\geq\) M(p)

Petri hálók vizsgálata

Elérhetőségi fa:

(N, \(M_0\)) Petri háló elérhetőségi (végtelen esetben fedési) fája, olyan gráf, amelyben a csúcsok súlyozásokkal vannak címkézve, az élek pedig átmenetekkel.

Konstrukció:

1. új := {\(M_0\)}
2. ciklus, amíg új \(\not=\) \(\oslash\)
   1. M :\(\in\) új, új := új \(\setminus\) {M}
   2. ha M-ig a gyökértől létezik már M címkéjű csúcs \(\Rightarrow\) M régi
   3. ha M-ben nincs aktivizálható átmenet \(\Rightarrow\) M zsákutca
   4. M-ben \(\forall\)t aktivizálható átmenetre kiszámoljuk MtM'-t
      1. Ha a gyökértől M-ig \(\exists\)M'' : M'' -t lefedi M' és M' \(\not=\) M'', akkor minden p \(\in\) M' : M'(p) > M''(p) helyre: M'(p) := \(\omega\)
      2. M' új csúcs: új := új \(\cup\) {M'}, az él címkéje t lesz

Legyen G a (N,M0) Petri háló lefedhetőségi fája.

• Korlátos a Petri háló \(\Leftrightarrow\) ha nincs G-ben \(\infty\) címkéjű csúcs.
• 1-korlátos (biztonságos) \(\Leftrightarrow\) csak 0, 1-es szám szerepel a címkékben.
• t holt (\(L_0\) eleven) \(\Leftrightarrow\) \(\neg\exists\)t él címke a G fedési fában.

Állapotgép: \(\forall\)t \(\in\) T: |•t| = |t•| = 1

Jelzett háló: \(\forall\)p \(\in\) P: |•p| = |p•| = 1

Petri dobozok

Lab - események egy előre megadott halmaza.

Átcímkézés:

\(\rho\) átcímkézés egy reláció:

\(\rho\) \(\subseteq\) (mult(Lab)) × Lab, úgy, hogy (\(\oslash\), \(\alpha\)) \(\in\) \(\rho\) akkor és csak akkor, ha \(\rho\) = {(\(\oslash\), \(\alpha\))}.

Címkézett Petri háló:

\(\Sigma\) = (S, T, W, \(\lambda\), M), ahol

• S a helyek halmaza
• T az átmenetek halmaza (S \(\cap\) T = \(\oslash\))
• W az éleket leíró reláció (W: ((S × T) \(\cup\) (T × S)) → \(N_0\))
• \(\lambda\) a címkefüggvény
  • \(\forall\)s \(\in\) S: \(\lambda\)(s) \(\in\) {e, i, x},
    • \(\lambda\)(s) = e (entry), akkor s belépési hely,
    • \(\lambda\)(s) = x (exit), akkor s kimenő hely,
    • \(\lambda\)(s) = i (internal), akkor s belső hely,
  • \(\forall\)t \(\in\) T: \(\lambda\)(t) egy átcímkézés,
• M a súlyozás (M: S × \(\mathbb{N}_0\))

Címkézett Petri háló

Lépés:

Átmenetek egy véges zsákja U \(\in\) mult(T), (egy lépés) engedélyezett \(\Sigma\)-ban, ha minden helyen van elég súly ahhoz, hogy szimultán végre tudjuk hajtani az összes U-beli átmenetet.

Megjegyzés: Egy lépés nem kell, hogy maximális legyen, például {\(t_0\)} is egy lépése, illetve {\(t_0\)}{\(t_1\)}{\(t_2\)} {\(t_2\)} és {\(t_0\),\(t_2\)}{\(t_1\)}{\(t_2\)} is egy lépéssorozata \(\Sigma_0\)-nak.

T-megszorítás: \(\forall\)t \(\in\) T :• t \(\not=\) \(\oslash\) \(\not=\) t•

ex-megszorítás: létezik legalább egy belépési és egy kilépési hely.

e-irányított háló: \(\Sigma\) e-irányított, ha a belépési helyekhez nem vezet él.

x-irányított háló: \(\Sigma\) x-irányított, ha a kilépési helyekből nem vezet ki él.

ex-irányított háló: \(\Sigma\) ex-irányított, ha e-irányított és x-irányított

Petri doboz

\(\Sigma\) címkézett Petri háló Petri doboz, ha ex-megszorított valamint ex-irányított (és T megszorított).

Operátor doboz

Egy operátor doboz olyan doboz, melynek minden átmenetéhez transzformációs (nem konstans) átcímkézés van rendelve.

Megjegyzés: Az operátor dobozt úgy képzelhetjük el, mint egy mintát, amely sima dobozok egy halmazát (átmenetenként egyet) köt össze a belépési és a kilépési helyeiken keresztül.

Speciális operátor dobozok

• Párhuzamos kompozíció: \(\Omega_{||}\) operátor doboz két teljesen különálló másolatot készít \(\Sigma_1\)-ből és \(\Sigma_2\)-ből.
• Elágazás: \(\Omega_{\square}\) egy elágazásban összekapcsolja \(\Sigma_1\)-et és \(\Sigma_2\)-t.
• Szekvenciális kompozíció: \(\Omega_{;}\) szekvenciálisan összekapcsolja \(\Sigma_1\)-et és \(\Sigma_2\)-t.

Párhuzamos és elosztott rendszerek szemantikai leírásának lehetséges formái

Műveleti szemantika (cimkézett állapotátmentrendszer):

A műveleti szemantika azt mondja meg, hogy milyen lépéseket hajt végre a program, azonban helyesség bizonyítására nem alkalmas.

Nyelvtan:

\[P ::= \text{nil} \ | \ a \ p \ | \ a+p \qquad a,p\in A \text{ - események}\] + : nem determinisztikus választás (kb. szelektív várakozás)

Megjegyzés: vannak levezetési szabályok, de eléggé egyértelműek.

Környezet: \((p,e) \in P \times P\): \(e || p\) - az \(e\) a \(p\) környezete

\(p\) megfelel az \(e\) környezetnek, ha minden esetben: Amikor elakad a lebontás, akkor a környezet =nil kell legyen.

Példák:

1. a b nil + b c nil || a(b nil + c nil) \(\xrightarrow{\text{a}}\)
   b nil || b nil + c nil \(\xrightarrow{\text{b}}\)
   nil || nil

   Ez esetben jobb oldal nil, tehát a program megfelel a környezetnek.

2. a b nil + b c nil || a nil + b(c nil + a nil)

   Jelen esetben két megvizsgálandó ág lesz:

   • a b nil + b c nil || a nil + b(c nil + a nil) \(\xrightarrow{\text{b}}\)
     c nil || c nil + a nil \(\xrightarrow{\text{c}}\)
     nil || nil
   • a b nil + b c nil || a nil + b(c nil + a nil) \(\xrightarrow{\text{a}}\)
     b nil || nil

   A baloldal nem nil, de ez nem jelent problémát, mert a környezet (tehát a jobb oldal) nil lett.

   Tehát ez esetben is megfelel a program a környezetnek.

Leíró szemantika

A leíró szemantika a részprogramok viselkedéséből következtet az összetett programra (program szintézis).

Axiomatikus szemantika

Az axiomatikus szemantikát a programok verifikálásra (helyességellenőrzésre) fejlesztették ki.