Logika dla informatyków/Zdaniowa logika dynamiczna

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zdaniowa logika dynamiczna

Zdaniowa logika dynamiczna (PDL, od angielskiej nazwy Propositional Dynamic Logic) została zaproponowana przez V. Pratta w 1976r. Jest ona eleganckim i zwięzłym formalizmem pozwalającym badać rozumowania dotyczące programów iteracyjnych. Formalizm ten rozszerza logikę modalną poprzez wprowadzenie modalności dla każdego programu z osobna. W tej części pokażemy jedynie dwie podstawowe własności PDL: własność małego modelu oraz pełność aksjomatyzacji. Z własności małego modelu natychmiast wynika rozstrzygalność problemu spełnialności dla PDL. System o podobnym charakterze, o nazwie Logika Algorytmiczna, został zaproponowany w roku 1970 przez A. Salwickiego.

Składnia i semantyka PDL

Syntaktycznie PDL jest mieszaniną trzech klasycznych składników: logiki zdaniowej, logiki modalnej oraz algebry wyrażeń regularnych. Język PDL zawiera wyrażenia dwóch rodzajów: zdania (lub formuły) oraz programy . Zakładamy, że mamy do dyspozycji przeliczalnie wiele atomowych symboli każdego rodzaju. Programy atomowe są oznaczane przez , a zbiór wszystkich atomowych programów oznaczamy przez .

Programy są budowane z programów atomowych przy użyciu operacji złożenia , niedeterministycznego wyboru oraz iteracji . Intuicyjnie wykonanie programu oznacza wykonanie , a następnie wykonanie na danych wyprodukowanych przez programu . Wykonanie programu oznacza niedeterministyczny wybór wykonania lub . Natomiast wykonanie programu oznacza wykonanie pewną liczbę razy, być może zero. Ponadto mamy operację testowania tworzącą z każdej formuły nowy program . Wykonanie programu jest możliwe tylko wtedy, gdy warunek zachodzi. Z drugiej strony, formuły mogą odwoływać się do dowolnego programu poprzez modalność konieczności : dla dowolnego zdania , napis

czytamy "po (każdym) wykonaniu programu koniecznie musi zajść ".

Definicja 10.1

Definicja formuł i programów jest wzajemnie rekurencyjna. Definiujemy zbiór programów oraz zbiór formuł jako najmniejsze zbiory spełniające następujące warunki

  • jeśli , to oraz
  • jeśli , to ,, oraz
  • jeśli oraz , to
  • jeśli , to

Aby uniknąć pisania zbyt wielu nawiasów, stosujemy następujące priorytety:

  • Jednoargumentowe operatory (wliczając ) wiążą silniej niż dwuargumentowe.
  • Operator wiąże silniej niż .
  • Spójniki logiczne mają takie same priorytety jak zdefiniowano wcześniej.

Tak więc wyrażenie

odpowiada następującemu wyrażeniu z nawiasami

Ponieważ operatory oraz okażą się być łączne, więc zwyczajowo będziemy opuszczać nawiasy w wyrażeniach typu lub .

Przypomnijmy, że negacja jest skrótem formuły . Dualnie do [ ] definiujemy modalność możliwości

Zdanie czytamy "istnieje obliczenie programu , które zatrzymuje się w stanie spełniającym formułę ". Istotną różnicą pomiędzy modalnościami [ ] i jest to, że implikuje iż program się zatrzymuje, podczas gdy nie gwarantuje zatrzymania się programu . W szczególności formuła wyraża własność mówiącą, że żadne obliczenie programu nie zatrzymuje się. Natomiast formuła jest zawsze fałszywa.

Przejdziemy teraz do zdefiniowania semantyki. Podstawową strukturą semantyczną dla PDL jest tzw. struktura Kripkego.

Definicja 10.2

Struktura Kripkego jest uporządkowaną parą Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathfrak{K} = \langle K,\mathrm{m}_{\mathfrak{K}\rangle} , gdzie jest zbiorem elementów zwanych stanami, a Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathrm{m}_{\mathfrak{K}} jest funkcją przyporządkowującą każdemu atomowemu zdaniu , podzbiór Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(p)\subseteq K} oraz każdemu atomowemu programowi relację binarną Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(a)\subseteq K\times K} .

