IA040 Modální a temporální logiky procesů
Aktuální informace:
Přednáška se dne 15.10. nekoná!
Sylabus:
- 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.
- Klasifikace vlastností procesů: lokální, globální vlastnosti, živost,
bezpečnost.
- Verifikace temporálních vlastností, ověřování modelu (model checking).
- Automatizovaná verifikace, aplikace
Rozvrh:
Čtvrtek, 10:00 - 11.50, B011
Požadavky na absolvování
předmětu: Předmět je zakončen zkouškou, která je tvořena písemnou
a ústní částí.
Literatura a studijní materiály:
- Handbook of logic in computer science. Vol. 2, Background : computational
structures. Edited by S. Abramsky - Dov M. Gabbay - T. S. E. Maibaum. Oxford :
Clarendon Press, 1992.
- Clarke, Edmund M. - Grumberg, Orna - Peled, Doron. Model
checking. Cambridge : MIT Press, 1999.
- Manna, Zohar - Pnueli, Amir. Temporal verification of reactive systems : safety. New York : Springer, 1995
- Poznámky k přednášce
Konzultační hodiny:
Pondělí od 9:00 do 10:00
Čtvrtek od 9:00 do 10:00