Logika dla informatyków/Zdaniowa logika dynamiczna

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 części tej pokażemy jedynie dwie podstawowe własności PDL: własność małego modelu oraz przedstawimy aksjomatyzację i udowodnimy jej pełność. 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) $\displaystyle \varphi ,\psi ,\ldots$ oraz programy $\displaystyle \alpha ,\beta ,\gamma ,\ldots$. Zakładamy, że mamy do dyspozycji przeliczalnie wiele atomowych symboli każdego rodzaju. Programy atomowe są oznaczane przez $\displaystyle a,b,c,\ldots$, a zbiór wszystkich atomowych programów oznaczamy przez $\displaystyle \Pi _{0}$.

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

$\displaystyle [\alpha ]\varphi$

czytamy "po (każdym) wykonaniu programu $\displaystyle \alpha$ koniecznie musi zajść $\displaystyle \varphi$".

Definicja 10.1

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

• $\displaystyle ZZ\subseteq \Phi$
• $\displaystyle \Pi _{0}\subseteq \Pi$
• jeśli $\displaystyle \varphi ,\psi \in \Phi$, to $\displaystyle \varphi \to \psi \in \Phi$ oraz $\displaystyle \bot \in \Phi$
• jeśli $\displaystyle \alpha ,\beta \in \Pi$, to $\displaystyle (\alpha ;\beta )$,$\displaystyle (\alpha \cup \beta )$, oraz $\displaystyle \alpha ^{*}\in \Pi$
• jeśli $\displaystyle \alpha \in \Pi$ oraz $\displaystyle \varphi \in \Phi$, to $\displaystyle [\alpha ]\varphi \in \Phi$
• jeśli $\displaystyle \varphi \in \Phi$, to $\displaystyle \varphi ?\in \Pi .$

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

• Jednoargumentowe operatory (wliczając $\displaystyle [\alpha ]$ ) wiążą silniej niż dwuargumentowe.
• Operator $\displaystyle ;$ wiąże silniej niż $\displaystyle \cup$.
• Spójniki logiczne mają takie same priorytety jak zdefiniowano wcześniej.

Tak więc wyrażenie

$\displaystyle [\alpha ;\beta ^{*}\cup \gamma ^{*}]\varphi \vee \psi$

odpowiada następującemu wyrażeniu z nawiasami

$\displaystyle ([(\alpha ;\beta ^{*})\cup \gamma ^{*}]\varphi )\vee \psi .$

Ponieważ operatory $\displaystyle ;$ oraz $\displaystyle \cup$ okażą się być łączne, więc zwyczajowo będziemy opuszczać nawiasy w wyrażeniach typu $\displaystyle \alpha ;\beta ;\gamma$ lub $\displaystyle \alpha \cup \beta \cup \gamma$.

Przypomnijmy, że negacja $\displaystyle \neg \varphi$ jest skrótem formuły $\displaystyle \varphi \to \bot$. Dualnie do [ ] definiujemy modalność możliwości

$\displaystyle \langle \alpha \rangle \varphi :=\neg [\alpha ]\neg \varphi .$

Zdanie $\displaystyle \langle \alpha \rangle \varphi$ czytamy "istnieje obliczenie programu $\displaystyle \alpha$, które zatrzymuje się w stanie spełniającym formułę $\displaystyle \varphi$". Istotną różnicą pomiędzy modalnościami [ ] i $\displaystyle \langle \rangle$ jest to, że $\displaystyle \langle \alpha \rangle \varphi$ implikuje iż program $\displaystyle \alpha$ się zatrzymuje, podczas gdy $\displaystyle \left[\alpha \right]\varphi$ nie gwarantuje zatrzymania się programu $\displaystyle \alpha$. W szczególności formuła $\displaystyle [\alpha ]\bot$ wyraża własność mówiącą, że żadne obliczenie programu $\displaystyle \alpha$ nie zatrzymuje się. Natomiast formuła $\displaystyle \langle \alpha \rangle \bot$ 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 $\displaystyle K$ jest zbiorem elementów $\displaystyle u,v,w,\ldots$ 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 $\displaystyle p\in ZZ$, 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 $\displaystyle a\in \Pi _{0}$ 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 $\displaystyle \varphi$, 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 $\displaystyle {\mathfrak {K}}$, w których $\displaystyle \varphi$ jest spełniona. Natomiast dla programu $\displaystyle \alpha$, 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 $\displaystyle \alpha$ w strukturze $\displaystyle {\mathfrak {K}}$.