Poniżej funkcję Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \mathrm{m}_{\mathfrak{K}} rozszerzymy do dowolnych formuł i dowolnych programów. Intuicyjnie dla formuły , zbiór stanów Parser nie mógł rozpoznać (nieznana funkcja „\vrphi”): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(\vrphi)} jest zbiorem wszystkich stanów struktury , w których jest spełniona. Natomiast dla programu , relacja Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\mathrm{m}_{\mathfrak{K}}(\alpha)} jest tzw. relacją wejścia-wyjścia programu  w strukturze .

Definicja 10.3

Parser nie mógł rozpoznać (błąd składni): {\displaystyle := \left\{\langle u,v\rangle | u \in {\mathrm{m}_\mathfrak{K}}(\varphi)\right}.}

Definicja 10.4

Powiemy, że formuła jest spełniona w stanie struktury , gdy . Podobnie jak w logice pierwszego rzędu spełnianie zapisujemy następująco . Gdy z kontekstu wynika o jaką strukturę chodzi, to możemy po prostu pisać .

Powiemy, że formuła jest prawdziwa w strukturze , gdy jest spełniona w każdym stanie tej struktury. Zapisujemy to . Formuła jest tautologią PDL, gdy jest ona prawdziwa w każdej strukturze Kripkego. Wreszcie powiemy, że formuła jest spełnialna, gdy istnieje struktura Kripkego , taka że jest spełniona w przynajmniej jednym stanie .

Przykład 10.5

Niech będzie zmienną zdaniową oraz niech będzie atomowym programem. Niech będzie taką strukturą Kripkego, że

.

Nastepujący diagram ilustruje .

Przykład105.PNG

W tej strukturze mamy , ale oraz . Ponadto każdy stan struktury spełnia następującą formułę

.

Przykład 10.6

Niech będą zmiennymi zdaniowymi i niech będą atomowymi programami. Ponadto niech będzie strukturą Kripkego zdefiniowaną następująco

Następujący rysunek ilustruje .

Przykład106.PNG

Następujące formuły są prawdziwe w .

Ponadto niech będzie programem

Program traktowany jako wyrażenie regularne, generuje wszystkie słowa nad alfabetem o parzystej liczbie wystąpień oraz . Można pokazać, że dla dowolnego zdania , formuła jest prawdziwa w . Zauważmy, że operator jest z natury infinitarny. Z definicji domknięcie zwrotne i przechodnie relacji jest nieskończoną sumą. Z tego względu twierdzenie o zwartości nie zachodzi dla PDL. Istotnie, zbiór

jest skończenie spełnialny (tzn. każdy skończony podzbiór jest spełnialny), ale cały zbiór nie jest spełnialny.

Przykłady tautologii PDL

W tej części przedstawimy przykłady tautologii PDL. Wszystkie dowody, jako łatwe pozostawimy Czytelnikowi. Pierwsza grupa tautologii to schematy znane z logiki modalnej.

Twierdzenie 10.7

Następujące formuły są tautologiami PDL.

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iii)\ \ \ [\alpha](\varphi\rightarrow\psi) \ \ \rightarrow\ \ ([\alpha]\varphi\rightarrow[\alpha]\psi)}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vii)\ \ \ [\alpha]\varphi \ \ \leftrightarrow\ \ \ \neg\langle\alpha\rangle\neg\varphi} .

Implikacje odwrotne w Twierdzeniu 10.7 nie zachodzą. Przykładowo implikacja odwrotna do nie jest spełniona w stanie następującej struktury Kripkego.

Przykład107.PNG

Następna grupa tautologii, specyficzna dla PDL, dotyczy spójników programotwórczych i oraz testu .

Twierdzenie 10.8

Następujące formuły są tautologiami PDL.

.

Ostatnia grupa tautologii dotyczy operatora iteracji .

Twierdzenie 10.9

Nastepujące formuły są tautologiami PDL.

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iii)\ \ [\alpha^*]\varphi\ \ \rightarrow\ \ [\alpha]\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (iv)\ \ \ \langle\alpha\rangle\varphi\ \ \rightarrow\ \ \langle\alpha^*\rangle\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (v)\ \ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^*\alpha^*]\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vi)\ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \langle\alpha^*\alpha^*\rangle\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (vii)\ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^{**}]\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (viii)\ \langle\alpha^*\rangle\varphi\ \leftrightarrow\ \ \langle\alpha^{**}\rangle\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (ix)\ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ \varphi\wedge[\alpha][\alpha^*]\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (x)\ \ \ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \varphi\vee\langle\alpha\rangle\langle\alpha^*\rangle\varphi}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (xi)\ \ \ [\alpha^*]\varphi\ \ \leftrightarrow\ \ \varphi\wedge[\alpha^*](\varphi\rightarrow[\alpha]\varphi)}
Parser nie mógł rozpoznać (błąd składni): {\displaystyle (xii)\ \ \langle\alpha^*\rangle\varphi\ \ \leftrightarrow\ \ \varphi\vee\langle\alpha^*\rangle(\neg\varphi\wedge\langle\alpha\rangle\varphi)} .

