Logika Hennessy-Milnera

Poprzedni rozdział opisywał mo˙zliwo´sci badania równowa˙zno´sci modeli w oparciu o ró˙zne rodzaje bisymulacji. Rozwi ˛azanie takie doskonale nadaje si˛e do badania np. zgodno´sci imple-mentacji danego systemu z jego specyfikacj ˛a. Oba modele mo˙zna swobodnie wyrazi´c w postaci algebry CCS lub innych algebr. Zdarza si˛e jednak, ˙ze w trakcie budowania sytemu dodaje si˛e do niego dodatkow ˛a funkcjonalno´s´c. Posłu˙zenie si˛e w takim przypadku równowa˙zno´sci ˛a obser-wacyjn ˛a b˛edzie w rzeczywisto´sci wymagało skonstruowania nowego modelu systemu (nowej specyfikacji). Dlatego te˙z korzystnym by było posiadanie narz˛edzia umo˙zliwiaj ˛acego spraw-dzenie czy system posiada po˙z ˛adane cechy i wykluczenie istnienia cech negatywnych.

Przykładem cechy pozytywnej mo˙ze by´c „ka˙zdorazowe potwierdzanie otrzymanego pakie-tu przez odbiornik”. Przykładem cechy negatywnej mo˙ze by´c „zatrzymanie systemu”. Pytania w ten sposób sformułowane mog ˛a by´c trudne do wyra˙zenia lub nawet niemo˙zliwe w postaci modelu w algebrze procesów ([1, 17]).

W pracy [31] Hennessy i Milner zaproponowali j˛ezyk, który pozwala na uzyskanie odpo-wiedzi na pytania formułowane w sposób przedstawiony powy˙zej. J˛ezyk ten nazwany został logik ˛a Hennessy-Milnera (HML). Stanowi on doskonałe uzupełnienie równowa˙zno´sci opartej o bisymulacj˛e w weryfikacji modelowej.

Definicja 13. Zbiór wszystkich wyra˙ze´n M logiki Hennessy-Milnera na zbiorze akcji Act de-finiowany jest indukcyjnie zgodnie z nast˛epuj ˛acymi regułami konstrukcji:

(1) tt, ff ∈ M;

Ponadto, je´sli A = {a1, . . . , an} ⊆ Act, (n ≥ 0), to przyjmuje si˛e nast˛epuj ˛ace skróty: • ha₁iF ∨ . . . ∨ ha_niF ⇔ hAiF ,

• ha1iF ∧ . . . ∧ haniF ⇔ [A]F .

Dodatkowo, je´sli A = ∅, to hAiF = tt ∧ [A]F = ff .

Semantyka formuł jest ´sci´sle zwi ˛azana z etykietowanym systemem przej´s´c (zob. def. 2) generowanym przez proces. Znaczenie formuł j˛ezyka M polega na opisie zbioru procesów, które je spełniaj ˛a. Mo˙zna je rozumie´c w nast˛epuj ˛acy sposób:

• wszystkie procesy spełniaj ˛a tt, • ˙zaden proces nie spełnia ff ,

• proces spełnia F ∧ G wtw., je´sli spełnia F i spełnia G, • proces spełnia F ∨ G wtw., je´sli spełnia F lub spełnia G,

• proces spełnia haiF dla pewnego a ∈ Act wtw., je´sli pozwala na tranzycj˛e a prowadz ˛ac ˛a do stanu spełniaj ˛acego F ,

• proces spełnia [a]F dla pewnego a ∈ Act wtw., je´sli dla ka˙zdej tranzycji a prowadzi do stanu spełniaj ˛acego F .

Zbiór stanów spełniaj ˛acych formuł˛e F logiki Hennessy-Milnera zapisuje si˛e jakoJF K i de-finiuje formalnie jak poni˙zej.

Definicja 14. JF K ⊆ P roc dla F ∈ M okre´sla zbiór stanów, w których formuła F jest speł-niona i zdefiniowany jest jak nast˛epuje:

• JttK = P roc, • Jff K = ∅, • JF ∧ GK = JF K ∩ JGK, • JF ∨ GK = JF K ∪ JGK, • JhaiF K = h·a·iJF K, • J[a]F K = [·a·]JF K,

gdzie h·a·i, [·a·] : 2^{P roc}→ 2P roczdefiniowane s ˛a jak poni˙zej: • h·a·iS = {p ∈ P roc : ∃p0 p−→ p^a 0 ∧ p0 ∈ S},

• [·a·]S = {p ∈ P roc : ∀p0 p−→ p^a 0 ⇒ p0 ∈ S}.

Fakt, ˙ze proces p spełnia formuł˛e logiki Hennessy-Milnera F zapisuje si˛e jako p  F . Stosuje si˛e tak˙ze zapis p 2 F i oznacza on, ˙ze p nie spełnia F . Posługuj ˛ac si˛e oraz def. 14 poda´c mo˙zna zwi ˛azki prezentowane w równaniu (3.29).

p  tt dla ka˙zdego p ∈ P roc (3.29a)