Definicja 10.3

${\mathrm {m} _{\mathfrak {K}}}(\varphi \to \psi )$	${\displaystyle :=(K-{\mathrm {m} _{\mathfrak {K}}}(\varphi )\cup {\mathrm {m} _{\mathfrak {K}}}(\psi )}$
${\mathrm {m} _{\mathfrak {K}}}(\bot )$	$\ :=\emptyset$
${\mathrm {m} _{\mathfrak {K}}}([\alpha ]\varphi )$	$\ :=\left\{u|\forall v\in K(\langle u,v\rangle \in {\mathrm {m} _{\mathfrak {K}}}(\alpha )\Rightarrow v\in {\mathrm {m} _{\mathfrak {K}}}(\varphi ))\right\}$
${\mathrm {m} _{\mathfrak {K}}}(\alpha ;\beta )$	${\displaystyle :=\left\{\langle u,v\rangle |\exists w\in K(\langle u,v\rangle \in {\mathrm {m} _{\mathfrak {K}}}(\alpha )\wedge \langle w,v\rangle \in {\mathrm {m} _{\mathfrak {K}}}(\beta ))\right\}}$
${\mathrm {m} _{\mathfrak {K}}}(\alpha \cup \beta )$	${\displaystyle :={\mathrm {m} _{\mathfrak {K}}}(\alpha )\cup {\mathrm {m} _{\mathfrak {K}}}(\beta )}$
${\mathrm {m} _{\mathfrak {K}}}(\alpha ^{*})$	${\displaystyle :=\bigcup _{n\geq 0}{\mathrm {m} _{\mathfrak {K}}}(\alpha )^{n}}$
${\mathrm {m} _{\mathfrak {K}}}(\varphi ?)$	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 $\displaystyle \varphi$ jest spełniona w stanie $\displaystyle u$ struktury $\displaystyle {\mathfrak {K}}$, gdy $u\in {\mathrm {m} _{\mathfrak {K}}}(\varphi )$. Podobnie jak w logice pierwszego rzędu spełnianie zapisujemy następująco $\displaystyle ({\mathfrak {K}},u)\vDash \varphi$. Gdy z kontekstu wynika o jaką strukturę chodzi, to możemy po prostu pisać $\displaystyle u\vDash \varphi$.

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

Przykład 10.5

Niech $\displaystyle p$ będzie zmienną zdaniową oraz niech $\displaystyle a$ będzie atomowym programem. Niech $\displaystyle {\mathfrak {K}}=(K,\mathrm {m} _{\mathfrak {K}})$ będzie taką strukturą Kripkego, że

$K$	$=\left\{u,v,w\right\}$
${\mathrm {m} _{\mathfrak {K}}}(p)$	$=\left\{u,v\right\}$
${\mathrm {m} _{\mathfrak {K}}}(a)$	$=\left\{\langle u,v\rangle ,\langle u,w\rangle ,\langle v,w\rangle ,\langle w,v\rangle \right\}$.

Nastepujący diagram ilustruje $\displaystyle {\mathfrak {K}}$.

W tej strukturze mamy $\displaystyle u\vDash \langle a\rangle \neg p\wedge \langle a\rangle p$, ale $\displaystyle v\vDash [a]\neg p$ oraz $\displaystyle w\vDash [a]p$. Ponadto każdy stan struktury $\displaystyle {\mathfrak {K}}$ spełnia następującą formułę

$\displaystyle \langle a^{*}\rangle [(aa)^{*}]p\wedge \langle a^{*}\rangle [(aa)^{*}]\neg p$

.

Przykład 10.6

Niech $\displaystyle p,q$ będą zmiennymi zdaniowymi i niech $\displaystyle a,b$ będą atomowymi programami. Ponadto niech $\displaystyle {\mathfrak {K}}=(K,\mathrm {m} _{\mathfrak {K}})$ będzie strukturą Kripkego zdefiniowaną następująco

$K$	$=\left\{s,t,u,v\right\}$
${\mathrm {m} _{\mathfrak {K}}}(p)$	$=\{u,v\}$
${\mathrm {m} _{\mathfrak {K}}}(q)$	$=\{t,v\}$
${\mathrm {m} _{\mathfrak {K}}}(a)$	$=\{\langle t,v\rangle ,\langle v,t\rangle ,\langle s,u\rangle ,\langle u,s\rangle \}$
${\mathrm {m} _{\mathfrak {K}}}(b)$	$=\{\langle u,v\rangle ,\langle v,u\rangle ,\langle s,t\rangle ,\langle t,s\rangle \}$

Następujący rysunek ilustruje $\displaystyle {\mathfrak {K}}$.

Następujące formuły są prawdziwe w $\displaystyle {\mathfrak {K}}$.

$p\leftrightarrow [(ab^{*}a)^{*}]p$ $q\leftrightarrow [(ba^{*}b)^{*}]q.$

Ponadto niech $\displaystyle \alpha$ będzie programem

$\displaystyle \alpha =(aa\cup bb\cup (ab\cup ba)(aa\cup bb)^{*}(ab\cup ba))^{*}.\qquad \qquad \qquad (14)$

Program $\displaystyle \alpha$ traktowany jako wyrażenie regularne, generuje wszystkie słowa nad alfabetem $\displaystyle \{a,b\}$ o parzystej liczbie wystąpień $\displaystyle a$ oraz $\displaystyle b$. Można pokazać, że dla dowolnego zdania $\displaystyle \varphi$, formuła $\displaystyle \varphi \leftrightarrow [\alpha ]\varphi$ jest prawdziwa w $\displaystyle {\mathfrak {K}}$. 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

$\{\langle \alpha ^{*}\rangle \varphi \}\cup \{\neg \varphi ,\neg \langle \alpha \rangle \varphi ,\neg \langle \alpha ^{2}\rangle \varphi ,\ldots \}$

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.

$(i)\ \ \ \ \ \langle \alpha \rangle (\varphi \vee \psi )\ \ \leftrightarrow \ \ \langle \alpha \rangle \varphi \vee \langle \alpha \rangle \psi$

$(ii)\ \ \ \ [\alpha ](\varphi \wedge \psi )\ \ \leftrightarrow \ \ [\alpha ]\varphi \wedge [\alpha ]\psi$

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

$(iv)\ \ \ \langle \alpha \rangle (\varphi \wedge \psi )\ \ \rightarrow \ \ \langle \alpha \rangle \varphi \wedge \langle \alpha \rangle \psi$

$(v)\ \ \ \ [\alpha ]\varphi \vee [\alpha ]\psi \ \ \rightarrow \ \ [\alpha ](\varphi \vee \psi )$

$(vi)\ \ \ \langle \alpha \rangle \bot \ \ \leftrightarrow \ \ \ \bot$

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 $(iii)-(v)$ nie zachodzą. Przykładowo implikacja odwrotna do $(iv)$ nie jest spełniona w stanie $\displaystyle u$ następującej struktury Kripkego.

Następna grupa tautologii, specyficzna dla PDL, dotyczy spójników programotwórczych $\displaystyle ;$ i $\displaystyle \cup$ oraz testu $\displaystyle ?$.

Twierdzenie 10.8

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

$(i)\ \ \ \ \langle \alpha \cup \beta \rangle \varphi \ \ \leftrightarrow \ \ \langle \alpha \rangle \varphi \vee \langle \beta \rangle \varphi$

$(ii)\ \ \ [\alpha \cup \beta ]\varphi \ \ \ \leftrightarrow \ \ [\alpha ]\varphi \wedge [\beta ]\varphi$

$(iii)\ \ \langle \alpha ;\beta \rangle \varphi \ \ \ \ \leftrightarrow \ \ \langle \alpha \rangle \langle \beta \rangle \varphi$

$(iv)\ \ \ [\alpha ;\beta ]\varphi \ \ \ \ \leftrightarrow \ \ [\alpha ][\beta ]\varphi$

$(v)\ \ \ \ \langle \varphi ?\rangle \psi \ \ \leftrightarrow \ \ (\varphi \wedge \psi )$

$(vi)\ \ \ [\varphi ?]\psi \ \ \leftrightarrow \ \ (\varphi \rightarrow \psi )$.

Ostatnia grupa tautologii dotyczy operatora iteracji $^{*}$.

Twierdzenie 10.9

Nastepujące formuły są tautologiami PDL.

$(i)\ \ \ \ [\alpha ^{*}]\varphi \ \ \rightarrow \ \ \varphi$

$(ii)\ \ \ \varphi \ \ \rightarrow \ \ \langle \alpha ^{*}\rangle \varphi$

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ść $(ii)$ mówi, że $\displaystyle \alpha ^{*}$ jest semantycznie relacją zwrotną. Przechodniość relacji $\displaystyle \alpha ^{*}$ jest wyrażona w $(vi)$. Natomiast fakt, że $\displaystyle \alpha ^{*}$ zawiera relację $\displaystyle \alpha$, jest wyrażony w $(iv)$. Implikacja $\displaystyle \leftarrow$ w $(xi)$ wyraża zasadę indukcji. Bazą jest założenie, że własność $\displaystyle \varphi$ jest spełniona w pewnym stanie $\displaystyle u$. Warunek indukcyjny mówi, że w każdym stanie osiągalnym z $\displaystyle u$ poprzez skończoną liczbę iteracji programu $\displaystyle \alpha$, kolejne wykonanie $\displaystyle \alpha$ zachowuje własność $\displaystyle \varphi$. Teza stwierdza, że wówczas $\displaystyle \varphi$ jest spełnione we wszystkich stanach osiągalnych w skończonej liczbie iteracji $\displaystyle \alpha$.

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 $\displaystyle \varphi$ 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 $\displaystyle 2^{|\varphi |}$ stanów, gdzie $\displaystyle |\varphi |$ oznacza rozmiar formuły $\displaystyle \varphi$. 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

$FL$	${\displaystyle :\Phi \ \ \rightarrow \ \ 2^{\Phi }}$
$FL^{\Box }$	${\displaystyle :\{[\alpha ]\varphi \;|\;\alpha \in \Psi ,\;\varphi \in \Phi \}\rightarrow 2^{\Phi }}$

przez wzajemną indukcję

$(a)\;FL(p)\;:=\;\{p\}$, gdy $\displaystyle p$ jest zmienną zdaniową

$(b)\;FL(\varphi \rightarrow \psi )\;:=\;\{\varphi \rightarrow \psi \}\cup FL(\varphi )\cup FL(\psi )$

$(c)\;FL(\bot )\;:=\;\{\bot \}$

$(d)\;FL([\alpha ]\varphi )\;:=FL^{\Box }([\alpha ]\varphi )\cup FL(\varphi )$

$(e)\;FL^{\Box }([a]\varphi )\;:=\;\{[a]\varphi \}$, gdy $\displaystyle a$ jest atomowym programem

$(f)\;FL^{\Box }([\alpha \cup \beta ]\varphi )\;:=\;\{[\alpha \cup \beta ]\varphi \}\cup FL^{\Box }([\alpha ]\varphi )\cup FL^{\Box }([\beta ]\varphi )$

$(g)\;FL^{\Box }([\alpha ;\beta ]\varphi )\;:=\;\{[\alpha ;\beta ]\varphi \}\cup FL^{\Box }([\alpha ][\beta ]\varphi )\cup FL^{\Box }([\beta ]\varphi )$

$(h)\;FL^{\Box }([\alpha ^{*}]\varphi )\;:=\;\{[\alpha ^{*}]\varphi \}\cup FL^{\Box }([\alpha ][\alpha ^{*}]\varphi )$

$(i)\;FL^{\Box }([\psi ?]\varphi )\;:=\;\{[\psi ?]\varphi \}\cup FL(\psi )$

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

Niech $\displaystyle |\alpha |$ oraz $\displaystyle |\varphi |$ oznaczają długość programu $\displaystyle \alpha$ i formuły $\displaystyle \varphi$ rozumianą jako liczbę wystąpień symboli nie licząc nawiasów. Dla dowolnego zbioru $\displaystyle X$, przez $\displaystyle |X|$ oznaczamy moc zbioru $\displaystyle X$. Następujący lemat podaje ograniczenie górne na moc domknięcia Fischera-Ladnera.

Lemat 10.10

$(i)\;\;$ Dla dowolnej formuły $\displaystyle \varphi$ mamy $\displaystyle |FL(\varphi )|\leq |\varphi |$.

$(ii)\;$ Dla dowolnej formuły $\displaystyle [\alpha ]\varphi$ 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 $\displaystyle FL$ oraz $\displaystyle FL^{\Box }$. Pozostawimy go Czytelnikowi jako ćwiczenie.

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

Lemat 10.11

$(i)$ Jeśli $\displaystyle \sigma \in FL(\varphi )$, to $\displaystyle FL(\sigma )\subseteq FL(\varphi )$.

$(ii)$ Jeśli $\displaystyle \sigma \in FL^{\Box }([\alpha ]\varphi )$, to

$\displaystyle FL(\sigma )\subseteq FL^{\Box }([\alpha ]\varphi )\cup FL(\varphi )$.

Dowód

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

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

Lemat 10.12

$(i)$ Jeśli $\displaystyle [\alpha ]\psi \in FL(\varphi )$, to $\displaystyle \psi \in FL(\varphi )$.

$(ii)$ Jeśli $\displaystyle [\rho ?]\psi \in FL(\varphi )$, to $\displaystyle \rho \in FL(\varphi )$.

$(iii)$ Jeśli $\displaystyle [\alpha \cup \beta ]\psi \in FL(\varphi )$, to $[\alpha ]\psi \in FL(\varphi )$ oraz $\displaystyle [\beta ]\psi \in FL(\varphi )$.

$(iv)$ Jeśli $\displaystyle [\alpha ;\beta ]\psi \in FL(\varphi )$, to $\displaystyle [\alpha ][\beta ]\psi \in FL(\varphi )$ oraz $\displaystyle [\beta ]\psi \in FL(\varphi )$.

$(v)$ Jeśli $\displaystyle [\alpha ^{*}]\psi \in FL(\varphi )$, to $[\alpha ][\alpha ^{*}]\psi \in FL(\varphi )$.

Dla danej formuły $\displaystyle \varphi$ oraz struktury Kripkego $\displaystyle {\mathfrak {K}}=(K,\mathrm {m} _{\mathfrak {K}})$ definiujemy nową strukturę $\displaystyle {\mathfrak {K}}/FL(\varphi )=\langle K/FL(\varphi ),\mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}\rangle$, zwaną filtracją struktury ${\mathfrak {K}}$ przez $FL(\varphi )$. Najpierw definiujemy binarną relację $\displaystyle \equiv$ w zbiorze stanów $\displaystyle {\mathfrak {K}}$.

