Logika temporalna – Wikipedia, wolna encyklopedia
Ten artykuł od 2012-11 wymaga zweryfikowania podanych informacji. |
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 G i F
[edytuj | edytuj kod]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 U i R
[edytuj | edytuj kod]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
[edytuj | edytuj kod]- – Jeśli zawsze z tego że wynika że to jeśli zawsze to zawsze
Czas dyskretny i operator X
[edytuj | edytuj kod]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
[edytuj | edytuj kod]- Osobny artykuł:
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 CTL*
[edytuj | edytuj kod]- Osobny artykuł:
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
[edytuj | edytuj kod]- Osobny artykuł:
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
[edytuj | edytuj kod]- Valentin Goranko , Antony Galton , Temporal Logic, [w:] Stanford Encyclopedia of Philosophy, CSLI, Stanford University, 7 lutego 2020, ISSN 1095-5054 [dostęp 2020-02-15] (ang.). (Logika temporalna)
Tense and temporal logic (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].