Własność mówi, że jest semantycznie relacją zwrotną. Przechodniość relacji jest wyrażona w . Natomiast fakt, że zawiera relację , jest wyrażony w . Implikacja w wyraża zasadę indukcji. Bazą jest założenie, że własność jest spełniona w pewnym stanie . Warunek indukcyjny mówi, że w każdym stanie osiągalnym z poprzez skończoną liczbę iteracji programu , kolejne wykonanie zachowuje własność . Teza stwierdza, że wówczas jest spełnione we wszystkich stanach osiągalnych w skończonej liczbie iteracji .

Własność małego modelu

W tej części udowodnimy własność małego modelu dla PDL. Własność ta mówi, że jeśli jest spełnialna, to jest spełniona w pewnej skończonej strukturze Kripkego. Co więcej, jak będzie wynikało z dowodu, struktura ta ma co najwyżej stanów, gdzie oznacza rozmiar formuły . Wynika stąd natychmiast rozstrzygalność problemu spełnialności dla PDL. Technika zastosowana w dowodzie twierdzenia o małym modelu nosi nazwę filtracji i jest od dawna stosowana w logikach modalnych. W przypadku PDL sytuację komplikuje fakt, że definicja formuł i programów jest wzajemnie rekurencyjna, co powoduje że indukcyjne rozumowania są nieco bardziej delikatne. Własność małego modelu dla PDL została udowodniona w 1977r. przez M. Fischera i R. Ladnera. Zaczniemy od definicji domknięcia Fischera-Ladnera. Zdefiniujemy dwie funkcje


przez wzajemną indukcję

, gdy jest zmienną zdaniową
, gdy jest atomowym programem

Zbiór jest nazywany domknięciem Fischera-Ladnera. Zauważmy, że definicja jest indukcyjna ze względu na budowę formuły , natomiast pomocnicza funkcja jest określona jedynie na formułach postaci i jej definicja jest indukcyjna ze względu na budowę programu . Tak więc chociaż w warunku formuła po prawej stronie definicji jest dłuższa niż po lewej, to program w zewnętrznej modalności jest prostszy niż i dlatego definicja ta jest dobrze ufundowana.

Niech oraz oznaczają długość programu i formuły rozumianą jako liczbę wystąpień symboli nie licząc nawiasów. Następujący lemat podaje ograniczenie górne na moc domknięcia Fischera-Ladnera.

Lemat 10.10

Dla dowolnej formuły mamy .
Dla dowolnej formuły mamy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle |FL^{\Box}([\alpha]\varphi}| \leq |\alpha|} .

Dowód

Dowód jest przez jednoczesną indukcję ze względu na schemat definiujący oraz . Pozostawimy go Czytelnikowi jako ćwiczenie.

End of proof.gif

Następny lemat ma charakter techniczny. Będzie wykorzystany w dowodzie lematu o filtracji.

Lemat 10.11

Jeśli , to .
Jeśli , to

.

Dowód

Dowodzimy (i) oraz (ii) przez jednoczesną indukcję. Szczegóły pozostawiamy Czytelnikowi jako ćwiczenie.

End of proof.gif

Następujące własości są bezpośrednią konsekwencją Lematu 10.11.

Lemat 10.12

Jeśli , to .
Jeśli , to .
Jeśli , to oraz .
Jeśli , to oraz .
Jeśli , to .


Dla danej formuły oraz struktury Kripkego definiujemy nową strukturę , zwaną filtracją struktury przez . Najpierw definiujemy binarną relację w zbiorze stanów .

wtedy i tylko wtedy, gdy

Innymi słowy, utożsamiamy stany oraz jeśli są one nierozróżnialne przez żadną formułę ze zbioru . Filtracja struktury jest zwykłą konstrukcją ilorazową. Niech

, gdy jest zmienną losową
, gdy jest atomowym programem.

Przekształcenie rozszerza się w zwykły sposób na wszystkie formuły i programy.

Następujący lemat pokazuje związek pomiędzy strukturami oraz . Główna trudność techniczna polega tu na sformułowaniu poprawnego założenia indukcyjnego. Sam dowód (jednoczesna indukcja) jest zupełnie rutynowy i dlatego pozostawimy go Czytelnikowi jako ćwiczenie.