$\displaystyle u\equiv v$ wtedy i tylko wtedy, gdy $\forall \psi \in FL(\varphi )(u\in \mathrm {m} _{\mathfrak {K}}(\psi )\iff v\in \mathrm {m} _{\mathfrak {K}}(\psi )).$

Innymi słowy, utożsamiamy stany $\displaystyle u$ oraz $\displaystyle v$ jeśli są one nierozróżnialne przez żadną formułę ze zbioru $\displaystyle FL(\phi )$. Filtracja struktury jest zwykłą konstrukcją ilorazową. Niech

$\displaystyle [u]$	${\displaystyle :=\{v\;|\;v\equiv u\}}$
$K/FL(\varphi )$	${\displaystyle :=\{[u]\;|\;u\in K\}}$
$\mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(p)$	${\displaystyle :=\{[u]\;|\;u\in \mathrm {m} _{\mathfrak {K}}(p)\}}$, gdy $p$ jest zmienną losową
$\mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(a)$	${\displaystyle :=\{\langle [u],[v]\rangle \;|\;\langle u,v\rangle \in \mathrm {m} _{\mathfrak {K}}(a)\}}$, gdy $a$ jest atomowym programem.

Przekształcenie $\mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}$ rozszerza się w zwykły sposób na wszystkie formuły i programy.

