Logika LTL

Struktura czasu

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

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

Język

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

Formuły

Niech ${\displaystyle WA}$ będzie zbiorem wyrażeń atomowych.

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

Prawdziwość formuł

• Oznaczenia:

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

• warunki prawdziwości podstawowych formuł:

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

Język

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

Formuły

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