5.1.2022 [NSWI101] Modely a verifikace chování systémů

1. Je zadán obrázek LTS s dvěma vyznačenými stavy $u$ a $v$. Rozhodněte zda:

2. $u \le_t v$

3. $v \le_t u$

4. $u \le_s v$

5. $v \le_s u$

6. $u \sim v$

7. Rozhodněte zda jsou následující dvě LTL formule ekvivalentní:

• $\mathrm{FX}\,p$

• $\mathrm{F}\,p$

3. Rozhodněte zda jsou následující dvě formule ekvivalentní:

• $\mathrm{GF}\,p$ (LTL)

• $\mathrm{AGEF}\,p$ (CTL)

4. Máme CTL formuli $f = \mathrm{AX}[\mathrm{E}(\neg p \, \mathrm{U} \, r)]$ a Kripkeho strukturu $M$ (zadána obrázkem). Pro každý stav určete formule, které jsou přirazeny na konci běhu algoritmu pro explicitní model checking.

5. Znázorněte pomocí optimálního OBDD relaci $R = \{ (2,1), (2,3), (3,1), (3,3) \}$.

6. (Je dána Kripkeho struktura obrázkem.) Vytvořte odpovídající ekvivalentní strukturu pro následující datovou abstrakci mapující atomické prepozice do abstraktní domény.
   $$x = 0 \rightarrow \neg P \quad \quad y = 0 \rightarrow \neg Q$$
   $$x = 1 \rightarrow \neg P \quad \quad y = 1 \rightarrow \neg Q$$
   $$x = 2 \rightarrow \neg P \quad \quad y = 2 \rightarrow Q$$
   $$x = 3 \rightarrow P \quad \quad \, \, \, \, y = 3 \rightarrow Q$$
   $$x = 4 \rightarrow P$$
   $$x = 5 \rightarrow P$$

7. Rozhodněte pro které $x \in [ 0,1 ]$ platí pro počáteční stav DTMC (zadán obrázkem) funkce $f = \mathrm{P}_{x}[ F^{\le 3} \, \, \mathrm{succ} ]$ (PCTL)

8. Pro (na obrázku zadaný) timed automat nakreslete region automat.

P. S. vypadá to, že Kofroň má pouze tuto jednu písemku

Ahoj,
díky moc za to, že sis dal/a práci to sem napsat. Moc jsi mi pomohl/a :D

Dostali jsme 14.1.2022 to samé, pouze v 3. a 4. byly vyměněny formule.

• $\mathrm{GFX}\, p$

• $\mathrm{GX}\, p$

• $\mathrm{FG}\, p$

• $\mathrm{AFAG}\, p$

Zadání z 2.7.2023 stejné jako z 14.1.2022.

Poznámka k úkolu 1: Ten graf je docela složitý a taky jsou v něm cykly, takže je to o dost těžší než ty úkoly na cviku.