Następujący lemat pokazuje związek pomiędzy strukturami $\displaystyle {\mathfrak {K}}$ oraz $\displaystyle {\mathfrak {K}}/FL(\varphi )$. 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 $\displaystyle u,v$ będą stanami w strukturze Kripkego $\displaystyle {\mathfrak {K}}$.

$(i)$ Dla dowolnej formuły $\displaystyle \psi \in FL(\varphi )$, mamy $\displaystyle u\in \mathrm {m} _{\mathfrak {K}}(\psi )\iff \ [u]\in \mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(\psi )$.

$(ii)$ Dla dowolnej formuły $\displaystyle [\alpha ]\psi \in FL(\varphi )$ zachodzi

$(a)$ jeśli $\displaystyle \langle u,v\rangle \in \mathrm {m} _{\mathfrak {K}}(\alpha )$, to $\displaystyle \langle [u],[v]\rangle \in \mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(\alpha )$;

$(a)$ jeśli $\displaystyle \langle [u],[v]\rangle \in \mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(\alpha )$ 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 $\displaystyle \varphi$ będzie spełnialną formułą PDL. Wówczas $\displaystyle \varphi$ jest spełniona w strukturze Kripkego mającej co najwyżej $\displaystyle 2^{|\varphi |}$ stanów.

