Logika temporalna

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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ć:

\forall t.\;\mbox{pociag jedzie}(t) \rightarrow \neg \mbox{szlaban podniesiony}(t)
\forall t.\;\exists t^\prime > t .\; \mbox{szlaban podniesiony}(t^\prime)

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 (p, q, r itd.), wszystkie spójniki logiczne (\and, \or, \rightarrow, \equiv, \neg itd.), oraz para operatorów – G i F.

G\phi oznacza, że od danego punktu już zawsze będzie miało miejsce \phi.

F\phi oznacza, że kiedyś w przyszłości będzie miało miejsce \phi.

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

G\phi \rightarrow F\phi – jeśli \phi będzie zachodziło zawsze, to \phi zajdzie w pewnym konkretnym momencie w przyszłości
G\phi \equiv \neg F\neg \phi\phi zachodzi zawsze wtedy i tylko wtedy, gdy w żadnym momencie przyszłości nie będzie zachodziło \neg \phi

Operatory te można składać:

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

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

G\; (\mbox{pociag jedzie} \rightarrow \neg \mbox{szlaban podniesiony}) – zawsze jeśli pociąg jedzie, to szlaban jest opuszczony
GF\; \mbox{szlaban podniesiony} – nigdy nie będzie tak, że szlaban będzie już cały czas opuszczony

Operatory U i R[edytuj | edytuj kod]

G i F 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:

\phi U \psi – kiedyś nastąpi \psi. Do czasu jego pierwszego wysąpienia zawsze będzie \phi.
\phi R \psi\psi będzie zachodziło tak długo, aż nie zajdzie \phi.

Zależności między nimi to:

\phi U \psi = (F \psi) \and (\psi R \phi)
\phi R \psi = (G\neg\phi) \or (\psi U \phi)
\phi U \psi = \neg (\neg \psi R \neg \phi)
\phi R \psi = \neg (\neg \psi U \neg \phi)

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

F \phi = \top U \phi
G \phi = \phi R \bot

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

Ważniejsze twierdzenia logiki[edytuj | edytuj kod]

(p \wedge q) U r \equiv (p U r) \wedge (q U r)
p U (q \vee r) \equiv p U (q \vee r)
(p U r) \vee (q U r) \implies (p \vee q) U r
p U (q \wedge r) \implies p U (q \wedge r)
G (p \wedge q) \equiv ((G p) \wedge (G q))
G (p \implies q) \implies ((Gp) \implies (Gq)) – Jeśli zawsze z tego że p wynika że q, to jeśli zawsze p to zawsze q

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 X\phi oznaczający, że \phi nastąpi w następnej chwili. XX\phi oznacza więc, że nastąpi za 2 chwile, XXXXX\phi za 5 chwil itd.

Przykłady twierdzeń z użyciem X:

G (p \implies X \neg p) – zawsze, jeśli w pewnej chwili zachodzi p, to w następnej nie będzie zachodziło
F (p \and X \neg p) p kiedyś będzie prawdziwe, a potem przestanie, równoważne F (p \and F \neg p)
F (p \and X \neg q) p kiedyś będzie prawdziwe, a w następnej chwili q będzie fałszywe (niemożliwe do wyrażenia bez X)

Logika LTL[edytuj | edytuj kod]

Information icon.svg Osobny artykuł: 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ą:

  • G\phi (globally \phi) mówiący, że \phi 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).
  • F\phi (finally \phi) mówiący, że kiedyś w przyszłości zajdzie \phi
  • X\phi (next \phi) mówiący, że w następnej chwili czasu zajdzie \phi
  • \phi U\psi (\phi until \psi) mówiący, że kiedyś w przyszłości zajdzie \psi, a do tego czasu będzie zachodzić \phi
  • \phi R\psi (\phi release \psi) mówiący, że \psi zachodzi tak długo, aż zajdzie \phi lub zachodzi zawsze, gdy \phi nigdy nie zajdzie

Wszystkie operatory można wyrazić za pomocą X\phi oraz \phi U\psi:

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

Logika CTL^*[edytuj | edytuj kod]

Information icon.svg Osobny artykuł: Logika CTL*.

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

A\phi – dla każdej ścieżki zachodzi \phi
E\phi – istnieje taka ścieżka obliczeń, że \phi

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. G \phi nie jest poprawną formułą CTL^*, ale AG \phi, EG \phi, (AG \phi) \or \neg (EF \psi) nimi są.

Logika CTL[edytuj | edytuj kod]

Information icon.svg Osobny artykuł: Logika CTL.

Logika CTL to ograniczenie logiki CTL^*, w którym operatory mogą występować tylko parami – operator ścieżkowy, operator stanowy – AX, EX, AG, EG, AF, EF, AU, EU, AR i ER.

Operatory te można przepisać za pomocą jedynie EU, EG i EX.