Matematička logika u računarstvu

NAZIV KOLEGIJA: Matematička logika u računarstvu

CILJ KOLEGIJA: Stjecanje uvida u neke aspekte matematičke logike koji neposredno sudjeluju u suvremenoj softverskoj tehnologiji.

NASTAVNI SADRŽAJI:

1.    Dokazivanje u računu sudova i predikata. Rezolucija i dijagrami odluke za račun sudova. Rezolucija za račun predikata. Herbrandov teorem. SLD-rezolucija i logičko programiranje, Prolog. Testovi valjanosti (semantički tabloi).

2.    Temporalna logika i verifikacija modela. Temporalne formule i njihova semantika. Kripkeovi modeli i tranzicijski sustavi. Pravednost, sigurnost i živost u distribuiranim sustavima. Testovi valjanosti za LTL. Izražajnost LTL. Drugi modeli vremena: CTL, CTL*. Algoritmi verifikacije modela za LTL i CTL*. Apstrakcija stanja i simbolička verifikacija modela. Interpretacije u automatima. Verifikacija modela u razvoju softvera – postupci i alati.

3.    Druge modalne logike u računarstvu. Logike akcija i programa, dinamička logika. Hoareove trojke i verifikacija programa. Logike znanja i očekivanja. Zajedničko i opće znanje. Modeliranje i verifikacija pomoću KT45n.

OBAVEZNA LITERATURA:

1.    M. Ben-Ari, Mathematical Logic for Computer Science, Springer Verlag, 2001.

2.    M. Huth, M. Ryan, Logic in Computer Science, Cambridge University Press, 2004.

DOPUNSKA LITERATURA:

1.    E. M. Clarke, O. Grumberg, D. A. Peled, Model-Checking, MIT Press, 2000.

2.    Z. Manna, A. Pnueli, The Temporal Logic of  Reactive and Concurrent  Systems, Springer Verlag, 1991.

3.    R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning about Knowledge, MIT Press, 2003.

4.    P. Blackburn, M. de Riejke, Y. de Venema, Modal Logic, Cambridge University Press, 2002.

5.    B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer Verlag, 2001.

6.    M. Vuković, Matematička logika, Element, 2009.

Go to top