LOGIKA TEMPORALNA
P. Jedynak, J. Stochel
11.1. Wprowadzenie
Pocz ˛atki logiki si˛egaj ˛a czasów staro˙zytnych. Greccy filozofowie uczyli swo-ich adeptów retoryki, czyli sztuki publicznego przemawiania. W skład tej nauki wchodziły tak˙ze podstawy logiki, dzi˛eki którym wszyscy mówcy uczestnicz ˛acy w dyskusji korzystali z tych samych reguł wnioskowania. Tak˙ze sama logika tem-poralna — główna bohaterka tego rozdziału, miała korzenie filozoficzne. Pier-wotnie u˙zywano jej przy prowadzeniu rozwa˙za ´n nad natur ˛a czasu. To wła´snie czas jest w niej najistotniejszy. Logika ta umo˙zliwia rozwa˙zanie zale˙zno´sci czaso-wych, mimo ˙ze czas nie jest w niej jasno zdefiniowany.
Oprócz filozoficznej problematyki natury czasu, logika temporalna znajduje zastosowanie głównie w informatyce — w temporalnych bazach danych, przy analizie wykonywania programów i ich poprawno´sci. W´sród innych zastosowa ´n mo˙zna wymieni´c lingwistyk˛e (analiza czasów gramatycznych), sztuczn ˛a inteli-gencj˛e (planowanie kolejno´sci akcji, przetwarzanie wiedzy zmiennej w czasie) i fizyk˛e (analizowanie nowych teorii, czas — czwarty wymiar).
Logiki temporalne mo˙zna podzieli´c na dwie grupy — z liniow ˛a oraz rozgał˛e-zion ˛a struktur ˛a czasu. Logiki te mog ˛a traktowa´c czas jako ci ˛agły lub, co jest cz˛e-´sciej spotykane, jako dyskretny. Najprostsz ˛a i zarazem najbardziej rozpowszech-nion ˛a jest LTL (ang. linear temporal logic), u˙zywaj ˛aca dyskretnego i liniowego modelu czasu. Rozszerzeniem LTL na rozgał˛ezione modele czasu s ˛a CTL* oraz CTL, w których dodano dwa dodatkowe operatory wraz z ograniczeniami. W dal-szej cz˛e´sci rozdziału przedstawiono podstawowe własno´sci wspomnianych logik.
11.2. Podstawowe operatory logik temporalnych
11.2.1. Operatory czasu liniowego
Zale˙zno´sci czasowe mo˙zna opisywa´c za pomoc ˛a zwykłego rachunku predy-katów, jednak dowodzenie twierdze ´n w tej notacji jest do´s´c trudne i niezbyt wy-godne. Logika temporalna została stworzona specjalnie z my´sl ˛a o wnioskowaniu
11.2. Podstawowe operatory logik temporalnych z u˙zyciem czasu. Umo˙zliwia bezpo´srednie okre´slanie relacji mi˛edzy zmiennymi wyra˙zaj ˛acymi czas, przez co zapis staje si˛e prostszy i bardziej elegancki.
Zdaniow ˛a logik˛e temporaln ˛a zbudowano z rachunku zda ´n pozbawionego kwantyfikatorów: ∀ — dla ka˙zdego oraz ∃ — istnieje takie. Dozwolone s ˛a dowolne zmienne zdaniowe, wszystkie spójniki, w tym: ¬ — negacja, ∧ — koniunkcja, ∨ — alternatywa, → — implikacja i ↔ – równowa˙zno´s´c. Dodatkowo wprowadzono trzy prefiksowe, unarne (jednoargumentowe) operatory temporalne:
• — zawsze, oznaczany równie˙zG (od ang. globally), • ♦— kiedy´s, tak˙zeF (od ang. finally),
• ° — nast˛epny, X (od ang. next).
Operator uniwersalnynieformalnie znaczy „dla ka˙zdej chwili t w przyszło-´sci”, a zapisp tłumaczy si˛e jako: „od danego momentu ju˙z zawsze b˛edzie za-chodziło p”. Z kolei♦to egzystencjalny operator oznaczaj ˛acy „dla pewnej chwili t w przyszło´sci”, a♦q oznacza, ˙ze kiedy´s w przyszło´sci b˛edzie miało miejsce q. Nale˙zy wspomnie´c, ˙ze operatory te maj ˛a priorytet spójnika logiczego negacji (¬). Przytoczy´c tu równie˙z mo˙zna dwa proste twierdzenia. Pierwsze (11.2.1) — je-´sli p b˛edzie zawsze zachodziło, to p zajdzie w pewnym konkretnym momencie przyszło´sci. Drugie (11.2.2) — dualno´s´c, oznacza, ˙ze p ma miejsce zawsze wtedy i tylko wtedy, kiedy w ˙zadnym momencie w przyszło´sci nie b˛edzie zachodziło ¬p.
Twierdzenie 11.2.1 p →♦p
Twierdzenie 11.2.2 (Dualno´s´c) p ↔ ¬♦¬p
Istotn ˛a własno´sci ˛ai♦jest to, ˙ze mo˙zna je składa´c. Po zło˙zeniu♦p otrzymuje si˛e formuł˛e znacz ˛ac ˛a, ˙ze kiedy´s, od pewnego momentu b˛edzie tak, ˙ze ju˙z zawsze b˛edzie zachodziło p. Składanie ze sob ˛a jednakowych operatorów nie wnosi ni-czego nowego, tzn.♦♦p =♦p, ap =p. Kolejna, bardziej zło˙zona formuła zdaniowa (11.2.3) opisuje nast˛epuj ˛ac ˛a sytuacj˛e: w ka˙zdym momencie przyszło-´sci mamy przed sob ˛a jakie´s wyst ˛apienie p (lewa strona równania), czyli nigdy nie b˛edzie tak, ˙ze ju˙z nigdy nie b˛edzie miało miejsca p (prawa strona równania).
Twierdzenie 11.2.3 p ↔ ¬♦¬p
Trzeci operator unarny nast˛epny (°) mo˙zna zdefiniowa´c w logikach temporal-nych z czasem dyskretnym. Czas taki charakteryzuje si˛e tym, ˙ze jest podzielony na momenty, w których stan ´swiata pozostaje niezmieniony. Przej´scia mi˛edzy stanami s ˛a niesko ´nczenie krótkie. Model ten nadaje si˛e do odwzorowania pracy procesora, gdzie dyskretnym momentom odpowiadaj ˛a takty zegara. W przy-padku kiedy czas jest ci ˛agły mo˙zna zastapi´c go dyskretnym, co wprowadza pewne uproszczenia w obliczeniach.
Zapis °p oznacza, ˙ze p zajdzie w nast˛epnej chwili. Równie˙z ten operator mo˙zna składa´c wielokrotnie z nim samym. Krotno´s´c n jego wyst ˛apie ´n ozna-cza, ˙ze zmienna zdaniowa, któr ˛a poprzedza n operatorów ° nast ˛api za n chwil. Twierdzenia 11.2.4 i 11.2.5 pokazuj ˛a przykładowe zastosowanie ° w formułach
zdaniowych. Pierwsze z nich (11.2.4) tłumaczy si˛e nast˛epuj ˛aco: r b˛edzie kiedy´s fałszywe, a w kolejnej dyskretnej chwili p b˛edzie prawdziwe. Natomiast drugie (11.2.5): zawsze b˛edzie tak, ˙ze je´sli w pewnej chwili zajdzie q, to w nast˛epnej chwili przestanie zachodzi´c.
Twierdzenie 11.2.4 ♦(¬r ∧ °p)
Twierdzenie 11.2.5 (q → °¬q)
11.2.2. Operatory poprzedzania
Poznane operatory nie pozwalaj ˛a na wyra˙zenie, ˙ze p zachodzi przed q. Do tego celu zostały wprowadzone dodatkowe, dwuargumentowe operatory tempo-ralne:
• pU q — (od ang. until) kiedy´s nast ˛api q, ale do tego czasu b˛edzie p, • pW q — (od ang. waiting for) p b˛edzie zachodziło w trakcie czekania na q, • pRq — (od ang. release) q b˛edzie zachodziło tak długo a˙z nie zajdzie p.
11.2.3. Operatory przeszło´sci
Ani operatory modalne ani operatory poprzedzania nie s ˛a w stanie wyrazi´c wymagania, ˙ze pewne zdarzenie musiało nast ˛api´c od czasu wyst ˛apienia innego wydarzenia. Z tego powodu powstały kolejne dwa binarne operatory — operatory przeszło´sci:
• pS q — odk ˛ad (ang. since); wyst ˛apienie q poprzedza wyst˛epowanie p, • pBq — wstecz (ang. back-to); je´sli było q to po nim było p.
Operator B jest słabsz ˛a wersj ˛a S . Na ich podstawie definiuje si˛e operatory unarne przeszło´sci:
• ♦ — kiedy´s (ang. once); operator egzystencjalny, definiowany jako ♦p = t r ueS p,
• — jak dot ˛ad (ang. so-far); uniwersalny, definiowany nast˛epuj ˛aco: p = ¬♦¬p,
• ª — poprzednio; jest to wersja ° dotycz ˛aca przeszło´sci.
Operator ª wymaga krótkiego wyja´snienia. Przy zapisie ªq oznacza, ˙ze zachodzi on w stanie si, je˙zeli q zachodziło w si −1. Przypadkiem szczególnym jest stan s0, dla którego formuła ªq nie mo˙ze by´c spełniona, poniewa˙z stan ten nie ma poprzednika. Dlatego powstała słabsza wersja ª, która odgórnie przyjmuje, ˙ze w s0formuła jest spełniona.
11.2.4. Operatory czasu rozgał˛ezionego
W logice temporalnej czasu rozgał˛ezionego „powracaj ˛a” kwantyfikatory, które ju˙z „po˙zegnano” przy omawianiu operatorów czasu liniowego. Do formalnego zdefiniowania logiki temporalnej z modelem czasu rozgał˛ezionego kwantyfika-tory s ˛a niezb˛edne, gdy˙z wraz ze znanymi doskonale(zawsze) oraz♦(kiedy´s)
11.3. Liniowa logika temporalna