p  ff dla ˙zadnego p ∈ P roc (3.29b)

p  F ∧ G wtw., je˙zeli p  F i p  G (3.29c) p  F ∨ G wtw., je˙zeli p  F lub p  G (3.29d) p  haiF wtw., je˙zeli p −→ p^{a 0} dla pewnego p⁰ ∈ P roc takiego, ˙ze p⁰  F (3.29e) p  [a]F wtw., je˙zeli p⁰  F dla ka˙zdego p⁰ ∈ P roc takiego, ˙ze p −→ p^{a 0} (3.29f) Zale˙zno´s´c pomi˛edzy operatorem oraz J_K przedstawia twierdzenie 3, natomiast twierdze-nie 4 pokazuje relacj˛e mi˛edzy logik ˛a Hennessy-Milnera a siln ˛a bisymulacj ˛a.

Twierdzenie 3. Niech (P roc, Act, {−→ : a ∈ Act}) b˛edzie etykietowanym systemem przej´s´c,^a p ∈ P roc i F ∈ M. Wtedy:

p  F ⇐⇒ p ∈ JF K. (3.30)

Twierdzenie 4. Niech (P roc, Act, {−→ : a ∈ Act}) b˛edzie sko´nczenie-przej´sciowym (image-^a finite) etykietowanym systemem przej´s´c² i p, q ∈ P roc. Wtedy

p ∼ q ⇐⇒ ∀F ∈ M : (p  F ⇔ q  F ). (3.31) Dla formuł logiki Hennessy-Milnera F definiuje si˛e formuły F^C, które s ˛a odpowiednikiem ich negacji. Spełnione s ˛a tak˙ze nast˛epuj ˛ace zale˙zno´sci:

ttC = ff (3.32a)

ff^C = tt (3.32b)

(F ∧ G)^C = F^C∨ G^C (3.32c) (F ∨ G)C = F^C∧ GC (3.32d)

(haiF )C = [a]F^C (3.32e)

([a]F )C = haiF^C (3.32f)

Rozwa˙zmy przykład prezentuj ˛acy procedur˛e parzenia kawy – jeden ze sposobów. Do kubka wsypujemy kaw˛e, wlewamy gor ˛ac ˛a wod˛e potem cukier. Formalnie wy˙zej wymienion ˛a proce-dur˛e mo˙zna zapisa´c nast˛epuj ˛aco:

agent KC = kawa.woda.cukier.0 (3.33)

Wykorzystuj ˛ac logik˛e Hennessy-Milnera i pozostaj ˛ac przy semantyce przykładu mo˙zemy teraz zapyta´c: „Czy parzenie kawy rozpoczyna si˛e od wsypania kawy?”. Zapis matematyczny tego pytania prezentuje wzór (3.34). Innymi słowy pytamy: „Czy proces KC reprezentuj ˛acy procedur˛e parzenia kawy rozpoczyna si˛e od akcji kawa?”.

hkawaitt (3.34)

Odpowied´z na pytanie wyra˙zone w równaniu (3.34) jest twierdz ˛aca i łatwo to udowodni´c wykorzystuj ˛ac definicj˛e semantyki operatora h_iF oraz tt. Podobnie mo˙zna zapyta´c: „Czy naj-pierw wsypujemy kaw˛e a potem dolewamy wody czy odwrotnie?”. Formuły przyjm ˛a wtedy posta´c:

[kawa]hwodaitt (3.35a)

[woda]hkawaitt (3.35b)

Niektóre osoby pij ˛a kaw˛e z mlekiem. Dla nich przepis na kaw˛e wygl ˛ada nast˛epuj ˛aco:

agent KCM = kawa.woda.cukier.mleko.0 (3.36)

Stworzy´c te˙z mo˙zna zbiór przepisów na kaw˛e:

agent K = KC + KCM (3.37)

Zapytanie „Czy agent K mo˙ze osi ˛agn ˛a´c stan mleko?” czy innymi słowy „Czy w przepisach na kaw˛e jest kawa zawieraj ˛aca mleko?” byłby ju˙z nieco kłopotliwy. Łatwo sobie wyobrazi´c

przykłady, gdzie ci ˛ag zdarze´n prowadz ˛acych do interesuj ˛acego fragmentu jest znacznie dłu˙zszy lub nawet niesko´nczony. Jednym z rozwi ˛aza´n takiego problemu jest zastosowanie formuł logiki H-M z niesko´nczonymi koniunkcjami lub dysjunkcjami. Takie wyj´scie jednak jest niezwykle niewygodne lub niemo˙zliwe do implementacji. St ˛ad logika Hennesy-Milnera rozszerzona zo-stała o rekurencj˛e, która to takich wad nie posiada. Zapytanie o dost˛epno´s´c przepisu na kaw˛e zawieraj ˛ac ˛a mleko mo˙zna rekurencyjnie zapisa´c nast˛epuj ˛aco:

X ≡ hmlekoitt ∨ h−iX (3.38)

