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

<{ForumPost(poster="awk", timestamp=2022-01-05 22:44:53)}>
1. Je zadán obrázek LTS s dvěma vyznačenými stavy $u$ a $v$. Rozhodněte zda: 

1. $u \le_t v$
1. $v \le_t u$
1. $u \le_s v$
1. $v \le_s u$
1. $u \sim v$

2. 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
<{/ForumPost}>

<{ForumPost(poster="hitotsu", timestamp=2022-01-14 12:40:48)}>
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.  
  
3.

*  $\mathrm{GFX}\, p$
*  $\mathrm{GX}\, p$

4.

*  $\mathrm{FG}\, p$
*  $\mathrm{AFAG}\, p$

<{/ForumPost}>

<{ForumPost(poster="Lazybug478", timestamp=2023-02-07 15:38:01)}>
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.
<{/ForumPost}>