Logika temporalna

Ten artykuł od 2012-11 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła, najlepiej w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu. Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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

${\displaystyle \forall t.\;{\mbox{pociag jedzie}}(t)\to \neg {\mbox{szlaban podniesiony}}(t),}$

${\displaystyle \forall t.\;\exists t'>t.\;{\mbox{szlaban podniesiony}}(t').}$

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 ${\displaystyle G}$ i ${\displaystyle F}$

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 (${\displaystyle p,}$ ${\displaystyle q,}$ ${\displaystyle r}$ itd.), wszystkie spójniki logiczne (${\displaystyle \land ,}$ ${\displaystyle \lor ,}$ ${\displaystyle \to ,}$ ${\displaystyle \equiv ,}$ ${\displaystyle \neg }$ itd.), oraz para operatorów – ${\displaystyle G}$ i ${\displaystyle F.}$

• ${\displaystyle G\phi }$ oznacza, że od danego momentu już zawsze będzie miało miejsce ${\displaystyle \phi .}$
• ${\displaystyle F\phi }$ oznacza, że kiedyś w przyszłości będzie miało miejsce ${\displaystyle \phi .}$

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

${\displaystyle G\phi \to F\phi }$ – jeśli ${\displaystyle \phi }$ będzie zachodziło zawsze, to ${\displaystyle \phi }$ zajdzie w pewnym konkretnym momencie w przyszłości.

${\displaystyle G\phi \equiv \neg F\neg \phi }$ – ${\displaystyle \phi }$ zachodzi zawsze wtedy i tylko wtedy, gdy w żadnym momencie przyszłości nie będzie zachodziło ${\displaystyle \neg \phi .}$

Operatory te można składać:

${\displaystyle FF\phi =F\phi }$ – kiedyś zajdzie, że kiedyś zajdzie ${\displaystyle \phi }$ oznacza po prostu, że kiedyś zajdzie ${\displaystyle \phi .}$

${\displaystyle GG\phi =G\phi }$ – zawsze będzie, że zawsze będzie ${\displaystyle \phi }$ oznacza po prostu, że zawsze będzie ${\displaystyle \phi .}$

${\displaystyle FG\phi }$ – kiedyś zajdzie, że już zawsze będzie ${\displaystyle \phi }$ – czyli od pewnego momentu, ${\displaystyle \phi }$ zachodzić już będzie zawsze.

${\displaystyle GF\phi =\neg FG\neg \phi }$ – zawsze będzie, że kiedyś zajdzie ${\displaystyle \phi }$ – czyli w każdym momencie mamy gdzieś przed sobą jakieś wystąpienie ${\displaystyle \phi .}$ Czyli nigdy nie będzie tak, że już nigdy nie nastąpi ${\displaystyle \phi .}$ W przypadku dyskretnym oznacza to, że ${\displaystyle \phi }$ zajdzie nieskończenie wiele razy.

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

${\displaystyle G\;({\mbox{pociag jedzie}}\to \neg {\mbox{szlaban podniesiony}})}$ – zawsze jeśli pociąg jedzie, to szlaban jest opuszczony.

${\displaystyle GF\;{\mbox{szlaban podniesiony}}}$ – nigdy nie będzie tak, że szlaban będzie już cały czas opuszczony.

Operatory ${\displaystyle U}$ i ${\displaystyle R}$

