Logika modalna µ

Rachunek µ ([29]) jest przykładem logiki modalnej czasu rozgał˛ezionego i mo˙ze by´c traktowany jako rozszerzenie logiki CTL (Computation Tree Logic, [14], [15], [16]) o operatory najmniejszego (µ) i najwi˛ekszego (ν) punktu stałego. Wersja rachunku µ u˙zywana w pakiecie CADP okre´slana jest jako regular alternation-free µ-calculus [32]. Wyklucza ona pewne zale˙zno´sci rekurencyjne mi˛edzy operatorami µ i ν, przez co mo˙zliwe jest zastosowanie do sprawdzania spełnialno´sci formuł algorytmów o zło˙zono´sci liniowej.

W poni˙zszym rozdziale zakładamy, ˙ze etykietowany system przej´s´c (graf LTS) jest definiowany jako czwórka LTS = (Γ, A, →, s0), tzn. w porównaniu do definicji 2.1 (patrz str. 15) jawnie wska-zywany jest stan pocz ˛atkowy s0.

Własno´sci w logice modalnej µ s ˛a wyra˙zane jako tzw. formuły stanu. Do podania definicji for-muł stanu konieczne jest zdefiniowanie ich elementów składowych, którymi s ˛a formuły regularne i formuły akcji. St ˛ad te˙z opis składni rachunku µ rozpoczniemy od tych ostatnich.

Gramatyk˛e formuł akcji przedstawiono na listingu 5.1. Formuł ˛a akcji jest dowolna akcja ze zbioru A, co na listingu zapisano jako"string". Warto zwróci´c uwag˛e, ˙ze metody weryfikacji dost˛epne w programie CADP evaluator s ˛a zorientowane na przej´scia realizowane przez model, za´s stany modelu s ˛a reprezentowane wył ˛acznie przez swoje numery porz ˛adkowe. Nazwy akcji podaje si˛e w podwójnych cudzysłowach. Zamiast nazwy akcji mo˙zna podawa´c wyra˙zenie regularne zgodne z POSIX Regular Expressions. Wyra˙zenia regularne podaje si˛e w pojedynczych cudzysłowach. Do-st˛epne s ˛a m.in. poni˙zsze konstrukcje, które mo˙zna u˙zy´c w wyra˙zeniach regularnych.

– x – dopasowanie do znaku x, przy zało˙zeniu, ˙ze x nie ma specjalnego znaczenia;

5.1. Logika modalna µ 83

– [znaki] – dopasowanie do jednego ze znaków wymienionych na li´scie;

– [^znaki] – dopasowanie do dowolnego znaku spoza listy;

– [z1-z2] – dopasowanie do dowolnego znaku z podanego zakresu;

– \k – dopasowanie do symbolu specjalnego k traktowanego jako zwykły znak, np. \. oznacza kropk˛e;

– * – okre´slenie krotno´sci (0 lub wi˛ecej wyst ˛apie´n danego znaku).

Listing 5.1: Zapis formuł akcji w pakiecie CADP

A ::= "string" | ’regexp’ | true | false | not A | A1 or A2 | A1 and A2 | A1 implies A2 | A1 equ A2

Formułami akcji s ˛a równie˙z stałe logicznetrueifalse. Ponadto, je˙zeli przyjmiemy, ˙ze sym-bole A, A1iA2 oznaczaj ˛a formuły akcji, to bardziej zło˙zone formuły mo˙zemy budowa´c stosuj ˛ac klasyczne operatory logiczne:not(nagacja),or(alternatywa),and(koniunkcja),implies (impli-kacja) iequ(równowa˙zno´s´c).

Interpretacj ˛aformuły akcjiAjest podzbiór A, tj. zbiór akcji, które spełniaj ˛a formuł˛eA. Interpre-tacja formuły jest definiowana nast˛epuj ˛aco:

– Wszystkie akcje spełniaj ˛a formuł˛etrue.

– ˙Zadna akcja nie spełnia formułyfalse.

– Formuł˛e"a", gdzie a ∈ A spełnia tylko akcja a.

– Formuł˛enot Aspełniaj ˛a wszystkie akcje, które nie spełniaj ˛a formułyA.

