Lista4.ps

Automaty zna Weryka ja Lista zada« nr 5

1. Podaj reprezenta j w posta i OBDD funk ji wyli z reprezenta j OBDD funk ji 2. Rozwa»my nastpuj¡ ¡ struktur

a∨b i a∨c. (a ∨ b) ∧ (a ∨ c).

U»ywaj¡ algorytmu z wykªadu

M = ({l0 , l1 , l2 , l3 }, →, L)

GFED @A @ABC GFED l0 O

GFED @ABC / l1

,  @ABC GFED l2 o ED @ABC

GFED @ABC l3 o

AP = {atl0 , atl1 , atl2 , atl3 } i L(l0 ) = {atl0 }, . . . , L(l3 ) = {atl3 }. Zakoduj stany l0 , . . . , l3 jako wektory boolowskie 00, 01, 10, 11. Podaj funk j boolowsk¡ f (v0 , v1 , v0′ , v1′ ) gdzie

reprezentuj¡ ¡ rela j przej± ia w tej strukturze i jej reprezenta j w posta i OBDD. Podaj reprezenta j w posta i OBDD zbioru stanów speªniaj¡ y h

EG(¬atl0 ).

3. Podaj algorytm symboli znego sprawdzania modelu dla logiki CTL, zyli algorytm, który dla podanej na wej± iu struktury Kripkego reprezentuj¡ y zbiór ty h stanów

M,

M

i formuªy

które speªniaj¡

ϕ

logiki CTL wyzna zy OBDD

ϕ.

4. Uogólnij algorytm z poprzedniego zadania tak, aby uwzgldni¢ wizy u z iwo± i (fairness): dla danej rodziny zbiorów

F ⊆ 2S

na kazdym etapie obli ze« uwzgldnij te i tylko

te ± ie»ki, na który h stany z ka»dego ze zbiorów z 5. Wyra¹

F

wystpuj¡ niesko« zenie wiele razy.

EGFair ϕ (istnieje u zwiwa ± ie»ka, na której zawsze jest speªniona formuªa ϕ) jako

punkt staªy pewnej fuk ji (wskazówka: potrzebne bdzie zagnie»d»enie dwó h punktów staªy h).