Lemat 10.13 (o filtracji)

Niech będą stanami w strukturze Kripkego .

Dla dowolnej formuły , mamy .
Dla dowolnej formuły zachodzi
jeśli , to ;
jeśli oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle u\in\mathrm{m}_{\mathfrak{K}([\alpha]\psi)} , to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle v\in\mathrm{m}_{\mathfrak{K}(\psi)} .

Z lematu o filtracji natychmiast dostajemy twierdzenie o małym modelu.


Twierdzenie 10.14 (Własność małego modelu)

Niech będzie spełnialną formułą PDL. Wówczas jest spełniona w strukturze Kripkego mającej co najwyżej stanów.

Dowód

Jeśli jest spełnialna, to istnieje struktura Kripkego oraz stan , taki że . Niech będzie domknięciem Fischera-Ladnera formuły . Na mocy Lematu 10.13 o filtracji mamy . Ponadto ma nie więcej stanów niż liczba wartościowań przypisujących wartości logiczne formułom z . Tych ostatnich jest, na mocy Lematu 10.10 , co najwyżej .

End of proof.gif

Z powyższego twierdzenia natychmiast wynika rozstrzygalność problemu spełnialności dla formuł PDL. Naiwny algorytm polegający na przeszukiwaniu wszystkich struktur Kripkego o co najwyżej stanach ma złożoność podwójnie wykładniczą względem długości formuły. Używając nieco sprytniejszej metody można rozstrzygnąć problem spełnialności w czasie pojedynczo wykładniczym. Złożoność ta jest najlepsza możliwa, można bowiem pokazać, że problem spełnialności dla PDL jest zupełny w deterministycznym czasie wykładniczym.

Aksjomatyzacja PDL

Podamy teraz system formalny dla PDL i naszkicujemy dowód jego pełności. Jest to system w stylu Hilberta.

Aksjomaty

Aksjomaty logiki zdaniowej

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P1) \ \ [\alpha](\varphi\to\psi)\ \ \to\ \ ([\alpha]\varphi\to[\alpha]\psi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P2) \ \ [\alpha](\varphi\wedge\psi)\ \ \leftrightarrow\ \ ([\alpha]\varphi\wedge[\alpha]\psi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P3) \ \ [\alpha\cup\beta]\varphi\ \ \leftrightarrow\ \ ([\alpha]\varphi\wedge[\beta]\varphi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P4) \ \ [\alpha;\beta]\varphi\ \ \leftrightarrow\ \ ([\alpha][\beta]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P5) \ \ [\psi?]\varphi\ \ \leftrightarrow\ \ (\psi\to\varphi)}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P6) \ \ \varphi\wedge[\alpha][\alpha^*]\varphi\ \ \leftrightarrow\ \ [\alpha^*]\varphi}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle (P7) \ \ \varphi\wedge[\alpha^*](\varphi\to[\alpha]\varphi)\ \ \to\ \ [\alpha^*]\varphi \ \ \ } (aksjomat indukcji)


Reguły dowodzenia


Reguła (GEN) nazywana jest regułą modalnej generalizacji. Jeśli daje się wyprowadzić w powyższym systemie poszerzonym o dodanie nowych aksjomatów ze zbioru , to będziemy to zapisywać przez . Jak zwykle piszemy , gdy jest zbiorem pustym.

Fakt, że wszystkie aksjomaty są tautologiami PDL, wynika z Sekcji: Przykłady tautologii PDL. Pozostawimy Czytelnikowi sprawdzenie, że powyższe reguły zachowują własność bycia tautologią. Tak więc każde twierdzenie powyższego systemu jest tautologią. Naszkicujemy dowód twierdzenia odwrotnego, czyli tzw. twierdzenia o pełności dla PDL. Przypomnijmy, że zbiór formuł jest sprzeczny, gdy . W przeciwnym przypadku mówimy, że jest niesprzeczny. W poniższym lemacie zebrane są podstawowe własności zbiorów niesprzecznych potrzebne do dowodu twierdzenia o pełności.

Lemat 10.15

Niech będzie zbiorem formuł PDL. Wówczas

jest niesprzeczny wtedy i tylko wtedy, gdy jest niesprzeczny lub jest niesprzeczny;

jeśli jest niesprzeczny, to jest zawarty w maksymalnym niesprzecznym zbiorze formuł.


