Rozvrh

Čtvrtek
14:00 - 15:50, posluchárna B411

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

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í. Použití literatury a poznámek není při písemce povoleno.

Doporučená literatura

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

Studijní materiály

Učební text. (Materiály jsou dostupné pouze z domény .muni.cz)

Slidy k přednáškám

Slidy jsou dostupné pouze z domény .muni.cz a nesmí být umístěny na veřejně dostupnou doménu!

1. Why we need non-classical logics? (PDF)
2. Formal models of processes (PDF)
3. Propositional modal logic (PDF)
4. Propositional dynamic logic (PDF)
5. Modal algebras (PDF)
6. Decision procedures for PML (PDF)
7. Between modal and temporal logics (PDF)
8. Propositional temporal logics (PDF)
9. Modal mu-calculus (PDF)
10. Completeness of axiom system for PML (PDF)