Dowód

Jeśli $\displaystyle \varphi$ jest spełnialna, to istnieje struktura Kripkego $\displaystyle {\mathfrak {K}}$ oraz stan $\displaystyle u\in {\mathfrak {K}}$, taki że $\displaystyle u\in \mathrm {m} _{\mathfrak {K}}(\varphi )$. Niech $\displaystyle FL(\varphi )$ będzie domknięciem Fischera-Ladnera formuły $\displaystyle \varphi$. Na mocy Lematu 10.13 o filtracji mamy $\displaystyle [u]\in \mathrm {m} _{{\mathfrak {K}}/FL(\varphi )}(\varphi )$. Ponadto $\displaystyle {\mathfrak {K}}/FL(\varphi )$ ma nie więcej stanów niż liczba wartościowań przypisujących wartości logiczne formułom z $\displaystyle FL(\varphi )$. Tych ostatnich jest, na mocy Lematu 10.10 $(i)$, co najwyżej $\displaystyle 2^{|\varphi |}$.

Z powyższego twierdzenia natychmiast wynika rozstrzygalość problemu spełnialności dla formuł PDL. Naiwny algorytm polegający na przeszukiwaniu wszystkich struktur Kripkego o co najwyżej $\displaystyle 2^{|\phi |}$ 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

