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

Co se jinam nevejde
Uživatelský avatar
awk
Matfyz(ák|ačka) level II
Příspěvky: 56
Registrován: 21. 5. 2018 18:54
Typ studia: Informatika Bc.

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

Příspěvek od awk »

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
  2. v \le_t u
  3. u \le_s v
  4. v \le_s u
  5. 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

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

Příspěvek od hitotsu »

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
Lazybug478

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

Příspěvek od Lazybug478 »

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.
Odpovědět

Zpět na „Ostatní“