I040 Modální a temporální logiky procesů

Fakulta informatiky
léto 1996
Rozsah
0/0. 2 kr. Ukončení: z.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Předpoklady
Doporučeno je absolvovat I010 Komunikace a paralelismus
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Logiky pro systémy reálného času.
  • Dokazování vlastností sekvenčních programů (Hoareova logika).
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností: metoda tabel, prověřování modelu (model checking).
Předmět je zařazen také v obdobích léto 1997, léto 1998, jaro 1999, jaro 2000, jaro 2001, jaro 2002.