– Formuł˛eA1 or A2spełniaj ˛a wszystkie akcje, które spełniaj ˛a formuł˛eA1lubA2.

– Formuł˛eA1 and A2spełniaj ˛a wszystkie akcje, które spełniaj ˛a formuł˛eA1iA2.

– Formuł˛eA1 implies A2spełniaj ˛a wszystkie akcje, które nie spełniaj ˛a formułyA1lub speł-niaj ˛a formuł˛eA2.

– Formuł˛eA1 equ A2spełniaj ˛a wszystkie akcje, które spełniaj ˛a formuł˛eA1iA2lub nie speł-niaj ˛a ˙zadnej z nich.

5.1. Logika modalna µ 84

Listing 5.2: Zapis formuł regularnych w pakiecie CADP

R ::= A | nil | R1 . R2 | R1 | R2 | R* | R+

Gramatyk˛e formuł regularnych przedstawiono na listingu 5.2. Formuł ˛a regularn ˛a jest dowolna formuła akcjiAoraz formuła pustanil. Ponadto, je˙zeliR,R1iR2oznaczaj ˛a formuły regularne, to bardziej zło˙zone formuły mo˙zemy budowa´c stosuj ˛ac operatory: konkatenacji (kropka), wyboru (|), domkni˛ecia zwrotno-przechodniego(*) i domkni˛ecia przechodniego (+). Najwy˙zszy priorytet maj ˛a operatory_*i+, kolejny jest operator|, a najni˙zszy priorytet ma operator kropka. W razie potrzeby mo˙zna stosowa´c nawiasy okr ˛agłe do zmiany kolejno´sci wykonywania operatorów.

Interpretacj ˛aformuły regularnejRjest relacja okre´slona w zbiorze Γ. Para stanów (s, s⁰) nale-˙z ˛aca do takiej relacji oznacza, ˙ze od stanu s mo˙zna przej´s´c do s⁰ w taki sposób, ˙ze zrealizowany w tym celu ci ˛ag akcji spełnia formuł˛eR.

– Formuła regularnaA, gdzieAjest jednocze´snie formuł ˛a akcji charakteryzuje ci ˛agi akcji o dłu-go´sci 1 takie, ˙ze jedyna akcja wyst˛epuj ˛aca w takim ci ˛agu spełniaA.

– Formuła regularnanilcharakteryzuje ci ˛agi akcji o długo´sci 0.

– Formuła regularnaR1 . R2charakteryzuje ci ˛agi akcji, które s ˛a sklejeniem dwóch ci ˛agów, z których pierwszy spełniaR1, a drugiR2.

– Formuła regularnaR1 | R2charakteryzuje ci ˛agi akcji, które spełniaj ˛aR1lubR2.

– Formuła regularnaR*charakteryzuje ci ˛agi akcji, które s ˛a sklejeniem zero lub wi˛ekszej liczby ci ˛agów spełniaj ˛acychR.

– Formuła regularnaR+ charakteryzuje ci ˛agi akcji, które s ˛a sklejeniem jednego lub wi˛ekszej liczby ci ˛agów spełniaj ˛acychR.

Gramatyk˛e formuł stanu przedstawiono na listingu 5.3. SymbolemRoznaczono formuł˛e regu-larn ˛a,F,F1iF2oznaczaj ˛a formuły stanu, za´sXoznacza zmienn ˛a, której warto´sci ˛a jest zbiór stanów (podzbiór Γ).

Formułami stanu s ˛a stałe logicznetrueifalseoraz dowolna zmienna, przyjmuj ˛aca jako war-to´s´c zbiór stanów (zakładamy, ˙ze okre´slony jest zbiór takich zmiennych). Dwie formuły stanu mo-˙zemy poł ˛aczy´c stosuj ˛ac klasyczne operatory logiczne omówione przy formułach akcji. Ponadto for-muły mo˙zemy budowa´c stosuj ˛ac operatory: mo˙zliwo´sci (< >), konieczno´sci ([ ]), niesko´nczonej p˛etli(@), najmniejszego punku stałego (mu) oraz najwi˛ekszego punku stałego (nu). Najwy˙zszy prio-rytet maj ˛a operatorynot,< >,[ ],muinu. Kolejne operatory w porz ˛adku malej ˛acego priorytetu

