5.1.2022 [NSWI101] Modely a verifikace chování systémů
Napsal: 5. 1. 2022 22:44
1. Je zadán obrázek LTS s dvěma vyznačenými stavy a . Rozhodněte zda:
5. Znázorněte pomocí optimálního OBDD relaci .
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é platí pro počáteční stav DTMC (zadán obrázkem) funkce (PCTL)
8. Pro (na obrázku zadaný) timed automat nakreslete region automat.
P. S. vypadá to, že Kofroň má pouze tuto jednu písemku
- (LTL)
- (CTL)
5. Znázorněte pomocí optimálního OBDD relaci .
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é platí pro počáteční stav DTMC (zadán obrázkem) funkce (PCTL)
8. Pro (na obrázku zadaný) timed automat nakreslete region automat.
P. S. vypadá to, že Kofroň má pouze tuto jednu písemku