Konkurens programok tulajdonságainak leírására alkalmas eszköz a temporális logika. Temporális logikában 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ó. Számos olyan modellt fogalmaztak meg, amely az összetett temporális logikai eszközkészlet egy alkalmasan megválasztott részétA modell operátorainak jelentése megadható a lineáris temporális logika valamely műveletsorozata segítségével [[???Sin 91]]. alkalmazza folyamatok specifikációjára [[???Cha Mis 89, ???Jär 92]] esetleg folyamatok szemantikájának definiálására is [[???Lam 91]].

Ezek közül a legismertebbek közé tartozik a Lamport által megfogalmazott TLATemporal Logic of Actions. Lamport a programot is és a feladatot is TLA formulával adja meg [[???Lam 91]], így a megoldás fogalma könnyen bevezethető.

A dolgozatban egy másik temporális logika alapú modellre támaszkodunk, a UNITY-ra [[???Cha Mis 89]]. A UNITY biztonságossági és haladási tulajdonságokat kifejező oprátorai megadhatóak lineáris temporális logikai alakban [[???Sin 91]]. Ez a modell alkalmas specifikációk lépésenkénti finomítására. UNITY-ban az absztrakt program struktúrája iteratív. Leggyengébb előfeltétel kalkulusra vezethető vissza annak igazolása, hogy egy program rendelkezik egy adott tulajdonsággal.

A . fejezetben a temporális logikákat részletesen bemutatjuk.