$(P0)$ 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

$(MP)\ \ {\frac {\varphi \quad \varphi \to \psi }{\psi }}$

$(GEN)\ \ {\frac {\varphi }{[\alpha ]\varphi }}$

Reguła (GEN) nazywana jest regułą modalnej generalizacji. Jeśli $\displaystyle \varphi$ daje się wyprowadzić w powyższym systemie poszerzonym o dodanie nowych aksjomatów ze zbioru $\displaystyle \Sigma$, to będziemy to zapisywać przez $\displaystyle \Sigma \vdash \varphi$. Jak zwykle piszemy $\displaystyle \vdash \phi$, gdy $\displaystyle \Sigma$ 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ł $\displaystyle \Sigma$ jest sprzeczny, gdy $\displaystyle \Sigma \vdash \bot$. W przeciwnym przypadku mówimy, że $\displaystyle \Sigma$ 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 $\displaystyle \Sigma$ będzie zbiorem formuł PDL. Wówczas

$(i)\ \ \ \ \Sigma$ jest niesprzeczny wtedy i tylko wtedy, gdy $\displaystyle \Sigma \cup \{\varphi \}$ jest niesprzeczny lub $\displaystyle \Sigma \cup \{\neg \varphi \}$ jest niesprzeczny;

$(ii)$ jeśli $\displaystyle \Sigma$ jest niesprzeczny, to $\displaystyle \Sigma$ jest zawarty w maksymalnym niesprzecznym zbiorze formuł.

