Notatki do wykªadu

Logiki modalne i temporalne

(cz¦±¢ trzecia - logiki temporalne)

(semestr zimowy 07/08)

Emanuel Kiero«ski

1 LTL - (propositional) Linear Time Logic

1.1 Skªadnia

Podobnie jak w logice modalnej mamy zbiór zmiennych zdaniowych V ar. J¦zyk LTL deniujemy nast¦puj¡co:

ϕ ::= p | ⊥ | > | ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | F ϕ | Gϕ | ϕU ψ | Xϕ

Minimalny zestaw:

ϕ ::= p | ¬ϕ | ϕ ∨ ϕ | ϕU ψ | Xϕ

Skróty: Gϕ = ¬F ¬ϕ, F ϕ = >Uϕ

1.2 Semantyka

Na pocz¡tek okre±lamy semantyk¦ w niesko«czonych modelach liniowych. Dla uproszczenia zakªadamy, »e

dzidzin¡ jest zbiór N. Model to funkcja M : N → 2

V ar

, czyli niesko«czony ci¡g P

0

, P

1

, . . .

podzbiorów V ar.

Deniujemy prawdziwo±¢ ϕ w punkcie modelu i:

(i) M, i |= p i p ∈ M(i)

(ii) M, i |= ¬ϕ i M, i 6|= ϕ

(iii) M, i |= ϕ ∨ ψ i M, i |= ϕ lub M, i |= ψ,

(iv) M, i |= Xϕ i M, i + 1 |= ϕ

(v) M, i |= ϕUψ i ∃k ≥ i : M, k |= ψ oraz ∀i ≥ j < k : M, j |= ϕ

Formuªa jest speªnialna je±li istnieje model M oraz punkt i, takie »e M, i |= ϕ. Poniewa» nasz wariant

mówi tylko o przyszªo±ci mo»emy ªatwo zauwa»y¢, »e ϕ speªnialna i ϕ speªnialna w punkcie 0 pewnego

modelu.

1.3 Automaty Büchi'ego

Denicja, przebieg, warunek akceptacji. Automaty uogólnione.

Twierdzenie 1 Problem niepusto±ci dla automatów (uogólnionych) Büchi'ego jest w NLOGSPACE.

Dowód (szkic) Obserwujemy, »e dowolny przebieg akceptuj¡cy ρ automatu A = (A, G

1

, . . . , G

k

)

na sªowie

w

daje si¦ przerobi¢ na ªadny przebieg akceptuj¡cy ρ

0

, ρ

0

= ρ

1

ρ

2

ρ

2

ρ

2

. . .

na (by¢ mo»e) innym sªowie w

0

. ρ

1

to

fragment ρ do pierwszego wyst¡pienia stanu s z G

1

pojawiaj¡cego si¦ niesko«czenie wiele razy. W ρ

2

wyst¦-

puje podci¡g s

2

, s

3

, . . . , s

k

, s

, taki »e s

i

∈ G

i

. Istnienie ªadnego przebiegu sprawdza si¦ niedeterministycznie

zgaduj¡c kolejne stany (pami¦tamy tylko dwa kolejne, s oraz informacj¦, którego G

i

teraz potrzebujemy). 2

Twierdzenie 2 Klasa j¦zyków rozpoznawalnych przez automaty Büchi'ego jest zamkni¦ta na sum¦, przekrój

i dopeªnianie.

Zamkni¦to±¢ na dopeªnienie jest trudnym wynikiem. Nie podajemy dowodu.

1

1.4 Problem speªnialno±ci dla LTL

Twierdzenie 3 Dla ka»dego ϕ mo»na zbudowa¢ automat uogólniony Büchi'ego A

ϕ

, taki »e j¦zyk akceptowany

przez A

ϕ

skªada si¦ z modeli ϕ.