5.1. Logika modalna µ 85

Listing 5.3: Zapis formuł stanów w pakiecie CADP

F ::= true | false | not F | F1 or F2 | F1 and F2 | F1 implies F2 | F1 equ F2 | < R > F | [ R ] F | @ ( R ) | X | mu X . F | nu X . F

Interpretacj ˛aformuły stanuFjest zbiór stanów (podzbiór Γ) spełniaj ˛acych formuł˛e. Interpreta-cja formuły jest definiowana nast˛epuj ˛aco:

– Wszystkie stany spełniaj ˛a formuł˛etrue.

– ˙Zaden stan nie spełnia formułyfalse.

– Formuł˛eXspełniaj ˛a stany ze zbioru przypisanego zmiennej.

– Formuł˛enot Fspełniaj ˛a wszystkie stany, które nie spełniaj ˛a formułyF.

– Formuł˛eF1 or F2spełniaj ˛a wszystkie stany, które spełniaj ˛a formuł˛eF1lubF2.

– Formuł˛eF1 and F2spełniaj ˛a wszystkie stany, które spełniaj ˛a formuł˛eF1iF2.

– Formuł˛eF1 implies F2spełniaj ˛a wszystkie stany, które nie spełniaj ˛a formułyF1lub speł-niaj ˛a formuł˛eF2.

– Formuł˛eF1 equ F2spełniaj ˛a wszystkie stany, które spełniaj ˛a formuł˛eF1iF2lub nie speł-niaj ˛a ˙zadnej z nich.

– Formuł˛e< R > Fspełniaj ˛a stany, dla których istniej ˛a ci ˛agi przej´s´c spełniaj ˛aceR, prowadz ˛ace do stanu spełniaj ˛acegoF.

– Formuł˛e[ R ] Fspełniaj ˛a stany, dla których wszystkie ci ˛agi przej´s´c spełniaj ˛aceR, prowadz ˛a do stanu spełniaj ˛acegoF.

– Formuł˛e@ ( R ) spełniaj ˛a stany, dla których istniej ˛a ci ˛agi przej´s´c, b˛ed ˛ace niesko´nczon ˛a konkatenacj ˛a ci ˛agów przej´s´c spełniaj ˛acych formuł˛e regularn ˛aR.

– Formułamu X . Freprezentuje najmniejsze rozwi ˛azanie (w zbiorze 2^Γ) równania punktu stałego X = F (X).

5.1. Logika modalna µ 86

– Formuł˛enu X . F reprezentuje najwi˛eksze rozwi ˛azanie (w zbiorze 2^Γ) równania punktu stałego X = F (X).

Formuły punktu stałego powinny spełnia´c ponadto dodatkowe wymagania. Dla ka˙zdej formuły stanu µX.ϕ i νX.ϕ, formuła ϕ powinna zawiera´c zmienn ˛a woln ˛a X. Liczba zanegowanych wyst ˛ a-pie´n tej zmiennej i/lub w nast˛epnikach implikacji powinna by´c liczb ˛a parzyst ˛a. Formuła stanu nie mo˙ze tak˙ze zawiera´c wzajemnie rekursywnie zale˙znych zmiennych operatorów µ i ν.

CADP evaluator jest jednym z licznych narz˛edzi wchodz ˛acych w skład pakietu CADP ([20], [21]). Przyjmuje on na wej´sciu odpowiednio zakodowany graf LTS oraz formuł˛e zapisan ˛a w ra-chunku µ. Wynikiem weryfikacji jest warto´s´c logicznatruelubfalsezale˙znie od tego, czy for-muła ta jest spełniona dla grafu LTS, czy nie. Przyjmuje si˛e przy tym, ˙ze graf LTS spełnia formuł˛e stanuF, je˙zeli spełnia j ˛a stan pocz ˛atkowy s0.