Ponadto, jeśli $\displaystyle \Sigma$ jest maksymalnym niesprzecznym zbiorem formuł, to

$(iii)\ \ \Sigma$ zawiera wszystkie twierdzenia PDL;

$(iv)\ \$ jeśli $\displaystyle \varphi \in \Sigma$ oraz $\displaystyle \varphi \to \psi \in \Sigma$, to $\displaystyle \psi \in \Sigma$;

$(v)\ \ \ \ \varphi \vee \psi \in \Sigma$ wtedy i tylko wtedy, gdy $\displaystyle \varphi \in \Sigma$ lub $\displaystyle \psi \in \Sigma$;

$(vi)\ \ \ \varphi \wedge \psi \in \Sigma$ wtedy i tylko wtedy, gdy $\displaystyle \varphi \in \Sigma$ oraz $\displaystyle \psi \in \Sigma$;

$(vii)\ \ \varphi \in \Sigma$ wtedy i tylko wtedy, gdy $\displaystyle \neg \varphi \not \in \Sigma$;

$(viii)\ \bot \not \in \Sigma$.

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

Lemat 10.16

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

$(a)$ Dla dowolnej formuły $\displaystyle \psi$, jeśli $\displaystyle \psi \in \Gamma$, to $\displaystyle \langle \alpha \rangle \psi \in \Sigma$.

$(b)$ Dla dowolnej formuły $\displaystyle \psi$, jeśli $\displaystyle [\alpha ]\psi \in \Sigma$, to $\displaystyle \psi \in \Gamma$.

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 $\displaystyle \alpha ^{*}$ nie będzie musiało być domknięcie przechodnie i zwrotne relacji wyznaczonej przez $\displaystyle \alpha$. 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ę $\displaystyle {\mathfrak {N}}=(N,\mathrm {m} _{\mathfrak {N}})$ 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 $\mathrm {m} _{\mathfrak {N}}(\alpha ^{*})$ było relacją zwrotną i przechodnią, zawierało relację $\displaystyle \mathrm {m} _{\mathfrak {N}}(\alpha )$ oraz spełniało aksjomaty $(P6)$ i $(P7)$. Tzn. zamiast warunku

$\displaystyle \mathrm {m} _{\mathfrak {N}}(\alpha ^{*}):=\bigcup _{n\geq 0}\mathrm {m} _{\mathfrak {N}}(\alpha )^{n},\qquad \qquad \qquad \quad \quad \quad \qquad (15)$

