A temporális logikák a klasszikus logika [[???Pász 93]] lehetséges kiterjesztései. A temporális logikai nyelvek szemantikájának definiálásakor szükségünk lesz az időpontok halmazáraAz időpont fogalmát absztrakt értelemben használjuk. Nem foglalkozunk az időpontok halmaza felett metrika definiálásával. Az ismertett modell egyelőre nem terjed ki a programok valós idejű végrehejtásának leírására [[???Mel 87]].. Az egyes formulákat egy olyan modell felett értelmezzük amelyben a formulák igazságértéke általában időpontról időpontra változó A temporális logikák a modális logikák körébe tartoznak [[???Rácz 92]]. A klasszikus logikai formula igazságértéke a modális logikák formalizmusa szerint, a logika típusa alapján nemcsak az individumváltozóktól, hanem valamilyen más paramétertől, pl.: helytől, időtől, stb. is függ. Defniálhatnánk pl. olyan modális logikát is, amelyben a paraméter időpillanat helyett időintervallum [[???Mel 87]]. Egy ilyen logika alkalmas lehet valós egyidejűség leírására. A modális paramétertér felett egy elérési reláció definiált. A különböző paraméterértékekhez tartozó univerzumokban egyszerre értelmezzük ugyanazon formulák igazságértékét. A formula igazságértéke egy adott paraméterérték által meghatározott univerzumban általában függ ugyanazon vagy más formulák az elérési reláció felhasználásával meghatározott univerzumokban felvett értékeitől. Az ilyen jellegű összefüggések leírására vezetik be a modális operátorokat, amelyek segítségével a modális paraméter ill. az elérési reláció explicit használata elkerülhető. A modális operátorokat tekinthetjük az egzisztenciális és az univerzális kvantor általánosításának. Az általánosított kvantor jelentése az elérési reláció tulajdonságaitól függ..

A nyelv szemantikájának definiálásakor megadjuk, hogy adott időpontban mely atomi formulák teljesülnek. Az időpontok halmaza felett egy, adott tulajdonságokkal rendelkező relációRelációnak nevezzük halmazok direktszorzatának egy részhalmazát. Bináris relációról beszélünk, ha a reláció pontosan két halmaz direktszorzatának része. definiált [[???Ben 88]]. Időstruktúráról beszélünk, ha az időpillanatok halmaza felett definiált reláció tulajdonságai megfelelnek az időről alkotott alapvető elképzeléseinknek, azaz a relációazaz a modális logika elérési relációja irreflexív és tranzitív. A reláció további tulajdonságai határozzák meg az időstruktúra temporális logikai típusát. Megkülönböztethetünk pl. lineáris ( ), majdnem összefüggő ( ), ill. elágazó idejű modellt, ahol a jövőbe vezető utak diszjunktak. Vannak véges ill. végtelen ( ), diszkrét ( , ill. sűrű struktúrák. Megkövetelhető az idő homogenitása, azaz bármely időpontpárhoz található olyan relációtartó automorfizmus, amely -et -ba viszi. Izotróp egy struktúra, ha izomorf azzal, amelyben a rendezési reláció fordított, azaz amelyben -nek felel meg.

A nyelv szintaxisa szempontjából ugyanúgy, ahogyan a klasszikus logikában, a temporális logika esetén is megkülönböztetjük a 0-ad és magasabbrendű logikai nyelveket. 0-ad rendű esetben a klasszikus logika 0-ad rendű formuláiból és a temporális operátorokból építjük fel a nyelvet. A temporális operátorok használatára vonatkozó szintaktikus szabályok határozzák meg a nyelv temporális logikai típusát. Ennek megfelelően választható ki a nyelvet interpretáló időstruktúra. Az időpillanatok halmaza megadható, mint egy program programállapotainak halmaza.Az elágazó idejű temporális logika formuláinak interpretációjához használt szokásos modellek [[???Eme Sri 88]] és az általunk definiált program ( def.) könnyen megfeleltethető egymásnak. Endogenous az a logika, amelynek időstruktúráját egyetlen program állapotai alapján definiálják, ill. exogenous a logika, ha programkonstrukciók is megengedettek.

Azt mondjuk, hogy egy temporális logikai formulának modellje egy időstruktúra, ha a struktúrában van olyan időpont, amelyben a formula teljesülHa megadjuk, hogy a feladat (. def.) átemenet- és peremfeltételeinek megfelelő temporális logikai formulákat hogyan írjuk fel, akkor a megoldás definícióját visszavezethetjük arra, hogy formulák egy halmazának matematikai logikai értelemben modellje-e a programnak megfelelő temporális logikai struktúra. Haladási feltételek lineáris temporális logikai megfogalmazására mutat példát [[???Lam 91]] a 22.2.3. bekezdésben.. Egy adott probléma megoldása a temporális logika terminológiája szerint a feladatot leíró formulahalmaz egy modelljének megtalálása lehet. Az automatikus programszintézishez modellkereső algoritmusokra van szükség. A szakirodalomban ismertetett eredmények [[???Eme Sri 88]] azt mutatják, hogy ezek az algoritmusok általában nagyon rossz hatékonyságúak, a megoldás előállításához a specifikáció hosszával exponenciálisan arányos időre van szükség. Az előállított megoldás minősége szempontjából az sem közömbös, hogy a formulahalmazt kielégítő modellek melyikét találja meg az algoritmus.

A továbbiakban egy rögzített interpretációban értelmezzük a 0-ad rendű elágazó idejű temporális logika operátorait.Egy rögzített program programállapotai által definiált időstruktúra esetén egy formula az állapottér felett értelmezett logikai függvényt definiál (. fejezet). Az alábbi temporális logikai műveletek segítségével tehát rögzített absztrakt program esetén logikai függvényekből új logikai függvényeket konstruálhatunk.

Az egyes temporális logikák között a leglényegesebb különbség a kifejezőerőben van. Általában minél nagyobb a logika kifejezőereje, annál bonyolultabb a logika eldöntési problémája. A bizonyításelmélet eldöntési problémájának nevezik azt a feladatot, amely úgy szól, hogy egy adott, tetszőleges formula bizonyítható-e. Az eldöntésprobléma megoldását jelenti az automatikus tételbizonyítás algoritmusának megadása. A modellelmélet eldöntésproblémája az a feladat, amely úgy szól, hogy egy adott, tetszőleges formula érvényes-e [[???Pász 93]].