Logika temporalna

Logika temporalna

Logika temporalna to narzędzie do analizy zależności czasowych bez bezpośredniego wprowadzania czasu. Początkowo miała zastosowanie w filozofii, obecnie znajduje szerokie zastosowanie w informatyce. Czas można wprowadzać do tradycyjnego rachunku predykatów, jednak dowodzenie twierdzeń w tej formie bywa trudne. Dlatego wprowadza się operatory modalne, które ułatwiają rozważania o czasie.

Logiki temporalne dzielą się na dwie główne grupy:

• liniowa struktura czasu
• rozgałęziona struktura czasu

Operacje zachodzące w logikach temporalnych zazwyczaj dotyczą zdarzeń dyskretnych, chociaż istnieją także logiki z czasem ciągłym.

Operatory G i F

W prostych logikach temporalnych można używać operatorów $G$ i $F$:

• $G\backslash phi$ oznacza, że od danego momentu $\backslash phi$ zawsze będzie zachodzić.
• $F\backslash phi$ oznacza, że w przyszłości $\backslash phi$ zajdzie.

Dzięki tym operatorom można formułować różne twierdzenia czasowe, takie jak:

• $G\backslash phi\; \backslash to\; F\backslash phi$ – jeśli $\backslash phi$ zawsze zachodzi, to zajdzie kiedyś w przyszłości.
• $GF\backslash phi\; =\; \backslash neg\; FG\; \backslash neg\; \backslash phi$ – zawsze, że kiedyś $\backslash phi$ zajdzie.

Operatory U i R

Operatory $\backslash phi\; U\; \backslash psi$ i $\backslash phi\; R\; \backslash psi$ pozwalają na określenie zależności czasowych pomiędzy zjawiskami.

• $\backslash phi\; U\; \backslash psi$ – oznacza, że kiedyś zajdzie $\backslash psi$, a do tego czasu $\backslash phi$ zawsze będzie prawdziwe.
• $\backslash phi\; R\; \backslash psi$ – $\backslash psi$ zachodzi tak długo, aż nie zajdzie $\backslash phi$.

Ważniejsze twierdzenia logiki

Niektóre istotne twierdzenia logiki temporalnej to:

• $(p\; \backslash wedge\; q)\; U\; r\; \backslash equiv\; (p\; U\; r)\; \backslash wedge\; (q\; U\; r)$
• $G\; (p\; \backslash wedge\; q)\; \backslash equiv\; ((G\; p)\; \backslash wedge\; (G\; q))$

Czas dyskretny i operator X

W logikach z czasem dyskretnym operator $X\backslash phi$ oznacza, że $\backslash phi$ nastąpi w następnej chwili. Przykłady twierdzeń z użyciem $X$ to:

• $G\; (p\; \backslash implies\; X\; \backslash neg\; p)$ – zawsze, gdy $p$ zachodzi, w następnej chwili nie będzie zachodziło.

Logika LTL

Linear Temporal Logic (LTL) jest jedną z podstawowych logik temporalnych, używającą dyskretnego modelu czasu. Jej operatory to:

• $G\backslash phi$ – $\backslash phi$ zachodzi w tej chwili i będzie zachodzić w przyszłości.
• $F\backslash phi$ – kiedyś w przyszłości zajdzie $\backslash phi$.

Logika CTL^* i CTL

Logika $CTL^*$ rozszerza LTL o operatory ścieżkowe, takie jak $A\backslash phi$ i $E\backslash phi$. W logice $CTL$ operatory mogą występować tylko parami, co ogranicza ich zastosowanie.

Linki zewnętrzne

* [https://www.rep.routledge.com/articles/thematic/tense-and-temporal-logic/v-1 Tense and temporal logic], Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].