Logika LTL – jedna z logik temporalnych. Jest oparta na liniowej strukturze czasu.
PLTL Jest to odmiana logiki LTL oparta na rachunku 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ł Oznaczenia: – 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 na rachunku 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
Kategoria:Logika temporalna