I. Teoretická část

Jednotlivá témata projdeme hrubě v rámci videokonference, podpůrný materiál je uveden níže.

Jako studijní text k části této problematiky lze použít opět tutoriál (sekce 5.1, sekce 6.3.2):

Úvod do problematiky stochastických modelů, motivační formalizace pomocí diskrétních markovových řetězců je podán v poslední sekci slidů:

Podrobné vysvětlení upřesněného modelu pomocí markovových řetězců spojitého času je dále podáno v následující presentaci:

Velmi flexibilní a přesná (ale výpočetně náročná) metoda analýzy je pravděpodobnostní model checking implementovaný v nástroji PRISM. Výklad k této problematice je v následující presentaci:

II. Cvičení

1. Převeďte Petriho síť z předchozího cvičení (Snoopy) na stochastickou Petriho síť a doplňte parametry stochastické kinetiky následujícím způsobem:

• k1 = 1 [S + E -> ES]
  
• k2 = 0.5 [ES -> S + E]
  
• k3 = 0.1 [ES -> EP]
  
• k4 = 0.01 [EP -> ES]
  
• k5 = 0.1[EP -> E + P]
  
• k6 = 0.01 [E + P -> EP]
  

2. Nastavte smysluplný iniciální marking (viz doporučení na slide 21 presentace ke Statické analýze z minulé lekce). Proveďte několik stochastických simulací metodou Gillespie v prostředí Snoopy.

3. Nainstalujte nástroj PRISM a převeďte model do jazyka reactive modules tak, aby byl korektně načten v PRISM (funkce build musí proběhnout bez chyby).

4. Pokud jste tak již neučinili v předchozím případě, přepište model do formy komunikujících modulů (každý modul odpovídá právě jedné substanci).

5. Uvazujte vlastnost P=? [ true U<=10 (P > 0) ], uvedomte si vyznam teto vlastnosti v kontextu modelu a zjistete jak se platnost teto vlastnosti meni se zmenou casoveho boundu.