od awk » 5. 1. 2022 22:44
1. Je zadán obrázek LTS s dvěma vyznačenými stavy
a
. Rozhodněte zda:
2. Rozhodněte zda jsou následující dvě LTL formule ekvivalentní:
3. Rozhodněte zda jsou následující dvě formule ekvivalentní:
(LTL)
(CTL)
4. Máme CTL formuli
![f = \mathrm{AX}\[\mathrm{E}\(\neg p \, \mathrm{U} \, r\)\]](http://latex.codecogs.com/gif.latex?f = \mathrm{AX}\[\mathrm{E}\(\neg p \, \mathrm{U} \, r\)\])
a Kripkeho strukturu
(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
, (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.
7. Rozhodněte pro které
![x \in \[ 0,1 \]](http://latex.codecogs.com/gif.latex?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} \]](http://latex.codecogs.com/gif.latex?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
1. Je zadán obrázek LTS s dvěma vyznačenými stavy [LaTeX]u[/LaTeX] a [LaTeX]v[/LaTeX]. Rozhodněte zda:
[list=a]
[*][LaTeX]u \le_t v[/LaTeX]
[*][LaTeX]v \le_t u[/LaTeX]
[*][LaTeX]u \le_s v[/LaTeX]
[*][LaTeX]v \le_s u[/LaTeX]
[*][LaTeX]u \sim v[/LaTeX]
[/list]
2. Rozhodněte zda jsou následující dvě LTL formule ekvivalentní:
[list]
[*][LaTeX]\mathrm{FX}\,p[/LaTeX]
[*][LaTeX]\mathrm{F}\,p[/LaTeX]
[/list]
3. Rozhodněte zda jsou následující dvě formule ekvivalentní:
[list]
[*][LaTeX]\mathrm{GF}\,p[/LaTeX] (LTL)
[*][LaTeX]\mathrm{AGEF}\,p[/LaTeX] (CTL)
[/list]
4. Máme CTL formuli [LaTeX]f = \mathrm{AX}\[\mathrm{E}\(\neg p \, \mathrm{U} \, r\)\][/LaTeX] a Kripkeho strukturu [LaTeX]M[/LaTeX] (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 [LaTeX]R = \{ (2,1), (2,3), (3,1), (3,3) \}[/LaTeX].
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.
[LaTeX]x = 0 \rightarrow \neg P \quad \quad y = 0 \rightarrow \neg Q[/LaTeX]
[LaTeX]x = 1 \rightarrow \neg P \quad \quad y = 1 \rightarrow \neg Q[/LaTeX]
[LaTeX]x = 2 \rightarrow \neg P \quad \quad y = 2 \rightarrow Q[/LaTeX]
[LaTeX]x = 3 \rightarrow P \quad \quad \, \, \, \, y = 3 \rightarrow Q[/LaTeX]
[LaTeX]x = 4 \rightarrow P[/LaTeX]
[LaTeX]x = 5 \rightarrow P[/LaTeX]
7. Rozhodněte pro které [LaTeX]x \in \[ 0,1 \][/LaTeX] platí pro počáteční stav DTMC (zadán obrázkem) funkce [LaTeX]f = \mathrm{P}_{x}\[ F^{\le 3} \, \, \mathrm{succ} \][/LaTeX] (PCTL)
8. Pro (na obrázku zadaný) timed automat nakreslete region automat.
P. S. vypadá to, že Kofroň má pouze tuto jednu písemku