Informatyka MIMUW

Wyobraźmy sobie grę w kółko i krzyżyk, w której kratki znanego diagramu są ponumerowane od 1 do 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$.