Jako format przej´sciowy do zapisu grafów LTS wykorzystamy format aldebaran. Przykład za-pisu grafu LTS w tym formacie pokazano na listingu 5.4. Pliki zaza-pisuje si˛e z rozszerzeniem aut. Pierwsza linia pliku zawiera nast˛epuj ˛ace informacje:

– numer stanu pocz ˛atkowego;

– liczb˛e kraw˛edzi;

– liczb˛e stanów.

Kolejne linie zawieraj ˛a informacje o kraw˛edziach i ich etykietach.

Listing 5.4: Zapis grafu LTS w formacie aldebaran

des (0,11,7) (0,"a",1) (0,"b",2) (0,"c",6) (1,"b",3) (2,"a",5) (2,"b",4) (3,"b",0) (4,"b",3) (5,"a",4) (5,"b",5) (6,"b",6)

Plik z grafem LTS mo˙zna automatycznie przekształci´c do formatu bcg (Binary Coded Graphs), za pomoc ˛a narz˛edzia bcg_io, wchodz ˛acego w skład pakietu CADP. Pliki w formacie bcg s ˛a czy-tane bezpo´srednio przez program evaluator. Sam format bcg jest formatem zamkni˛etym, ale poza wspomnian ˛a translacj ˛a dost˛epne jest API na potrzeby generowania plików w tym formacie przez zewn˛etrzne narz˛edzia, np. z poziomu j˛ezyka C.

5.1. Logika modalna µ 87

Listing 5.5: Konwersja plików z u˙zyciem programów bcg_io i dot

bcg_io plik.aut plik.bcg bcg_io plik.bcg plik.dot dot -Tpdf -O plik.dot

Metod˛e konwersji mi˛edzy formatami aldebaran i bcg oraz bcg i dot pokazano na listingu 5.5. Warto zwróci´c jeszcze uwag˛e na pokazan ˛a mo˙zliwo´s´c konwersji mi˛edzy formatami bcg i dot. Nazwa dotodnosi si˛e zarówno do formatu opisu grafów ([19]) jak i programu do przetwarzania tego for-matu. Pliki zapisane tekstowo w formacie dot mo˙zna eksportowa´c m.in. do formatów takich jak gif, png, pdf. Istotn ˛a zalet ˛a tego formatu jest fakt, ˙ze jest on wspierany przez wiele narz˛edzi komputero-wych przetwarzaj ˛acych grafy. Graf LTS z listingu 5.4, ale w formacie dot pokazano na listingu 5.6. Po konwersji do formatu pdf uzyskujemy wizualizacj˛e pokazan ˛a na rys. 5.1.

Listing 5.6: Zapis grafu LTS w formacie dot

digraph BCG { size = "7, 10.5"; center = TRUE;

node [shape = circle]; 0 [peripheries = 2]; 0 -> 6 [label = "c"]; 0 -> 2 [label = "b"]; 0 -> 1 [label = "a"]; 1 -> 3 [label = "b"]; 2 -> 4 [label = "b"]; 2 -> 5 [label = "a"]; 3 -> 0 [label = "b"]; 4 -> 3 [label = "b"]; 5 -> 5 [label = "b"]; 5 -> 4 [label = "a"]; 6 -> 6 [label = "b"]; }

Oprócz konwersji do formatu pdf (lub innego graficznego), mo˙zliwe jest graficzne przegl ˛adanie plików w formacie dot za pomoc ˛a wolnodost˛epnego oprogramowania, np. program xdot.py dost˛epny na stronie http://code.google.com/p/jrfonseca/wiki/XDot.

Drugim obok grafu LTS w formacie bcg plikiem wej´sciowym dla programu evaluator jest plik z formuł ˛a w logice modalnej. Jest to plik tekstowy z rozszerzeniem mcl, zawieraj ˛acy formuł˛e w logice µ do sprawdzenia. W pliku takim mo˙zna umieszcza´c komentarze zawarte mi˛edzy znakami

(*i*).

Przykład zastosowania programu CADP evaluator pokazano na listingu 5.7. W przykładowym wywołaniu zało˙zono, ˙ze graf LTS znajduje si˛e w plikults.bcg, a formuła (równie˙z pokazana na