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\to \{0,1\},$ $WA$ – zbiór wyrażeń atomowych

Język

• zmienne zdaniowe $p,q,r,\dots$
• spójniki zdaniowe rachunku zdań:
  • koniunkcja $(\wedge ),$
  • alternatywa $(\vee ),$
  • implikacja $(\Rightarrow ),$
  • równoważność $(\iff ),$
  • negacja $(\mathrm{\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 \mathrm{\neg }(\mathrm{\neg }\alpha U\mathrm{\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\mathrm{\perp })$
  • $F$ – $F\alpha$ oznacza, że $\alpha$ będzie prawdziwe w pewnym momencie w przyszłości $(F\alpha \equiv \mathrm{\top }U\alpha )$
  • $F^{\mathrm{\infty }}$ – $F^{\mathrm{\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^{\mathrm{\infty }}\alpha \equiv GF\alpha )$
  • $G^{\mathrm{\infty }}$ – $G^{\mathrm{\infty }}\alpha$ oznacza, że $\alpha$ będzie prawdziwe od pewnego momentu w przyszłości $(G^{\mathrm{\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 $\mathrm{\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\iff p\in L(s_i)$
$(M,s_i)\models (\alpha \wedge \beta )\iff ((M,s_i)\models \alpha )\wedge ((M,s_i)\models \beta )$
$(M,s_i)\models \mathrm{\neg }\alpha \iff \mathrm{\neg }(M,s_i)\models \alpha$
$(M,s_i)\models \alpha U\beta \iff {\mathrm{\exists }}_{k>i}(M,s_k)\models \beta \wedge (\mathrm{\forall }j:(i\le j<k)(M,s_j)\models \alpha ))$
$(M,s_i)\models X\alpha \iff (M,s_{i+1})\models \alpha$

PLTLFO

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

Język

• wszystkie elementy PLTL
• kwantyfikatory – $\mathrm{\forall },\mathrm{\exists }$
• znak równości $=$
• symbole predykatywne $P,Q,R,\dots$
• symbole funkcyjne $f,g,h,\dots$
• symbole stałe $c_1,c_2,\dots$
• zmienne $x_1,x_2,\dots$

Formuły

• termy:
  • zmienne,
  • stałe,
  • wyrażenia postaci: $f(t_1,t_2,\dots ,t_n),$ gdzie $t_i$ są stałymi bądź zmiennymi
• predykaty:
  • wyrażenia postaci: $P(t_1,t_2,\dots ,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: $\mathrm{\forall }x\alpha$ oraz $\mathrm{\exists }x\alpha ,$ gdzie $\alpha$ jest formułą, a $x$ jest zmienną.

Linki zewnętrzne

• Szablon:Cytuj
• Szablon:Cytuj
• Szablon:Cytuj