Wyobraźmy sobie grę w kółko i krzyżyk, w której kratki znanego diagramu są ponumerowane od 1 do 9:
| 1 | 2 | 3 |
| 4 | 5 | 6 |
| 7 | 8 | 9 |
Teraz weźmy sygnaturę dla PDL, w której są programy \(\bigcirc_1,\bigcirc_2,\dots,\bigcirc_9\) oraz
\({\times}_1,{\times}_2,\dots,{\times}_9\), odpowiadające wpisywaniu kółek i krzyżyków w odpowiednie kratki.
Poza tym mamy trzy zmienne zdaniowe \(win_\bigcirc,win_{\times},draw.\)
Struktury nad tą sygnaturą opisują możliwe (choć niekoniecznie zgodne z powszechnie znanymi regułami) rozgrywki.
Zadanie 1
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, po wpisaniu kółka bądź krzyżyka w kratkę \(n\), nic więcej w nią już nie można wpisać.
Zadanie 2
Napisać zdanie, które wyraża fakt, że w aktualnym stanie każdy ruch jest możliwy.
Zadanie 3
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, gracze wykonują ruchy na przemian.
Zadanie 4
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, po wpisaniu kółka bądź krzyżyka w kratkę \(n\), nic więcej w nią już nie można wpisać.
Zadanie 5
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, jeśli nikt nie wpisze kółka bądź krzyżyka w kratkę \(n\), to można to zrobić poźniej, a po wykonaniu tego ruchu już nigdy więcej.
Zadanie 6
Napisać zdanie, które wyraża fakt, że ze stanów z rozstrzygniętym wynikiem gry już nie można wykonywać ruchów.
Zadanie 7
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, zakładając prawdziwość w nim zdań z poprzednich zadań, to aby dotrzeć do stanu wygrywającego dla gracza używającego kółek, trzeba ustawić jakieś trzy kółka w linię.
Zadanie 8
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, , zakładając prawdziwość w nim zdań z poprzednich zadań, gracz używający kółek ma strategię wygrywającą.
Zadanie 9
Napisać zdanie, które wyraża fakt, że poczynając od aktualnego stanu, zakładając prawdziwość w nim zdań z poprzednich zadań, gracz używający kółek ma strategię wygrywającą.
Zadanie 10
Na ilustracji przedstawiona jest struktura Kripkego dla PDL. Jest tylko jeden program atomowy \(a\) i jedna zmienna zdaniowa \(t\), która prawdziwa jest tylko w jednym stanie, oznaczonym gwiazdką.
UWAGA: Link do ZMODYFIKOWANEGO\({}^2\) (tzn. po raz drugi) obrazka
Napisać formuły PDL, które rozróżniają poszczególne stany zaznaczone grubymi strzałkami: dla każdej pary spośród nich należy napisać formułę, która jest prawdziwa w jednym z tych stanów a fałszywa w drugim.
Zadanie 11
Niech w sygnaturze będzie jeden program atomowy \(s\) i dwie zmienne zdaniowe \(p\) i \(q\).
Struktura \(\mathfrak{m}\) jest lewostronnie ograniczonym i prawostronnie nieskończonym łańcuchem, w którym interpretacja programu \(s\) jest następnikiem.
Napisać zdanie \(\varphi\) logiki PDL, które wyliczone w początkowym stanie łańcucha wyraża następującą własność:
"Istnieje taki stan \(x\), od którego począwszy \(q\) jest zawsze prawdziwe (natomiast \(p\) może być prawdziwe albo fałszywe), a we wszystkich stanach od początkowego aż do \(x\) włącznie \(p\) jest zawsze prawdziwe (natomiast \(q\) może być prawdziwe albo fałszywe)."
Zadanie 12
Niech w sygnaturze będzie jeden program atomowy \(s\) i jedna zmienna zdaniowa \(p\).
Struktura \(\mathfrak{m}\) jest lewostronnie ograniczonym i prawostronnie nieskończonym łańcuchem, w którym interpretacja programu \(s\) jest następnikiem. Strukturę \(\mathfrak{m}\) można naturalnie traktować jako nieskończony ciąg zerojedynkowy: tam gdzie \(p\) jest prawdziwe, są jedynki, a tam gdzie jest fałszywe są zera.
Udowodnić, że dla dowolnego deterministycznego automatu skończonego \(A\) nad alfabetem \(\{0,1\}\) istnieje zdanie \(\varphi\) logiki PDL, które wyliczone w początkowym stanie łańcucha wyraża następującą własność:
"Jeśli \(w\) jest prefiksem słowa \(\mathfrak{m}\), oraz \(w\) nie jest akceptowane przez automat \(A\), to istnieje inne słowo \(v\) której jest akceptowane przez \(A\) i takie, że \(wv\) jest prefiksem \(\mathfrak{m}\)."
Zadanie 13
Rozważamy modele dla PDL postaci skończonego łańcucha złożonego z dwóch programów atomowych: \(u\) i \(v\). Między każdymi dwoma kolejnymi stanami przechodzi jeden i tylko jeden z tych programów. Zmienne zdaniowe są dwie: \(p\) prawdziwa tylko w pierwszym stanie łańcucha i \(k\) prawdziwa tylko w ostatnim stanie. Innych zmiennych zdaniowych nie ma.
Każdą taką strukturę można naturalnie uważać również za strukturę pierwszego rzędu, wówczas \(u\) i \(v\) są relacjami dwuargumentowymi a \(p\) i \(k\) relacjami jednoargumentowymi.
Udowodnić, że dla każdego zdania \(\varphi\) logiki MSO istnieje zdanie \(\phi\) logiki PDL takie, że dla każdej struktury \(\mathfrak{A}\) jak powyżej, \(\phi\) jest prawdziwe w stanie początkowym struktury \(\mathfrak{A}\) wtedy i tylko wtedy, gdy \(\mathfrak{A}\models\varphi\).
