Logika LTL


Logika LTL w encyklopedii

Z Wikipedii, wolnej encyklopedii Przejdź do nawigacji Przejdź do wyszukiwania

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

Spis treści

PLTL | edytuj kod

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

Struktura czasu | edytuj kod

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

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

Język | edytuj kod

  • zmienne zdaniowe p , q , r , {\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:
    • U {\displaystyle U} α 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 }
    • R {\displaystyle R} α R β {\displaystyle \alpha R\beta } oznacza, że β {\displaystyle \beta } będzie prawdziwe dopóki nie zacznie być prawdziwe α {\displaystyle \alpha } ( α R β ¬ ( ¬ α U ¬ β ) ) {\displaystyle (\alpha R\beta \equiv \neg (\neg \alpha U\neg \beta ))}
    • X {\displaystyle X} X α {\displaystyle X\alpha } oznacza, że α {\displaystyle \alpha } będzie prawdziwe w następnym momencie (oznaczany też jako {\displaystyle \circ } )
    • G {\displaystyle G} G α {\displaystyle G\alpha } oznacza, że α {\displaystyle \alpha } jest prawdziwe w każdym momencie ( G α α U ) {\displaystyle (G\alpha \equiv \alpha U\bot )}
    • F {\displaystyle F} F α {\displaystyle F\alpha } oznacza, że α {\displaystyle \alpha } będzie prawdziwe w pewnym momencie w przyszłości ( F α U α ) {\displaystyle (F\alpha \equiv \top U\alpha )}
    • F {\displaystyle F^{\infty }} F α {\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) ( F α G F α ) {\displaystyle (F^{\infty }\alpha \equiv GF\alpha )}
    • G {\displaystyle G^{\infty }} G α {\displaystyle G^{\infty }\alpha } oznacza, że α {\displaystyle \alpha } będzie prawdziwe od pewnego momentu w przyszłości ( G α F G α ) {\displaystyle (G^{\infty }\alpha \equiv FG\alpha )}
  • nawiasy

Formuły | edytuj kod

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

  • każde wyrażenie α W A {\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 α U β {\displaystyle \alpha U\beta } i X α {\displaystyle X\alpha } też są formułami

Prawdziwość formuł | edytuj kod

  • Oznaczenia:

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

  • warunki prawdziwości podstawowych formuł:

( M , s i ) p p L ( s i ) {\displaystyle (M,s_{i})\models p\Leftrightarrow p\in L(s_{i})}
( M , s i ) ( α β ) ( ( M , s i ) α ) ( ( M , s i ) β ) {\displaystyle (M,s_{i})\models (\alpha \wedge \beta )\Leftrightarrow ((M,s_{i})\models \alpha )\wedge ((M,s_{i})\models \beta )}
( M , s i ) ¬ α ¬ ( M , s i ) α {\displaystyle (M,s_{i})\models \neg \alpha \Leftrightarrow \neg (M,s_{i})\models \alpha }
( M , s i ) α U β k > i ( M , s k ) β ( j : ( i j < k ) ( M , s j ) α ) ) {\displaystyle (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 ) X α ( M , s i + 1 ) α {\displaystyle (M,s_{i})\models X\alpha \Leftrightarrow (M,s_{i+1})\models \alpha }

PLTLFO | edytuj kod

Odmiana logiki LTL oparta o rachunek predykatów pierwszego rzędu.

Język | edytuj kod

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

Formuły | edytuj kod

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

Linki zewnętrzne | edytuj kod

Na podstawie artykułu: "Logika LTL" pochodzącego z Wikipedii
OryginałEdytujHistoria i autorzy