Logika temporalna

Z Wikipedii

Logika temporalna to 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. żeby powiedzieć, że zawsze kiedy jedzie pociąg szlaban musi być opuszczony (żeby uniknąć wypadku), oraz że dla każdej chwili czasu szlaban kiedyś się podniesie (żeby 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ą na czasie składającym się z dyskretnych wydarzeń, choć możliwe są też logiki używające czasu ciągłego.

[edytuj] Operatory $G$ i $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 logice takiej 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 φ$ oznacza, że od danego punktu już zawsze będzie miało miejsce $φ$ .

$F φ$ 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:

$G\phi \rightarrow F\phi$ – jeśli

φ

będzie zachodziło zawsze, to

φ

zajdzie w pewnym konkretnym momencie w przyszłości

$G\phi \equiv \neg F\neg \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ć:

F F φ = F φ

– kiedyś zajdzie, że kiedyś zajdzie

φ

oznacza po prostu, że kiedyś zajdzie

φ

G G φ = G φ

– zawsze będzie, że zawsze będzie

φ

oznacza po prostu, że zawszę będzie

φ

F G φ

– kiedyś zajdzie, że już zawszę będzie

φ

– czyli od pewnego momentu,

φ

zachodzić już będzie zawsze

$GF\phi = \neg FG \neg \phi$ – 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:

$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

[edytuj] Operatory $U$ i $R$

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

φ U ψ

– kiedyś nastąpi

ψ

. Do czasu jego pierwszego wysąpienia zawsze będzie

φ

φ R ψ

–

ψ

będzie zachodziło tak długo, aż nie zajdzie

φ

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.

[edytuj] Ważniejsze twierdzenia logiki

$(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

[edytuj] Czas dyskretny i operator $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 rzeczywistym świecie nie jest taka – ale jest nią np. struktura wydarzeń zachodzących wewnątrz procesora – każde wydarzenie potrafimy przyporządkować do konkretnego taktu 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 dyskretnym czasem można zdefiniować operator $X φ$ , oznaczający że $φ$ nastąpi w następnej chwili. $X X φ$ oznacza więc że nastąpi za 2 chwile, $X X X X X φ$ 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

)

[edytuj] 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 φ$ (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).
$F φ$ (finally $φ$ ), mówiący, że kiedyś w przyszłości zajdzie $φ$
$X φ$ (next $φ$ ), mówiący, że w następnej chwili czasu zajdzie $φ$
$φ U ψ$ ( $φ$ until $ψ$ ), mówiący, że kiedyś w przyszłości zajdzie $ψ$ , a do tego czasu będzie zachodzić $φ$
$φ R ψ$ ( $φ$ release $ψ$ ), mówiący, że $ψ$ zachodzi tak długo, aż zajdzie $φ$ , lub już zawsze, jeśli $φ$ nigdy nie zajdzie

Wszystkie operatory można wyrazić za pomocą $X φ$ oraz $φ U ψ$ :

$G\phi = \neg F \neg \phi$ .

Zawsze będzie

φ

Nieprawda że kiedyś nastąpi nie-

φ

$F\phi = \top U \phi$ .

Kiedyś nastąpi

φ

Kiedyś nastąpi

φ

, 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

ψ

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-

φ

[edytuj] Logika $C T L *$

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

A φ

– dla każdej ścieżki zachodzi

φ

E φ

– 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. $G φ$ nie jest poprawną formułą $C T L *$ , ale $A G φ$ , $E G φ$ , $(AG \phi) \or \neg (EF \psi)$ nimi są.

[edytuj] Logika CTL

Logika $C T L$ to ograniczenie logiki $C T L *$ , w którym operatory mogą występować tylko parami – operator ścieżkowy, operator stanowy – $A X$ , $E X$ , $A G$ , $E G$ , $A F$ , $E F$ , $A U$ , $E U$ , $A R$ i $E R$ .

Operatory te można przepisać za pomocą jedynie $E U$ , $E G$ i $E X$ .

Kategoria: Logika matematyczna

See also ebooksgratis.com: no banners, no cookies, totally FREE.

Logika temporalna

Z Wikipedii

Spis treści

[edytuj] Operatory $G$ i $F$

[edytuj] Operatory $U$ i $R$

[edytuj] Ważniejsze twierdzenia logiki

[edytuj] Czas dyskretny i operator $X$

[edytuj] Logika LTL

[edytuj] Logika $C T L *$

[edytuj] Logika CTL

Views

nawigacja

zmiany

dla edytorów

Szukaj

W innych językach

See also ebooksgratis.com: no banners, no cookies, totally FREE.

Logika temporalna

Z Wikipedii

Spis treści

[edytuj] Operatory G i F

[edytuj] Operatory U i R

[edytuj] Ważniejsze twierdzenia logiki

[edytuj] Czas dyskretny i operator X

[edytuj] Logika LTL

[edytuj] Logika CTL *

[edytuj] Logika CTL

Views

nawigacja

zmiany

dla edytorów

Szukaj

W innych językach

[edytuj] Operatory $G$ i $F$

[edytuj] Operatory $U$ i $R$

[edytuj] Czas dyskretny i operator $X$

[edytuj] Logika $C T L *$