FI:I040 Modální a temporální logiky pr - Informace o předmětu

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

Rozsah

0/2. 2 kr. Doporučované ukončení: k. Jiná možná 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

• Informatika (program FI, B-IN)
• Informatika (program FI, M-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, M-IN)
• Učitelství výpočetní techniky pro střední školy (program FI, M-SS)
• Výpočetní technika (program FI, B-IN)

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).

• Statistika zápisu (léto 1997, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/leto1997/I040