Rozvrh
Úterý,
12:00 - 13:50, posluchárna
B411
Výuka
Předmět je veden formou výuky, která
kombinuje přednášky a samostudium. Přednáška v trvání
jedné vyučovací hodiny
je úvodem do daného tématu (viz níže). Druhá hodina je věnována
samostatné práci studentů s textem
s cílem seznámit se s tématem podrobně.
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
Znalosti a dovednosti, které je potřeba zvládnout, jsou uvedeny v katalogu
předmětů. 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. Každá písemka je
jinak obtížná, proto nelze uvést
generickou hodnotu pro absolvování
předmětu či postup k ústní části. Ústní část zkoušky není bodována.
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 - témata
Slidy jsou dostupné pouze z domény
.muni.cz a nesmí být umístěny na veřejně dostupnou doménu!
- Why we need non-classical logics? (PDF)
- Formal models of processes (PDF)
- Propositional modal logic (PDF)
- Propositional dynamic logic (PDF)
- Modal algebras (PDF)
- Decision procedures for PML (PDF)
- Between modal and temporal logics (PDF)
- Propositional temporal logics (PDF)
- Modal mu-calculus (PDF)
- Completeness of axiom system for PML (PDF)