Matfyz Wiki

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

awk at 2022-01-05 22:44:53

  1. Je zadán obrázek LTS s dvěma vyznačenými stavy u{: alt="u" type="image/"} a v{: alt="v" type="image/"}. Rozhodněte zda:

  2. u \le_t v{: alt="u \le_t v" type="image/"}

  3. v \le_t u{: alt="v \le_t u" type="image/"}

  4. u \le_s v{: alt="u \le_s v" type="image/"}

  5. v \le_s u{: alt="v \le_s u" type="image/"}

  6. u \sim v{: alt="u \sim v" type="image/"}{: style="list-style-type:lower-alpha"}

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

  • \mathrm{FX},p{: alt="\mathrm{FX},p" type="image/"}

  • \mathrm{F},p{: alt="\mathrm{F},p" type="image/"}

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

  • \mathrm{GF},p{: alt="\mathrm{GF},p" type="image/"} (LTL)

  • \mathrm{AGEF},p{: alt="\mathrm{AGEF},p" type="image/"} (CTL)

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

  2. Znázorněte pomocí optimálního OBDD relaci R = { (2,1), (2,3), (3,1), (3,3) }{: alt="R = { (2,1), (2,3), (3,1), (3,3) }" type="image/"}.

  3. (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{: alt="x = 0 \rightarrow \neg P \quad \quad y = 0 \rightarrow \neg Q" type="image/"}
    x = 1 \rightarrow \neg P \quad \quad y = 1 \rightarrow \neg Q{: alt="x = 1 \rightarrow \neg P \quad \quad y = 1 \rightarrow \neg Q" type="image/"}
    x = 2 \rightarrow \neg P \quad \quad y = 2 \rightarrow Q{: alt="x = 2 \rightarrow \neg P \quad \quad y = 2 \rightarrow Q" type="image/"}
    x = 3 \rightarrow P \quad \quad , , , , y = 3 \rightarrow Q{: alt="x = 3 \rightarrow P \quad \quad , , , , y = 3 \rightarrow Q" type="image/"}
    x = 4 \rightarrow P{: alt="x = 4 \rightarrow P" type="image/"}
    x = 5 \rightarrow P{: alt="x = 5 \rightarrow P" type="image/"}

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

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

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

hitotsu at 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.

  • \mathrm{GFX}, p{: alt="\mathrm{GFX}, p" type="image/"}

  • \mathrm{GX}, p{: alt="\mathrm{GX}, p" type="image/"}

  • \mathrm{FG}, p{: alt="\mathrm{FG}, p" type="image/"}

  • \mathrm{AFAG}, p{: alt="\mathrm{AFAG}, p" type="image/"}

Lazybug478 at 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.