Logika LTL

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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


PLTL[edytuj]

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

Struktura czasu[edytuj]

Strukturą czasu w PLTL jest struktura , gdzie:

  • - zbiór stanów: ,
  • - nieskończona ścieżka stanów: ,
  • - wartościowanie (przypisanie każdemu ze stanów wyrażeń, które są prawdziwe w tym stanie) , - zbiór wyrażeń atomowych)


Język[edytuj]

  • zmienne zdaniowe
  • spójniki zdaniowe rachunku zdań:
    • koniunkcja ( ) ,
    • alternatywa ( ) ,
    • implikacja ( ) ,
    • równoważność( ) ,
    • negacja ( )
  • operatory temporalne:
    • - oznacza, że w pewnym momencie w przyszłości będzie prawdziwe , a do tego momentu będzie prawdziwe
    • - oznacza, że w pewnym momencie w przyszłości będzie prawdziwe , a do tego momentu będzie prawdziwe
      ( )
    • - oznacza, że będzie prawdziwe w następnym momencie (oznaczany też jako )
    • - oznacza, że jest prawdziwe w każdym momencie ( )
    • - oznacza, że będzie prawdziwe w pewnym momencie w przyszłości ( )
    • - oznacza, że będzie prawdziwe w przyszłości w nieskończenie wielu momentach (zawsze z wyjątkiem pewnej skończonej liczby momentów) ( )
    • - oznacza, że będzie prawdziwe od pewnego momentu w przyszłości ( )
  • nawiasy

Formuły[edytuj]

Niech będzie zbiorem wyrażeń atomowych.

  • każde wyrażenie jest formułą
  • jeśli i są formułami, to i też są formułami
  • jeśli i są formułami, to i też są formułami

Prawdziwość formuł[edytuj]

  • Oznaczenia:

- formuła jest prawdziwa w strukturze na ścieżce
- formuła jest prawdziwa w strukturze w stanie

  • warunki prawdziwości podstawowych formuł:







PLTLFO[edytuj]

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

Język[edytuj]

  • wszystkie elementy PLTL
  • kwantyfikatory -
  • znak równości
  • symbole predykatywne
  • symbole funkcyjne
  • symbole stałe
  • zmienne

Formuły[edytuj]

  • termy:
    • zmienne,
    • stałe,
    • wyrażenia postaci: , gdzie są stałymi bądź zmiennymi
  • predykaty:
    • wyrażenia postaci: , gdzie są stałymi bądź zmiennymi
  • atomy:
    • stałe,
    • predykaty,
    • wyrażenia postaci: , gdzie i są stałymi bądź zmiennymi
  • formuły:
    • takie, jak w PLTL,
    • atomy,
    • wyrażenia postaci: oraz , gdzie jest formułą, a jest zmienną.


Linki zewnętrzne[edytuj]