Szczegóªowy dowód tego twierdzenia (wraz z informacjami o automatach Büchi'ego) mo»na znale¹¢ w

notatkach Madhavana Mukunda:

http://www.cmi.ac.in/madhavan/papers/isical97.html

Konstrukcja z twierdzenia 3 daje automat wielko±ci wykªadniczej wzgl¦dem |ϕ|, a wi¦c, dzi¦ki twierdzeniu

1, mamy zªo»ono±¢ EXPTIME problemu SAT(LTL). Zaobserwowali±my jednak, »e tak naprawd¦, to nie

musimy nigdzie wypisywa¢ caªego automatu. Niepusto±¢ A

ϕ

mo»na sprawdzi¢ konstruuj¡c ±cie»k¦ stanów.

Wystarczy, »e umiemy sprawdzi¢ (w pami¦ci wielomianowej), »e zgadni¦ty zbiór formuª jest atomem (czyli

stanem), sprawdzi¢, czy mi¦dzy kolejnymi dwoma stanami jest mo»liwe przej±cie, sprawdzi¢, czy stan nale»y

do G

i

, itp. Wszystko to w naszym przypadku daje si¦ zrobi¢ bez problemu, st¡d:

Twierdzenie 4 Problem speªnialno±ci dla LTL jest w PSPACE.

1.5 LTL w modelach nieliniowych i model checking

Poj¦cie speªniania formuª LTL mo»na rozszerzy¢ na modele, które nie musz¡ by¢ liniowe. Niech M =
{W, R, L}

, gdzie W - zbiór stanów, R - relacja przej±cia (zakªadamy, »e ∀w∃vRwv), L : W → 2

V ar

. ‘cie»k¡

w M nazywamy niesko«czony ci¡g w

0

, w

1

, . . .

elementów W , taki »e w

i

Rw

i+1

dla wszystkich i. Foruªy LTL

na ±cie»kach wyliczane s¡ w naturalny sposób.

Rozwa»a si¦ dwie wersje denicji speªniania LTL w M:

(i) ϕ speªniona w punkcie w ∈ W i istnieje ±cie»ka zaczynaj¡ca si¦ w w, która speªnia ϕ;

(ii) ϕ speªniona w punkcie w ∈ W i ka»da ±cie»ka zaczynaj¡ca si¦ w w speªnia ϕ;

My przyjmiemy pierwsz¡ wersj¦ denicji. Zauwa»my jednak, »e ϕ jest speªniona w w w sensie (i) i ¬ϕ

nie jest speªniona w w w sensie (ii).

Zauwa»my równie», »e zachodzi nast¦puj¡cy oczywisty fakt:

Fakt 5 Je±li ϕ jest speªnialna, to ϕ jest speªnialna w modelu liniowym.

Problem model checking polega na sprawdzeniu dla danego M, w i ϕ, czy M speªnia ϕ w punkcie w.

Twierdzenie 6 Problem model checking dla LTL jest PSPACE-zupeªny

Dowód Granica górna: redukcja do problemu speªnialno±ci. Pytamy o speªnianie ϕ w punkcie u modelu
M

. Model M zakodujemy w formule ψ i b¦dziemy pyta¢ o speªnialno±¢ formuªy ϕ ∧ ψ.

Wprowadzamy nowe zmienne zdaniowe Q

w

dla ka»dego elementu w ∈ W . Dla Q

w

piszemy formuª¦ ψ

w

,

która mówi:

(i) prawdziwo±c Q

w

poci¡ga prawdziwo±¢ tych zmiennych z ϕ, które nale»¡ do L(w) oraz nieprawdziwo±¢

tych, które nie nale»¡ do L(w);

(ii) prawdziwo±¢ Q

w

implikuje, »e w nast¦pnym stanie prawdziwe jest jakie± Q

v

dla pewnego v, takiego »e

wRv

.

Dodatkowo mówimy formuª¡ ψ

0

, »e w ka»dym stanie prawdziwe jest dokªadnie jedno Q

w

. Ostatecznie:

ψ = Q

u

∧ ψ

0

∧

V

w

Gψ

w

.

Šatwo teraz pokaza¢, »e istnieje ±cie»ka w M, zaczynaj¡ca si¦ w u, speªniaj¡ca ϕ i ϕ ∧ ψ speªnialna.

Granica dolna: kodowanie maszyny Turinga rozwi¡zuj¡cej problem z PSPACE. Na wykªadzie pokazali±my

ide¦ konstrukcji wykorzystuj¡cej tylko operatory X i F (oraz dualny G). Na ¢wiczeniach zobaczymy, »e

PSPACE-trudny jest te» wariant LTL-a jedynie z operatorem U.

2

Wniosek 7 Problem speªnialno±ci dla LTL jest PSPACE-trudny (a zatem, dzi¦ki twierdzeniu 4, tak»e PSPACE-

zupeªny).

2

1.6 LTL(F)

Zbadamy teraz wariant LTL, w którym jedynym operatorem temporalnym jest F (mo»na oczywi±cie u»ywa¢

równie» dualnego do niego G). Udowodnimy:

Twierdzenie 8 Probelm speªnialno±ci dla LTL(F) jest NP-zupeªny

Dowód granicy górnej w poni»szym twierdzeniu opiera si¦ na obserwacji, »e ka»da formuªa speªnialna ma

model liniowy ksztaªtu IRRRR . . ., gdzie I oraz R s¡ wielko±ci liniowej wzgl¦dem dªugo±ci ϕ (lub, inaczej

mówi¡c, model sko«czony skªadaj¡cy si¦ ze ±cie»ki I oraz cyklu R). Konstrukcja jest nast¦puj¡ca:

Niech M = s

0

, s

1

, s

2

, . . .

b¦dzie liniowym modelem ϕ. Zbiory L(s

i

)

nazywa¢ bedziemy typami. Poniewa»

interesuj¡ nas tylko zmienne pojawiaj¡ce si¦ w ϕ mamy maksymalnie wykªadniczo du»o (wzgl¦dem |ϕ|)

typów.

Wyrózniamy w M dwa punkty: s

k−1

- ostatnia realizajca typu wyst¦puj¡cego w M sko«czenie wiele razy

(je±li ka»dy typ jest realizowany niesko«czenie wiele razy, to k = 0); s

l

- taki punkt, »e przedziaª s

k

, . . . , s

l

zawiera realizacje wszystkich typów wyst¦puj¡cych niesko«czenie wiele razy. Fragment s

0

, . . . s

k−1

nazwiemy

fragmentem pocz¡tkowym, fragment s

k

, . . . s

l

fragmentem powtarzanym.

Lemat 9 Je±li i, j ≥ k, to w punktach s

i

i s

j

speªniane s¡ dokªadnie te same formuªy LTL(F).

Lemat 10 M

0

= s

0

, . . . , s

k−1

, s

0
k

, . . . , s

0
l

, s

1
k

, . . . , s

1
l

, s

2
k

, . . . s

2
l

, . . .

, w którym typ s

i
j

jest taki jak typ s

j

w M,

jest modelem ϕ. Co wi¦cej, zbiór formuª speªnianych w punkcie s

i
j

w modelu M

0

jest taki sam jak speªnianych

w M w punkcie s

j

(dla j ≥ k). Zbiory formuª speªniane w punkcie s

j

, dla j < k s¡ równie» w obu modelach

identyczne.

Okazuje si¦, »e w ci¡gu pocz¡tkowym oraz w ci¡gu powtarzanym mo»na zostawi¢ tylko ±wiadków dla

podformuª postaci F ψ. Zapiszmy ϕ w postaci negacyjnej normalnej (negacje zepchni¦te do zmiennych

zdaniowych). Uzyskujemy w ten sposób ϕ

0

. Dla ka»dej podformuªy ϕ

0

postaci F ψ: je±li F ψ jest speªniona

w ci¡gu pocz¡tkowym, to wybieramy maksymalne i < k, takie »e M, s

i

|= F ψ

; je±li F ψ jest speªniona

w ci¡gu powtarzanym, to wybieramy dowolne k ≤ i ≤ l, takie »e M, s

i

|= F ψ

. Elementy z fragmentów

pocz¡tkowego i powtarzanego (z wyj¡tkiem elementu s

0

), które nie zostaªy wybrane wykre±lamy. Zaªó»my,

»e po tej procedurze w ci¡gu pocz¡tkowym pozostaªy s

i

0

, s

i

1

, . . . , s

i

m

, a w powtarzanym: s

i

n

, s

i

n+1

, . . . , s

i

p

.

Lemat 11 M

00

= s

i

0

, s

i

1

, . . . , s

i

m

, s

0
i

n

, s

0
i

n+1

, . . . , s

0
i

p

, s

1
i

n

, s

1
i

n+1

, . . . , s

1
i

p

, . . .

, gdzie typ s

i
j

jest taki sam jak typ

s

j

w M, jest modelem ϕ. Co wi¦cej, zbiór podformuª ϕ speªnianych w punkcie s

i
j

w modelu M

00

jest taki sam

jak speªnianych w M w punkcie s

j

. Zbiory podformuª speªniane w punkcie s

j

s¡ równie» w obu modelach

identyczne.

Algorytm NP polega teraz na zgadni¦ciu maªych wersji fragmentu pocz¡tkowego i fragmentu powtarza-

nego i sprawdzeniu w czasie wielomianowym (lista 11, zadanie 3), czy rzeczywi±cie daj¡ one model ϕ.

Twierdzenie 12 Problem model checking dla LTL(F) jest NP-zupeªny.

Dowód Granica dolna: Kodowanie 3-SAT.

Granica górna (szkic):

•

Szukamy ±cie»ki, na której jest speªniona nasza formuªa ϕ

•

Szukana ±cie»ka jest postaci: IR

1

R

2

. . .

, gdzie I jest minimalnym fragmentem zawieraj¡cym wszystkie

stany pojawiaj¡ce si¦ sko«czenie wiele razy, a R

i

s¡ cyklami zaczynaj¡cym si¦ w tym samym punkcie.

•

Zarówno I jak i R

i

nie musz¡ by¢ proste.

• I

mo»emy wybra¢ krótkie - wystrczy, »e zawiera ±wiadków dla podformuª F ψ oraz ª¡cz¡ce je ±cie»ki

(proste!) - jest wi¦c maksymalnie dªugo±ci |M| · |ϕ|.

•

Zbiór stanów R pojawiaj¡cych si¦ w R

i

generuje silnie spójn¡ skªadow¡ modelu. Kolejno±¢ tych stanów

na ±cie»ce jest nieistotna. Wystarczy wi¦c zgadn¡¢ I, R i sprawdzi¢, czy daj¡ one poprawny model

(oraz czy s¡, odpowiednio, ±cie»k¡ i silnie spójn¡ skªadow¡) - to daje si¦ zrobi¢ w czasie wielomianowym

(Lista 11, zad. 3).

2

3

2 Logiki czasu rozgaª¦zionego

2.1 Denicja CTL* i CTL

Jak zwykle V AR jest zbiorem zmiennych zdaniowych. Wyró»niamy formuªy stanowe oraz ±cie»kowe. Skªad-

nia CTL* jest nast¦puj¡ca:

•

Formuªy stanowe ϕ:

ϕ ::= V AR | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬ϕ | ϕ → ϕ | Eψ | Aψ

•

Formuªy ±cie»kowe ψ:

ψ ::= ϕ | ψ ∧ ψ | ψ ∨ ψ | ψ → ψ | Xψ | ψU ψ | F ψ | Gψ

W przypadku CTL formuªy ±cie»kowe s¡ takie:

•

Formuªy ±cie»kowe ψ w CTL:

ψ ::= Xϕ | ϕU ϕ | F ϕ | Gϕ

CTL jest zatem fragmentem CTL*. Fragmentem CTL* jest tak»e LTL.

CTL mo»na zdeniowa¢ te» po prostu tak (tylko formuªy stanowe):

ϕ ::= P | ϕ ∧ ϕ | ϕ ∨ ϕ | ¬ϕ | EF ϕ | EGϕ | AF ϕ | AGϕ | E(ϕU ϕ) | A(ϕU ϕ) | EXϕ | AXϕ

Niektóre z formuª mo»na traktowa¢ jako skróty. Przykªadowy minimalny zestaw (dla CTL-a):

ϕ ::= V AR | ϕ ∧ ϕ | ¬ϕ | EGϕ | E(ϕU ϕ) | EXϕ

Semantyka CTL* deniowana jest wzgl¦dem struktur Kripkego. Prawdziwo±¢ formuª stanowych denio-

wana jest w stanach, a ±cie»kowych  na ±cie»kach (niesko«czonych). Niech M = (W, R, L) b¦dzie struktur¡

Kripkego. Zakªadamy, »e ∀w ∈ W ∃w

0

∈ W Rww

0

. Dla ±ciezki niesko«czonej π = (s

0

, s

1

, . . .)

przez π

i

oznaczamy ±ciezk¦ (s

i

, s

i+1

, . . .)

• M, s |= P

i P ∈ L(s)

• M, s |= ϕ ∧ ψ

i M, s |= ϕ oraz M, s |= ψ

• M, s |= ¬ϕ

i nieprawda, »e M, s |= ϕ

• M, s |= Eϕ

i istnieje niesko«czona ±cie»ka π = (s, . . .), taka »e M, π |= ϕ

• M, s |= Aϕ

i ka»da niesko«czona ±cie»ka π = (s, . . .) speªnia M, π |= ϕ

• M, π |= ϕ

i M, s |= ϕ dla ϕ stanowych

• M, π |= ϕ ∧ ψ

i M, π |= ϕ oraz M, π |= ψ

• M, π |= ¬ϕ

i nieprawda, »e M, π |= ϕ

• M, π |= ϕU ψ

i istnieje i, takie »e M, π

i

|= ψ

oraz dla wszystkich j < i: M, π

j

|= ϕ

• M, π |= Xϕ

i M, π

1

|= ϕ

Pozostaªe przypadki analogicznie. Semantyka LTL w stanach: formuªa ϕ jest prawdziwa w stanie s, je±li

w s zachodzi Aϕ (tym razem na potrzeby kolejnego podrozdziaªu przyjmujemy inny wariant ni» przy denicji

problemu model checking dla LTL).

2.2 Porównanie mocy CTL*, CTL, LTL

Denition 13 Mówimy, »e dwie formuªy (stanowe) ϕ i ψ w CTL* s¡ równowa»ne je±li dla ka»dego modelu
M

i ka»dego punktu s: M, s |= ϕ i M, s |= ψ. Formuªa (stanowa) CTL* ϕ jest równowa»na formule LTL,

gdy dla ka»dego modelu M i ka»dego punktu s: M, s |= ϕ i M, s |= Aψ.

Poka»emy, »e LTL i CTL s¡ nieporównywalne.

Przykªadowe formuªy w CTL, które nie maj¡ równowa»nych w LTL:

• AF AGP

4

• AF (P ∧ AXP )

• AGEF P

Przykªadowe formuªy w LTL, które nie maj¡ równowa»nych w CTL:

• F GP

• F (P ∧ XP )

Przykªadowa formuªa CTL*, która nie ma równowa»nej ani w CTL ani w LTL:

• AF GP ∨ AGEF Q

2.2.1 Kryterium dla LTL
Dla ϕ w CTL* przez ϕ

d

oznaczamy formuª¦ LTL powstaª¡ z ϕ poprzez usuni¦cie wszystkich kwantykatorów

±cie»kowych E i A.

Twierdzenie 14 [Clarke, Draghicescu] Niech ϕ b¦dzie formuª¡ CTL*. Wtedy: ϕ jest równowa»ne pewnej

formule LTL i ϕ jest równowa»ne ϕ

d

.

2.2.2 Kryterium dla CTL
Rozszerzymy denicj¦ speªniania do struktur Kripkego z ograniczeniami. Struktura ma dodatkowy zbiór F ⊆
2

W

, M = (W, R, L, F). Dla ±cie»ki π oznaczmy przez inf(π) zbiór stanów wyst¦puj¡cych w π niesko«czenie

wiele razy. Semantyk¦ ograniczamy do ±cie»ek, dla których inf(π) ∈ F. Mo»emy (bez straty ogólno±ci)

przyj¡¢, »e wszystkie zbiory w F tworz¡ nietrywialne silnie spójne skªadowe w M. Silnie spójnie skªadowa

jest trywialna tylko, gdy jest singletonem bez p¦telki.

Twierdzenie 15 [Clarke, Draghicescu] Niech M = (W, R, L, F) b¦dzie struktur¡ Kripkego z ogranicze-

niami. Niech M

0

= (W, R, L, F

0

)

b¦dzie taka, »e F

0

= F ∪ F

0

, gdzie F ⊂ F

0

dla pewnego F ∈ F. Wtedy dla

ka»dej formuªy CTL ϕ i ka»dego s ∈ W :

M

, s |= ϕ

i M

0

, s |= ϕ.

2.3 Wªasno±¢ modelu sko«czonego dla CTL

Twierdzenie 16 Ka»da speªnialna formuªa CTL ϕ ma model wykªadniczy wzgl¦dem |ϕ|.

Dowód tego twierdzenia mo»na znale¹¢ w pracy Emersona i Halperna. Ró»ni si¦ on jednak troch¦ od

prezentowanego na wykªadzie.

5