Anketa

Na ovoj stranici trenutno nije odabrana niti jedna anketa!

Repozitorij

Repozitorij je prazan

Matematička logika u računarstvu

Šifra: 61527
ECTS: 5.0
Nositelji: doc. dr. sc. Vedran Čačić - Predavanja
Izvođači: doc. dr. sc. Vedran Čačić - Auditorne vježbe
Engleski jezik:

1,0,0

Nastava se odvija na hrvatskom jeziku u svim svojim elementima, a stranim studentima koji su pridruženi mješovitoj grupi nudi se mogućnost savladavanja predmeta pomoću dodatnih izravnih konzultacija s nastavnikom i asistentima na engleskom jeziku. Pri tome, nastavnik stranog studenta upućuje na odgovarajuću literaturu na engleskom jeziku te mu osigurava mogućnost polaganja predmeta na engleskom jeziku.
Opterećenje:

1. komponenta

Vrsta nastaveUkupno
Predavanja 30
Auditorne vježbe 15
* Opterećenje je izraženo u školskim satima (1 školski sat = 45 minuta)
Opis predmeta:
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.

OBAVEZE STUDENATA TOKOM NASTAVE I NAČINI NJIHOVA IZVRŠAVANJA: Pohađanje predavanja i vježbi, izrada domaćih zadaća, polaganje dva kolokvija.

UVJETI ZA POTPIS: Prisustvo na 70% predavanja i vježbi, predaja rješenja za 70% domaćih zadaća, prolazna ocjena na svim kolokvijima.

NAČIN POLAGANJA ISPITA: Završni dio ispita polaže se u pismenom ili usmenom obliku. Konačna ocjena oblikuje se na osnovi uspjeha u izradi domaćih zadaća, ocjena dobivenih na kolokvijima te ocjene odgovora na završnom dijelu ispita.
Literatura:
  1. M. Ben-Ari: Mathematical Logic for Computer Science
  2. M. Huth, M. Ryan: Logic in Computer Science
  3. E. M. Clarke, O. Grumberg, D. A. Peled: Model-Checking
  4. Z. Manna, A. Pnueli: The Temporal Logic of Reactive and Concurrent Systems
  5. R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi: Reasoning about Knowledge
  6. P. Blackburn, M. de Riejke, Y. de Venema: Modal Logic
  7. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen: Systems and Software Verification
  8. M. Vuković: Matematička logika
3. semestar
Izborni predmet 3, 4, 5, 6 - Redovni Studij - Računarstvo i matematika

4. semestar
Izborni predmet 3, 4, 5, 6 - Redovni Studij - Računarstvo i matematika
Termini konzultacija:

SADRŽAJ

Link na stranicu kolegija: 


Obavijesti