${\displaystyle G}$ i ${\displaystyle 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:

${\displaystyle \phi U\psi }$ – kiedyś nastąpi ${\displaystyle \psi .}$ Do czasu jego pierwszego wystąpienia zawsze będzie ${\displaystyle \phi .}$

${\displaystyle \phi R\psi }$ – ${\displaystyle \psi }$ będzie zachodziło tak długo, aż nie zajdzie ${\displaystyle \phi .}$

Zależności między nimi to:

${\displaystyle \phi U\psi =(F\psi )\land (\psi R\phi ),}$

${\displaystyle \phi R\psi =(G\neg \phi )\lor (\psi U\phi ),}$

${\displaystyle \phi U\psi =\neg (\neg \psi R\neg \phi ),}$

${\displaystyle \phi R\psi =\neg (\neg \psi U\neg \phi ).}$

Używając tych operatorów można przedstawić ${\displaystyle G}$ oraz ${\displaystyle F{:}}$

${\displaystyle F\phi =\top U\phi ,}$

${\displaystyle G\phi =\phi R\bot .}$

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

Ważniejsze twierdzenia logiki

${\displaystyle (p\wedge q)Ur\equiv (pUr)\wedge (qUr)}$

${\displaystyle pU(q\vee r)\equiv pU(q\vee r)}$

${\displaystyle (pUr)\vee (qUr)\implies (p\vee q)Ur}$

${\displaystyle pU(q\wedge r)\implies pU(q\wedge r)}$

${\displaystyle G(p\wedge q)\equiv ((Gp)\wedge (Gq))}$

${\displaystyle G(p\implies q)\implies ((Gp)\implies (Gq))}$ – Jeśli zawsze z tego że ${\displaystyle p}$ wynika że ${\displaystyle q,}$ to jeśli zawsze ${\displaystyle p}$ to zawsze ${\displaystyle q}$

Czas dyskretny i operator ${\displaystyle X}$

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

Przykłady twierdzeń z użyciem ${\displaystyle X{:}}$

${\displaystyle G(p\implies X\neg p)}$ – zawsze, jeśli w pewnej chwili zachodzi ${\displaystyle p,}$ to w następnej nie będzie zachodziło,

${\displaystyle F(p\land X\neg p)}$ – ${\displaystyle p}$ kiedyś będzie prawdziwe, a potem przestanie, równoważne ${\displaystyle F(p\land F\neg p),}$

${\displaystyle F(p\land X\neg q)}$ – ${\displaystyle p}$ kiedyś będzie prawdziwe, a w następnej chwili ${\displaystyle q}$ będzie fałszywe (niemożliwe do wyrażenia bez ${\displaystyle X}$).

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

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

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

${\displaystyle G\phi =\neg F\neg \phi .}$

Zawsze będzie ${\displaystyle \phi .}$

Nieprawda, że kiedyś nastąpi nie-${\displaystyle \phi .}$

${\displaystyle F\phi =\top U\phi .}$

Kiedyś nastąpi ${\displaystyle \phi .}$

Kiedyś nastąpi ${\displaystyle \phi ,}$ a do tego czasu zawsze będzie zachodziło prawda.

${\displaystyle \neg (\phi R\psi )=\neg \phi U\neg \psi .}$ (negacja przeniesiona na drugą stronę dla łatwiejszego zrozumienia)

Nieprawda, że ${\displaystyle \psi }$ będzie zachodziło aż do momentu, w którym nastąpi ${\displaystyle \phi }$

Zajdzie kiedyś nie-${\displaystyle \psi ,}$ a do czasu, w którym zajdzie, zawsze będzie zachodziło nie-${\displaystyle \phi }$

Logika ${\displaystyle CTL^{*}}$

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

${\displaystyle A\phi }$ – dla każdej ścieżki zachodzi ${\displaystyle \phi ,}$

${\displaystyle E\phi }$ – istnieje taka ścieżka obliczeń, że ${\displaystyle \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. ${\displaystyle G\phi }$ nie jest poprawną formułą ${\displaystyle CTL^{*},}$ ale ${\displaystyle AG\phi ,}$ ${\displaystyle EG\phi ,}$ ${\displaystyle (AG\phi )\lor \neg (EF\psi )}$ nimi są.

Logika CTL

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

Operatory te można przepisać za pomocą jedynie ${\displaystyle EU,}$ ${\displaystyle EG}$ i ${\displaystyle EX.}$

Linki zewnętrzne

• ValentinV. Goranko ValentinV., AntonyA. Galton AntonyA., Temporal Logic, [w:] Stanford Encyclopedia of Philosophy [online], CSLI, Stanford University, 7 lutego 2020, ISSN 1095-5054 [dostęp 2020-02-15]  (ang.). (Logika temporalna)