Jest to odmiana logiki LTL oparta o rachunek zdań (bazująca wyłącznie na zmiennych zdaniowych).
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
- 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
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
– formuła jest prawdziwa w strukturze na ścieżce
– formuła jest prawdziwa w strukturze w stanie
- warunki prawdziwości podstawowych formuł:
Odmiana logiki LTL oparta o rachunek predykatów pierwszego rzędu.
- wszystkie elementy PLTL
- kwantyfikatory –
- znak równości
- symbole predykatywne
- symbole funkcyjne
- symbole stałe
- zmienne
- 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ą.