żądamy, aby dla każdego programu $\displaystyle \alpha$, relacja $\displaystyle \mathrm {m} _{\mathfrak {N}}(\alpha ^{*})$ była zwrotna, przechodnia, zawierała $\displaystyle \mathrm {m} _{\mathfrak {N}}(\alpha )$ oraz spełniała następujące dwa warunki dla dowolnej formuły $\displaystyle \varphi$

$\mathrm {m} _{\mathfrak {N}}([\alpha ^{*}]\varphi )=\mathrm {m} _{\mathfrak {N}}(\varphi \wedge [\alpha ;\alpha ^{*}]\varphi )\qquad \qquad \qquad \quad \quad \quad (16)$

$\mathrm {m} _{\mathfrak {N}}([\alpha ^{*}]\varphi )=\mathrm {m} _{\mathfrak {N}}(\varphi \wedge [\alpha ^{*}](\varphi \to [\alpha ]\varphi )).\qquad \qquad \qquad (17)$

Wracamy teraz do konstrukcji struktury z maksymalnych niesprzecznych zbiorów formuł. Zdefiniujemy niestandardową strukturę Kripkego $\displaystyle {\mathfrak {N}}=(N,\mathrm {m} _{\mathfrak {N}})$ następująco

$N$	${\displaystyle :=\{}$ maksymalnie niesprzeczne zbiory formuł PDL $\}$
$\mathrm {m} _{\mathfrak {N}}(\varphi )$	${\displaystyle :=\{s\;|\;\varphi \in s\}}$
$\mathrm {m} _{\mathfrak {N}}(\alpha )$	${\displaystyle :=\{\langle s,t\rangle \;|\;}$ dla wszystkich $\varphi$, jeśli $\varphi \in t$, to $\langle \alpha \rangle \varphi \in s\}$
	${\displaystyle :=\{\langle s,t\rangle \;|\;}$ dla wszystkich $\varphi$, jeśli $[\alpha ]\varphi \in s$, to $\varphi \in t\}$

Z Lematu Lematu 10.16 wynika, że obydwie definicje $\mathrm {m} _{\mathfrak {N}}(\alpha )$ są równoważne. Dowód nastepującego twierdzenia pozostawimy Czytelnikowi.

Twierdzenie 10.18

Struktura $\displaystyle {\mathfrak {N}}$ jest niestandardową strukturą Kripkego.

Dowód

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

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 $\displaystyle {\mathfrak {N}}$ będzie niestandardową strukturą Kripkego i niech $\displaystyle u,v$ będą stanami w $\displaystyle {\mathfrak {N}}$.

$(i)$ Dla dowolnej formuły $\displaystyle \psi \in FL(\varphi )$, 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)} .

$(ii)$ Dla dowolnej formuły $[\alpha ]\psi \in FL(\varphi )$ zachodzi

$(a)$ jeśli $\langle u,v\rangle \in \mathrm {m} _{\mathfrak {N}}(\alpha )$, to $\langle [u],[v]\rangle \in \mathrm {m} _{{\mathfrak {N}}/FL(\varphi )}(\alpha );$

$(b)$ jeśli $\langle [u],[v]\rangle \in \mathrm {m} _{{\mathfrak {N}}/FL(\varphi )}(\alpha )$ oraz $u\in \mathrm {m} _{\mathfrak {N}}([\alpha ]\psi )$ to $v\in \mathrm {m} _{\mathfrak {N}}(\psi )$.

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 $(ii)$ dla przypadku, gdy $\displaystyle \alpha$ jest programem postaci $\displaystyle \beta ^{*}$ wykorzystujemy jedynie własności (16) oraz (17), zamiast (15).

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 $\displaystyle \varphi$, jeśli $\displaystyle \vDash \varphi$, to $\displaystyle \vdash \varphi$.

Dowód

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