INFORMATIKAI KAR DOKTORI PROGRAM
SZIGORLATI TEMATIKA

Temporális logikák


Az ítélet alapú lineáris idejû temporális logikák szintaxisa, szemantikája. A klasszikus ítéletkalkulus kiértékelési fogalmának kiterjesztése: a Temporális vagy Kripke-struktúra fogalma. A tautologikusan érvényes formula, az érvényesség, a kielégíthetõség fogalmai és a rájuk vonatkozó összefüggések, tételek. Az ítélet alapú temporális logika bizonyításelméleti tárgyalása. Az axiómarendszer helyessége, teljessége. Az elsõrendû temporális logika szintaxisa, szemantikája.
A temporális logikák alkalmazásai konkurens programokra. Konkurens programok átmenet-gráfjai, multiprogramozott végrehajtásai. Programok invariancia és elevenségi tulajdonságai. Válaszadási képesség. Korrekt viselkedés; a kommunikációs protokoll tulajdonságai. Konkurens programok helyességbizonyításának egy kalkulusa.
A tabló az ítéletalapú temporális logikákban. A tablón alapuló programszintézis lényege, példák.
Az objektumok viselkedésének leírása múlt idejû operátorokkal kiterjesztett temporális logikákkal.
Az intervallum logikák és alkalmazásaik.


Irodalom:

F. Kröger: Temporal Logic of Programs, Springer-Verlag Berlin Heidelberg, 1987.
L. K. Dillon et. al.: A Graphical Interval Logic for Specifying Concurrent Systems, ACM Trans. On Soft. Eng. And Meth. 3 (2) 1994, pp. 131-165.
P.C. Attie, E. A. Emerson: Synthesis of Concurrent Programs with Many Similar Processes, ACM TOPLAS Vol. 20, No. 1, January 1998, pp. 51-115.
Hajdara, Sz. - Kozma, L. - Ugron, B.: Synthesis of a System Composed by Many Similar Objects, Annales Univ. Sci. Budapest., Sect. Comp., 22 (2003) pp.127-150