Linear Temporal Logic (LTL) | Informatyka MIMUW

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.