Temporální logika je široké spektrum formálních systémů, jejichž společným cílem je formalizovat a analyzovat věty obsahující časové (temporální) komponenty jako někdy, vždy či dokud. Kromě původních, spíše lingvistických a filosofických motivací nachází temporální logika od poslední třetiny dvacátého století uplatnění i v informatice a umělé inteligenci.
Úvod Temporální logika má svůj počátek v díle Arthura Priora.Zásadní publikace jsou A.N. Prior. Time and Modality. John Locke lectures. Clarendon Press,1957, a A.N. Prior. Past, Present and Future. Oxford Books. OUP Oxford, 1967. Jak už naznačuje její název, jde o formální vědu zabývající se studiem modelů času. Jejím cílem není odhalit ty charakteristiky, které „skutečně" času náleží, naopak podobně jako jiná odvětví matematické logiky ji lze spíše chápat jako nástroj na popis a zpřehlednění struktur, které si s během času a problémem jeho zachycení lze představit. Oproti běžnému úzu ve studiu modálních logik postupoval historický vývoj jednotlivých temporálních logik od zamýšlených interpretací (modelů, struktur) k formálním systémům, a nikoli naopak.
Z hlediska času jako takového nachází temporální logika uplatnění například ve filosofických diskuzích.Např. M. Perloff N. Belnap and M. Xu. Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press on Demand, 2001.. Už však motivace jejího vzniku byly především lingvistického rázu,Priorovy motivace byly jak lingvistické, tak filosofické. totiž objasnit strukturu temporálních forem přirozeného jazyka, případně nabídnout pro tyto formy adekvátní sémantiku. To se například týká temporálních adverbií nebo slovesných časů. Na konci šedesátých a v sedmdesátých letech dvacátého století se začaly objevovat aplikace některých systémů v oblasti umělé inteligenceViz D. Gabbay, C. Hogger, and J. Robinson, editors. Handbook of logic in artificial intelligence and logic programming (Vol. 4): epistemic and temporal reasoning. Oxford University Press, 1995.. a v informatice.Původní článek je A. Pnueli. The temporal logic of programs. 18th Annual Symposium on Foundations of Computer Science, pages 46–57, 1977. To vedlo k dalšímu rozšiřování již tak velkého množství různých teorií co do šířky (například obohacování syntaxe), hloubky (studium logických vlastností jako úplnost, rozhodnutelnost, definovatelnost, kvantitativní aspekty) a spektra záběru.
Priorova výroková temporální logika TL Výrokovou verzi Minimální temporální logiky lze syntakticky chápat jako rozšíření klasické výrokové logiky KVL o dva unární modální operátory a . Interpretace výroku je „vždy v budoucnosti p”, interpretace je „vždy v minulosti p”. Podobně jako v modální logice s operátorem mají i a svoje duální verze a , „někdy v budoucnosti” a „někdy v minulosti”.V. Goranko and A. Rumberg. Temporal Logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab,Stanford University, Summer 2020 edition, 2020. https://plato.stanford.edu/entries/logic-temporal/.Sekce 3.1. Ze sémantického hlediska lze také chápat jako zjemnění KVL, totiž tak, že hodnota formule se relativizuje vzhledem k časovému okamžiku . Sémantika klasické logiky je v sémantice zahrnuta v tom smyslu, že čistě výrokové formule, které neobsahují temporální operátory, se vyhodnocují lokálně.
Syntax a sémantika Nechť značí jazyk KVL obohacený o operátory a . Jejich duály a jsou definovány následovně:Interpretaci formulí tvoří standardní sémantika modálních logik, kripkovské rámce, které se v temporální logice nazývají časové rámce. Jde o dvojici , z níž je neprázdná množina časových okamžiků a je binární relace, intuitivně značí tvrzení „ následuje po ”.
Pro temporální logiku je tedy zamýšlená interpretace relace ostré (částečné) uspořádání , u minimální logiky se však na žádná omezení nekladou. Ohodnocení proměnných je funkce , tedy každé dvojici se přiřadí hodnota True ci False. Model nad rámcem je trojice pro nějaké .
Formální sémantiku temporálních operátorů tvoří následující dvě klauze (hodnota formule se počítá vůči modelu a vrcholu ):Tvrzení značí, že je splněna v ohodnocením . Definice platnosti v modelu, rámci a třídě rámců je následující: platí v právě tehdy, když je splněna v každém , formule platí v právě tehdy, když platí v každém modelu nad , a formule platí ve třídě rámců právě tehdy, když platí v každém .
Definovatelnost Definice platnosti ve třídě časových rámců umožňuje zkoumat, které třídy rámců jsou „vydělitelné" pomocí některé formule , případně porovnávat expresivitu jazyka prvořádové logiky a jazyka logiky temporální. Temporální formule definuje (charakterizuje) třídu rámců , pokud platí právě v každém rámci ve třídě . Lze se například ptát, zda existují temporální formule charakterizující částečně uspořádané rámce, lineární rámce, hustě uspořádané lineární rámce, diskrétně uspořádané lineární rámce (jednoznačný následník a předchůdce každého bodu), shora neomezené rámce (každý bod má následníka), dobře uspořádané rámce, úplně uspořádané rámce, a další. Existují prvořádové vlastnosti, které nejsou vyjádřitelné temporální formulí. Jako příklady lze vzít antireflexivitu a antisymetrii. Na druhou stranu existují i vlastnosti rámců definovatelné temporální formulí, které nejsou vyjádřitelné jazykem prvořádové logiky. Důležité příklady jsou spojitost a dobré uspořádání.Y. Venema. Temporal logic. In The Blackwell Guide to Philosophical Logic, chapter 10. John Wiley & Sons, Ltd, 2017. Kap. 3.
Standardní překlad, axiomatizace, úplnost Nechť . Minimální logiku lze přeložit do klasické predikátové logiky s rovností. Nechť její jazyk obsahuje jeden binární predikát a spočetně mnoho unárních predikátů Potom lze nadefinovat standardní překlad z jazyka do následovně:Proměnná symbolizuje aktuální stav věcí (přítomnost) a zápis značí substituci proměnné za všechny volné výskyty ve . Tímto způsobem lze každou formuli temporálního jazyka přeložit do prvořádové logiky.V. Goranko and A. Rumberg. Temporal Logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2020 edition, 2020. Sekce 3.3.
Ačkoli je studium temporálních logik primárně motivováno strukturami zamýšlenými k popisu, například přirozenými či racionálními čísly, jako u všech ostatních logik je k dispozici i deduktivní (axiomatická) stránka. Minimální temporální logika má kromě vhodných výrokových axiomů následující dvě temporální obdoby modálního axiomu , dva axiomy stanovující dualitu operátorů a , a nakonec tranzitivitu (a tedy i ):Kromě pravidla modus ponens (MP) se přidají ještě dvě odvozovací pravidla, obdoby necesitace z modálních logik: je silně úplná vůči všem časovým rámcům. Důkaz je standardní jako u běžných modálních logik, konstruuje se tzv. kanonický model jakožto protipříklad na danou dvojici takovou, že . Tuto základní větu o úplnosti lze zesílit na úplnost vůči všem antisymetrickým rámcům.L. Běhounek. Formálnı́ sémantika logiky modalit. In Vojtěch Kolman,editor, Možnost, skutečnost, nutnost. Filosofia, Praha, 2005. Str. 81. Důsledek tohoto zesílení je, že neexistuje temporální formule charakterizující právě antisymetrické rámce.
Rozšíření a varianty
Rozšíření TL na lineárních rámcích Ostré lineární (totální) uspořádání je antireflexivní a tranzitivní relace taková, že každé dva objekty jsou srovnatelné, tj. . Ovšem ani tato vlastnost, ani antireflexivita nejsou vyjádřitelné jazykem . K zachycení žádoucích struktur jako , nebo se využije následující vlastnosti, která je temporálně charakterizovatelná: Binární relace se nevětví do budoucnosti, pokud , relace se nevětví do minulosti, pokud , a se nevětví, pokud se nevětví do budoucnosti ani do minulosti.Podmínka, že se struktura nevětví, například nevylučuje seriální lineární přímky. Výhoda však je, že tuto vlastnost lze temporálně vyjádřit následující formulí: Logika spolu s tímto axiomem se někdy nazývá a tento systém je silně úplný vůči všem lineárním rámcům.D.H.J. de Jongh and F.Veltman. Intensional logics, 1988. Lecture notes. https://staff.fnwi.uva.nl/f.j.m.m.veltman/papers/FVeltman-intlog.pdf. Sekce 5.2.2. Nabízí se také možnost rozšířit ho o další axiomy, které tyto rámce blíže specifikují. Můžeme požadovat, aby tyto struktury byly hustě či diskrétně uspořádané, aby měly či neměly koncové body, nebo například aby byly Dedekindovsky úplné, tedy aby neobsahovaly „mezery”. Všechny tyto varianty lze vyjádřit jazykem a ukazuje se, že dané axiomy věrně popisují zamýšlené interpretace.
Racionální čísla jsou strukturálně spočetné a husté lineární uspořádání bez koncových bodů. Přidáme-li k axiomy charakterizující hustotu a neexistenci nejmenšího a největšího bodu, dostaneme logiku . Tato logika je silně úplná vůči všem hustě uspořádaným lineárním rámcům bez koncových bodů. Poslední požadovaná vlastnost, spočetnost, není vyjádřitelná temporálně ani prvořádově. Avšak ze standardního důkazu věty o úplnosti vyjde spočetný protipříklad, neboť jazyk je také spočetný. A jelikož každé každé spočetné a husté lineární uspořádání bez koncových bodů je izomorfní se strukturou racionálních čísel, logika je silně úplná dokonce vůči této struktuře.Id., sekce 5.3.1.
Reálná čísla jsou husté a úplné uspořádání bez koncových bodů, které navíc obsahuje jako hustě vnořenou podmnožinu. Úplnost uspořádání nelze vyjádřit jazykem prvořádové logiky, ale lze ukázat, že v ji charakterizuje následující formule (kde je zkratka za formuli , intuitivně tedy nutnost jako platnost všude): Logika rozšířena o tento axiom se nazývá a je silně úplná vůči všem hustým a spojitým uspořádáním bez koncových bodů. Toto tvrzení lze opět zesílit do té podoby, že je silně úplná vůči struktuře .Id., sekce 5.3.2.
Diskrétně uspořádaná množina je taková, že každý její prvek (kromě případného maxima a minima) má bezprostředního předchůdce a následníka. Zamýšlená struktura odpovídající spočetnému a diskrétnímu lineárnímu uspořádání bez koncových bodu je , struktura celých čísel. Existenci bezprostředního předchůdce lze vyjádřit formulí , existenci bezprostředního následníka formulí . Logika spolu s těmito dvěma axiomy tvoří logiku diskrétního času , která je silně úplná vůči všem diskrétním lineárním rámcům bez koncových bodů. Avšak toto tvrzení oproti předchozím příkladům nelze zesílit na silnou úplnost vůči jedné konkrétní struktuře reprezentující tuto třídu uspořádání, tedy .Id., sekce 5.3.4.
Varianty temporálních logik Existuje mnoho systémů, jejichž základ tvoří původní Priorova minimální temporální logika, a které ji tak či onak rozšiřují. Jeden přístup, ilustrovaný v následující sekci, je fixovat strukturu, která tvoří zamýšlenou interpretaci daného systému, a rozšířit o další symboly a zvýšit tím jeho expresivitu. Jiná možnost je zobecnit uvažované struktury i na nelineární částečná uspořádání. Další se potom týká zobecnění vůbec základních entit, s nimiž temporální logika pracuje, totiž časových jednotek. Původní motivace těchto tří přístupů, které jsou krátce představeny níže, pocházejí primárně z informatiky a filosofie.
Výroková lineární temporální logika LTL Jedno významné rozšíření Priorovy minimální logiky, které našlo velké uplatnění v informatice, je takzvaná Lineární temporální logika . Hlavní motivace stojící za jejím vznikem je hledání vhodného formalismu pro specifikaci a verifikaci korektnosti (potenciálně nekonečných) reaktivních systémů.Viz E. Allen Emerson. Temporal and modal logic. In Handbook of theoretical computer science, pages 995–1072. Elsevier, 1995. Vzhledem k této aplikaci se jako podkladová struktura uvažuje především dopředu neomezené, diskrétní a reflexivní lineární uspořádání s počátečním stavem. To odpovídá struktuře přirozených čísel, kde je reflexivní totální uspořádání.