Zapis ten mo˙zna odczyta´c jako: „Proces pozwala na tranzycj˛e mleko teraz lub w której´s z na-st˛epnych tranzycji” (− oznacza tranzycj˛e o dowolnej etykiecie).

Formalna definicja logiki Hennessy-Milnera z jedn ˛a zmienn ˛a X wygl ˛ada nast˛epuj ˛aco:

Definicja 15. Zbiór wszystkich wyra˙ze´n M{X}logiki Hennessy-Milnera z jedn ˛a zmienn ˛a X na zbiorze akcji Act definiowany jest indukcyjnie zgodnie z nast˛epuj ˛acymi regułami konstrukcji:

(1) tt, ff , X ∈ M;

(2) Je˙zeli wyra˙zenia F, G ∈ M i a ∈ Act, to równie˙z F ∧ G, F ∨ G, haiF i [a]F nale˙z ˛a do M.

Formuła F , ewentualnie zawieraj ˛aca zmienn ˛a X, jest interpretowana jako funkcja OF: 2^{P roc} → 2P roc, która dany zbiór procesów, z zało˙zenia spełniaj ˛acy X, transformuje w zbiór procesów, które spełniaj ˛a F . Szczegółowy opis definicji funkcji OF wraz dowodami istnienia rozwi ˛aza´n bazuj ˛acymi na twierdzeniu Knastera-Tarskiego o punkcie stałym znajduje si˛e w pra-cy [1].

Semantyka zmienej X jest nast˛epuj ˛aca:

Je´sli X ^max= F_X toJXK = S S ⊆ P roc | S ⊆ OFX(S) (3.39a) Je´sli X ^min= F_X toJXK = T S ⊆ P roc | OFX(S) ⊆ S (3.39b) Symbole^max= oraz ^min= odnosz ˛a si˛e do maksymalnego i minimalnego rozwi ˛azania i wyni-kaj ˛a z twierdzenia Knastera-Tarskiego. Maksymalne rozwi ˛azanie u˙zywa si˛e do tych własno´sci, które s ˛a spełnione, chyba ˙ze pojawia si˛e sko´nczona ilo´s´c przypadków, która temu przeczy. Roz-wi ˛azanie minimalne u˙zywane jest do własno´sci, które spełniaj ˛a proces, je´sli sko´nczona ilo´s´c przypadków to potwierdza.

Rozwa˙zmy przykładowe procesy zdefiniowane równaniami (3.40).

A = a.A (3.40a)

B = a.B + a.0 (3.40b)

Zapytanie o to czy procesy te mog ˛a zawsze wykona´c tranzycj˛e a mo˙ze wygl ˛ada´c jak w rów-naniu (3.41). Zapytanie o rozwi ˛azanie maksymalne jest konsekwencj ˛a u˙zycia „zawsze” w za-pytaniu.

X ^max= haitt ∧ [a]X (3.41)

Bardziej ogólnie formuł˛e, która sprawdza czy dana własno´s´c F jest spełniana w ka˙zdym z osi ˛agalnych stanów (Inv(F )) mo˙zna zapisa´c jako:

X ^max= F ∧ [−]X (3.42)

Podobnie mo˙zna zdefiniowa´c formuł˛e, która b˛edzie sprawdza´c czy dana własno´s´c jest speł-niana przez chocia˙z jeden z osi ˛agalnych procesów (P os(F )):

Posługuj ˛ac si˛e powy˙zszym schematem definiowa´c mo˙zna inne operatory jak cho´cby „bez-piecze´nstwo”, „ostatecznie” itp. Kilka przykładów zaprezentowano we wzorach (3.44).

Safe X ^max= F ∧ ([−]ff ∨ h−iX) (3.44a) Even X ^min= F ∨ (h−itt ∧ [−]X) (3.44b) F US G X ^max= G ∨ (F ∧ [−]X) (3.44c) F UW G X ^min= G ∨ (F ∧ h−itt ∧ [−]X) (3.44d) Własno´s´c (3.44a) jest spełniona przez proces, który posiada zupełn ˛a sekwencj˛e tranzycji oraz ka˙zdy ze stanów spełnia F . Proces spełnia własno´s´c (3.44b), je´sli ka˙zda pełna sekwen-cja tranzycji spełnia cho´c w jednym punkcie własno´s´c F . Własno´s´c (3.44c) okre´slana jest jako „silne dopóki” („strong until”). Okre´sla ona, ˙ze własno´s´c F musi by´c spełniona a˙z do tranzycji kiedy własno´s´c G stanie si˛e prawd ˛a. Równanie (3.44d) okre´sla własno´s´c nazywan ˛a „słabe do-póki” („weak until”) i spełniona jest wtedy, je´sli F jest spełniona a˙z do stanu kiedy G staje si˛e spełnione, z tym ˙ze mo˙ze to nie nast ˛api´c.

Rekurencyjne definicje własno´sci mog ˛a by´c zagnie˙zd˙zone. Obliczanie zbiorów spełniaj ˛ a-cych dan ˛a własno´s´c odbywa si˛e od tych najbardziej do najmniej zagnie˙zd˙zonych.