Logika temporalna

Logika temporalna – logika umożliwiająca rozważanie zależności czasowych bez wprowadzania czasu explicite. Pierwotnie służyła jako narzędzie do filozoficznych rozważań nad naturą czasu, dzisiaj jest używana głównie w informatyce.

Czas można wprowadzić do zwykłego rachunku predykatów pierwszego rzędu. Np. aby powiedzieć, że zawsze, kiedy jedzie pociąg, szlaban musi być opuszczony (żeby uniknąć wypadku), oraz że dla każdej chwili szlaban kiedyś się podniesie (aby samochody mogły w końcu przejechać), możemy napisać:

Dowodzenie twierdzeń w tak ogólnej notacji może być jednak trudne.

Z tego powodu dodaje się do rachunku zdań bez kwantyfikatorów pewne operatory modalne. Brak kwantyfikatorów umożliwia nam łatwe dowodzenie twierdzeń, zaś operatory modalne umożliwiają nam rozważanie zależności czasowych.

Logik temporalnych jest wiele. Można je jednak podzielić na dwie grupy – te, które zakładają liniową strukturę czasu, oraz te, które zakładają rozgałęzioną strukturę czasu. Logiki temporalne zazwyczaj operują czasem składającym się z wydarzeń dyskretnych, choć możliwe są też logiki używające czasu ciągłego.

Operatory i

Stwórzmy prostą logikę temporalną, w której czas się nie rozgałęzia, i nie interesuje nas, czy jest dyskretny, czy ciągły. W takiej logice dozwolone są dowolne zmienne zdaniowe ( itd.), wszystkie spójniki logiczne ( itd.), oraz para operatorów – i

  • oznacza, że od danego momentu już zawsze będzie miało miejsce
  • oznacza, że kiedyś w przyszłości będzie miało miejsce

W tak prostej logice można już zbudować kilka twierdzeń na temat czasu:

– jeśli będzie zachodziło zawsze, to zajdzie w pewnym konkretnym momencie w przyszłości.
zachodzi zawsze wtedy i tylko wtedy, gdy w żadnym momencie przyszłości nie będzie zachodziło

Operatory te można składać:

– kiedyś zajdzie, że kiedyś zajdzie oznacza po prostu, że kiedyś zajdzie
– zawsze będzie, że zawsze będzie oznacza po prostu, że zawsze będzie
– kiedyś zajdzie, że już zawsze będzie – czyli od pewnego momentu, zachodzić już będzie zawsze.
– zawsze będzie, że kiedyś zajdzie – czyli w każdym momencie mamy gdzieś przed sobą jakieś wystąpienie Czyli nigdy nie będzie tak, że już nigdy nie nastąpi W przypadku dyskretnym oznacza to, że zajdzie nieskończenie wiele razy.

Mając te operatory, łatwo możemy zdefiniować zachowanie szlabanu kolejowego:

– zawsze jeśli pociąg jedzie, to szlaban jest opuszczony.
– nigdy nie będzie tak, że szlaban będzie już cały czas opuszczony.

Operatory i

i pozwalają na umiejscawianie zjawisk w czasie, ale nie dają nam wielu możliwości przedstawiania zależności czasowych pomiędzy zjawiskami. Do tego służą dwa kolejne operatory:

– kiedyś nastąpi Do czasu jego pierwszego wystąpienia zawsze będzie
będzie zachodziło tak długo, aż nie zajdzie

Zależności między nimi to:

Używając tych operatorów można przedstawić oraz

Tak więc wszystkie 4 operatory można przedstawić używając jedynie lub jedynie Nie jest to jednak rozwiązanie praktyczne.

Ważniejsze twierdzenia logiki

– Jeśli zawsze z tego że wynika że to jeśli zawsze to zawsze

Czas dyskretny i operator

Podzielmy czas na dyskretne momenty, tak że w każdym momencie stan świata nie ulega zmianie, a przejścia z jednego momentu do drugiego są natychmiastowe.

Struktura czasu w świecie rzeczywistym jest inna, ale np. jest nią struktura wydarzeń zachodzących wewnątrz procesora – każde wydarzenie potrafimy przyporządkować konkretnemu wskazaniu zegara. Jeśli struktura czasu jest nam właściwie obojętna, możemy traktować ją jako dyskretną, nawet jeśli nie ma ona takiego charakteru, gdyż upraszcza to wiele obliczeń.

W logikach z czasem dyskretnym można zdefiniować operator oznaczający, że nastąpi w następnej chwili. oznacza więc, że nastąpi za 2 chwile, za 5 chwil itd.

Przykłady twierdzeń z użyciem

– zawsze, jeśli w pewnej chwili zachodzi to w następnej nie będzie zachodziło,
kiedyś będzie prawdziwe, a potem przestanie, równoważne
kiedyś będzie prawdziwe, a w następnej chwili będzie fałszywe (niemożliwe do wyrażenia bez ).

Logika LTL

Do najprostszych logik temporalnych należy linear temporal logic (liniowa logika temporalna), używająca dyskretnego i liniowego modelu czasu.

Operatorami tej logiki są:

  • (globally ) mówiący, że zachodzi w tej chwili, oraz że będzie zachodziło w każdym momencie w przyszłości (choć być może nie zachodziło w przeszłości),
  • (finally ) mówiący, że kiedyś w przyszłości zajdzie
  • (next ) mówiący, że w następnej chwili czasu zajdzie
  • ( until ) mówiący, że kiedyś w przyszłości zajdzie a do tego czasu będzie zachodzić
  • ( release ) mówiący, że zachodzi tak długo, aż zajdzie lub zachodzi zawsze, gdy nigdy nie zajdzie.

Wszystkie operatory można wyrazić za pomocą oraz

Zawsze będzie
Nieprawda, że kiedyś nastąpi nie-
Kiedyś nastąpi
Kiedyś nastąpi a do tego czasu zawsze będzie zachodziło prawda.
(negacja przeniesiona na drugą stronę dla łatwiejszego zrozumienia)
Nieprawda, że będzie zachodziło aż do momentu, w którym nastąpi
Zajdzie kiedyś nie- a do czasu, w którym zajdzie, zawsze będzie zachodziło nie-

Logika

Logika (computation tree logic) to rozszerzenie logiki LTL na rozgałęziające się modele czasu. Do operatorów LTL dochodzą jeszcze:

– dla każdej ścieżki zachodzi
– istnieje taka ścieżka obliczeń, że

Na składanie operatorów nałożone jest jedno ograniczenie: do żadnego operatora LTL-owskiego nie da się dojść, nie przechodząc przez operator ścieżkowy.

Czyli np. nie jest poprawną formułą ale nimi są.

Logika CTL

Logika to ograniczenie logiki w którym operatory mogą występować tylko parami – operator ścieżkowy, operator stanowy – i

Operatory te można przepisać za pomocą jedynie i

Linki zewnętrzne