Ponadto, jeśli jest maksymalnym niesprzecznym zbiorem formuł, to

zawiera wszystkie twierdzenia PDL;

jeśli oraz , to ;

wtedy i tylko wtedy, gdy lub ;

wtedy i tylko wtedy, gdy oraz ;

wtedy i tylko wtedy, gdy ;

.

Z powyższego lematu natychmiast dostajemy następującą własność.

Lemat 10.16

Niech oraz będą maksymalnymi niesprzecznymi zbiorami formuł oraz niech będzie dowolnym programem. Następujące dwa warunki są równoważne:

Dla dowolnej formuły , jeśli , to .
Dla dowolnej formuły , jeśli , to .

Struktura, którą za chwilę zbudujemy przy użyciu maksymalnych niesprzecznych zbiorów formuł nie będzie strukturą Kripkego z tego względu, że znaczeniem programu nie będzie musiało być domknięcie przechodnie i zwrotne relacji wyznaczonej przez . Spełnione będą nieco słabsze własności, wystarczające jednak do przeprowadzenia dowodu twierdzenia o pełności.

Definicja 10.17

Niestandardową strukturą Kripkego nazwiemy każdą strukturę spełniającą wszystkie warunki struktury Kripkego podane w definicjach 10.2 oraz 10.3 za wyjątkiem warunku (14). Zamiast tego warunku żądamy, aby było relacją zwrotną i przechodnią, zawierało relację oraz spełniało aksjomaty . Tzn. zamiast warunku

żądamy, aby dla każdego programu , relacja była zwrotna, przechodnia, zawierała oraz spełniała następujące dwa warunki dla dowolnej formuły



Wracamy teraz do konstrukcji struktury z maksymalnych niesprzecznych zbiorów formuł. Zdefiniujemy niestandardową strukturę Kripkego następująco: Elementami zbioru $N$ są maksymalne niesprzeczne zbiory formuł PDL. Dalej:


dla wszystkich , jeśli , to
dla wszystkich , jeśli , to


Z Lematu Lematu 10.16 wynika, że obydwie definicje są równoważne. Dowód nastepującego twierdzenia pozostawimy Czytelnikowi.

Twierdzenie 10.18

Struktura jest niestandardową strukturą Kripkego.

Dowód

Fakt, że spełnia własności (16) oraz (17) wynika natychmiast z Lematu 10.15 oraz z aksjomatów (P6) i (P7). Sprawdzenie pozostałych warunków pozostawimy Czytelnikowi jako ćwiczenie.

End of proof.gif

Istotną cechą niestandardowych struktur Kripkego jest to, że daje się przenieść na nie lemat o filtracji (Lemat 10.13).


Lemat 10.19 (o filtracji dla niestandardowych struktur Kripkego)

Niech będzie niestandardową strukturą Kripkego i niech będą stanami w .

Dla dowolnej formuły , mamy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle u\in \mathrm{m}_{\mathfrak{N}}(\psi) \ \iff \ [u]\in \mathrm{m}_{\mathfrak{N}/FL(\varphi)}(\psi)} .
Dla dowolnej formuły zachodzi
jeśli , to
jeśli oraz to .

Dowód

Szczegóły dowodu tego lematu pomijamy, zachęcając jednocześnie Czytelnika do spróbowania własnych sił. Różnica w dowodzie tego lematu w stosunku do dowodu Lematu 10.13 polega na tym, że w dowodze kroku indukcyjnego dla części dla przypadku, gdy jest programem postaci wykorzystujemy jedynie własności (16) oraz (17), zamiast (15).

End of proof.gif

Możemy już teraz zakończyć dowód twierdzenia o pełności.

Twierdzenie 10.20 (Pełność dla PDL)

Każda tautologia PDL jest twierdzeniem systemu: dla dowolnej formuły , jeśli , to .

Dowód

Rozumujemy przez sprzeczność. Jeśli , to jest zbiorem niesprzecznym. Zatem na mocy Lematu 10.15 istnieje maksymalny niesprzeczny zbiór formuł PDL zawierający . Na mocy lematu o filtracji dla niestandardowych struktur Kripkego (Lemat 10.19) stwierdzamy, że jest spełniona w stanie skończonej struktury . Łatwo jest zauważyć, że skończona niestandardowa struktura Kripkego jest zwykłą strukturą Kripkego (tzn. taką, w której zachodzi (15)). Tak więc nie jest tautologią. To kończy dowód twierdzenia o pełności.

End of proof.gif