Logika LTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.
PLTL
Jest to odmiana logiki LTL oparta o rachunek zdań (bazująca wyłącznie na zmiennych zdaniowych).
Struktura czasu
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
- 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
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ł
– formuła jest prawdziwa w strukturze na ścieżce
– formuła jest prawdziwa w strukturze w stanie
- warunki prawdziwości podstawowych formuł:
PLTLFO
Odmiana logiki LTL oparta o rachunek predykatów pierwszego rzędu.
Język
- wszystkie elementy PLTL
- kwantyfikatory –
- znak równości
- symbole predykatywne
- symbole funkcyjne
- symbole stałe
- zmienne
Formuły
- 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
- PawełP. Głuchowski PawełP., Temporal Logic and Timed Automata, LTL logic [online], Politechnika Wrocławska [dostęp 2020-06-27] (ang.).
- AndrzejA. Oszer AndrzejA., Logiki temporalne [online] (pol.).
- ReuvenR. Yakar ReuvenR., Temporal Logic Theory and Applications [online], Uniwersytet Telawiwski, 6 grudnia 2007 (ang.).