- (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