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

awk · Příspěvek od **awk** » 5. 1. 2022 22:44

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

$u \le_t v$
$v \le_t u$
$u \le_s v$
$v \le_s u$
$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

hitotsu · Příspěvek od **hitotsu** » 14. 1. 2022 12:40

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

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$

Lazybug478 · Příspěvek od **Lazybug478** » 7. 2. 2023 15:38

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.

Fórum studentů MFF UK

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

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

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

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