Logika Temporalna Czasu Liniowego LTL

Zad. 1

Sformalizować w LTL własność "\(\varphi\) jest prawdziwe we
wszystkich parzystych stanach, a fałszywe we wszystkich nieparzystych"

Zad. 2
Pokazać, że nie da się w LTL sformalizować własności \(\varphi\)
jest prawdziwe we wszystkich parzystych stanach".

Zad. 3
Dokonać separacji kilku dodatkowych przypadków w dowodzie tw. Gabbaya.

Zad. 4
Jak można by sformułować twierdzenie o separacji dla logiki pierwszego rzędu, tak aby było ono prawdziwe?

Wskazówka 1

Ściśle rzecz biorąc, dla każdej formuły \(\varphi(x)\) logiki pierwszego rzędu nad modelami-słowami poszukujemy jej równoważnego (nad modelami-słowami) wyrażenia w postaci kombinacji boolowskiej formuł również z jedną zmienną wolną \(x\), z których każda wyraża odwołuje się wyłącznie do elementów wcześniejszych lub równych \(x\) w porządku obecnym w modelach.

Wskazówka 2

Daną formułę logiki pierwszego rzędu \(\varphi(x)\) możemy uważać za formułę czasu przeszłego, jeśli wszystkie kwantyfikatory w niej użyte są w następujący sposób: \(\forall z (z\leq x\to \psi)\) lub \(\exists z (z\leq x\land \psi)\).
Analogicznie można zdefiniować formułą czasu przyszłego.

Zad. 5
Proszę sformułować i udowodnić analogiczne twierdzenie o separacji dla monadycznej logiki drugiego rzędu.

Wskazówka 1

Pojęcia "formuła czasu przeszłego" i "formuła czasu przyszłego" odnoszące się do formuł logiki monadycznej drugiego rzędu rzędu \(\varphi(x)\) z jedną wolną zmienną pierwszego rzędu można wzorować na poprzednio opisanym sposobie dl alogiki pierwszego rzędu. Trzeba tylko wymyślić sposób relatywizacji zmiennych drugiego rzędu.

Wskazówka 2

W celu udowodnienia twierdzenia o sepracji należy odpowiednio posłużyć się tw. Buchi-Elgota i równoważności logiki monadycznej drugiego rzędu i automatów skończonych. Ze względu na to, że tw. Buchi-Elgota mówi o zdaniach, a my mamy formuły z jedną zmienną wolną, zależy tę zmienną zamienić na dodatkowy symbol relacji unarnej.
Po tej operacji, separacja to zadanie o automatach skończonych, możliwe do rozwiązania metodami z wykładu JAiO.

Zad. 6

"Słaby until", oznaczany \(\mathtt{U}_w\), to temporalny operator dwuargumentowy taki, że \(\alpha\mathtt{U}_w\beta\) jest równoważna formule \((\alpha\mathtt{U}\beta)\lor\mathtt{G}\alpha\). ``Słaby until'' jest więc skrótem notacyjnym.

Wykazać, że dysponując operatorami \(\mathtt{X}\) i \(\mathtt{U}_w\) może zdefiniować standardowy unitl \(\mathtt{U}\).
Wynika stąd, że definicję logiki LTL można by równie dobrze oprzeć o słaby until.