Logika LTL

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

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

PLTL[edytuj | edytuj kod]

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

Struktura czasu[edytuj | edytuj kod]

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 | edytuj kod]

  • 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 będzie prawdziwe dopóki nie zacznie być 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 | edytuj kod]

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 | edytuj kod]

  • 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 | edytuj kod]

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

Język[edytuj | edytuj kod]

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

Formuły[edytuj | edytuj kod]

  • 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 | edytuj kod]