Logika LTL

Logika LTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.

PLTL

Jest to odmiana logiki LTL oparta na rachunku zdań (bazująca wyłącznie na zmiennych zdaniowych).

Struktura czasu

Strukturą czasu w PLTL jest struktura $M=(S,X,L),$ gdzie:

• $S$ – zbiór stanów: $S=\{s_{0},s_{1},s_{2},...\},$
• $X$ – nieskończona ścieżka stanów: $X=(s_{0},s_{1},s_{2},...),$
• $L$ – wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie) $L:S\times WA\rightarrow \{0,1\},$ $WA$ – zbiór wyrażeń atomowych

Język

• zmienne zdaniowe $p,q,r,\ldots$
• spójniki zdaniowe rachunku zdań:
  • koniunkcja $(\wedge ),$
  • alternatywa $(\vee ),$
  • implikacja $(\Rightarrow ),$
  • równoważność $(\Leftrightarrow ),$
  • negacja $(\neg )$
• operatory temporalne:
  • $U$ – $\alpha U\beta$ oznacza, że w pewnym momencie w przyszłości będzie prawdziwe $\beta ,$ a do tego momentu będzie prawdziwe $\alpha$
  • $R$ – $\alpha R\beta$ oznacza, że $\beta$ będzie prawdziwe dopóki nie zacznie być prawdziwe $\alpha$ $(\alpha R\beta \equiv \neg (\neg \alpha U\neg \beta ))$
  • $X$ – $X\alpha$ oznacza, że $\alpha$ będzie prawdziwe w następnym momencie (oznaczany też jako $\circ$)
  • $G$ – $G\alpha$ oznacza, że $\alpha$ jest prawdziwe w każdym momencie $(G\alpha \equiv \alpha U\bot )$
  • $F$ – $F\alpha$ oznacza, że $\alpha$ będzie prawdziwe w pewnym momencie w przyszłości $(F\alpha \equiv \top U\alpha )$
  • $F^{\infty }$ – $F^{\infty }\alpha$ oznacza, że $\alpha$ będzie prawdziwe w przyszłości w nieskończenie wielu momentach (zawsze z wyjątkiem pewnej skończonej liczby momentów) $(F^{\infty }\alpha \equiv GF\alpha )$
  • $G^{\infty }$ – $G^{\infty }\alpha$ oznacza, że $\alpha$ będzie prawdziwe od pewnego momentu w przyszłości $(G^{\infty }\alpha \equiv FG\alpha )$
• nawiasy

Formuły

Niech $WA$ będzie zbiorem wyrażeń atomowych.

• każde wyrażenie $\alpha \in WA$ jest formułą
• jeśli $\alpha$ i $\beta$ są formułami, to $\alpha \wedge \beta$ i $\neg \alpha$ też są formułami
• jeśli $\alpha$ i $\beta$ są formułami, to $\alpha U\beta$ i $X\alpha$ też są formułami

Prawdziwość formuł

• Oznaczenia:

$(M,x)\models \alpha$ – formuła $\alpha$ jest prawdziwa w strukturze $M$ na ścieżce $x$
$(M,s_{i})\models \alpha$ – formuła $\alpha$ jest prawdziwa w strukturze $M$ w stanie $s_{i}$

• warunki prawdziwości podstawowych formuł:

$(M,s_{i})\models p\Leftrightarrow p\in L(s_{i})$
$(M,s_{i})\models (\alpha \wedge \beta )\Leftrightarrow ((M,s_{i})\models \alpha )\wedge ((M,s_{i})\models \beta )$
$(M,s_{i})\models \neg \alpha \Leftrightarrow \neg (M,s_{i})\models \alpha$
$(M,s_{i})\models \alpha U\beta \Leftrightarrow \exists _{k>i}(M,s_{k})\models \beta \wedge (\forall j:(i\leq j<k)\quad (M,s_{j})\models \alpha ))$
$(M,s_{i})\models X\alpha \Leftrightarrow (M,s_{i+1})\models \alpha$

PLTLFO

Odmiana logiki LTL oparta na rachunku predykatów pierwszego rzędu.

Język

• wszystkie elementy PLTL
• kwantyfikatory – $\forall ,\exists$
• znak równości $=$
• symbole predykatywne $P,Q,R,\ldots$
• symbole funkcyjne $f,g,h,\ldots$
• symbole stałe $c_{1},c_{2},\ldots$
• zmienne $x_{1},x_{2},\ldots$

Formuły

• termy:
  • zmienne,
  • stałe,
  • wyrażenia postaci: $f(t_{1},t_{2},\ldots ,t_{n}),$ gdzie $t_{i}$ są stałymi bądź zmiennymi
• predykaty:
  • wyrażenia postaci: $P(t_{1},t_{2},\ldots ,t_{n}),$ gdzie $t_{i}$ są stałymi bądź zmiennymi
• atomy:
  • stałe,
  • predykaty,
  • wyrażenia postaci: $t_{1}=t_{2},$ gdzie $t_{1}$ i $t_{2}$ są stałymi bądź zmiennymi
• formuły:
  • takie, jak w PLTL,
  • atomy,
  • wyrażenia postaci: $\forall x\ \alpha$ oraz $\exists x\ \alpha ,$ gdzie $\alpha$ jest formułą, a $x$ jest zmienną.

Linki zewnętrzne

• PawełP. Głuchowski PawełP., Temporal Logic and Timed Automata, LTL logic [online], Politechnika Wrocławska [dostęp 2020-06-27]  (ang.).
• AndrzejA. Oszer AndrzejA., Logiki temporalne [online]  (pol.).
• ReuvenR. Yakar ReuvenR., Temporal Logic Theory and Applications [online], Uniwersytet Telawiwski, 6 grudnia 2007  (ang.).