FI:IA040 Modální a temporální logiky pr - Informace o předmětu
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2004
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
- Vyučující
- prof. RNDr. Luboš Brim, CSc. (přednášející)
- Garance
- prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc. - Rozvrh
- Čt 14:00–15:50 B410
- Předpoklady
- ! I040 Modální a temporální logiky pr
Doporučeno je absolvovat IV010 Komunikace a paralelismus - Omezení zápisu do předmětu
- Předmět je určen pouze studentům mateřských oborů.
- Mateřské obory/plány
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- Informatika (program FI, N-IN)
- Učitelství výpočetní techniky pro střední školy (program FI, M-SS)
- Učitelství výpočetní techniky pro střední školy (program FI, M-TV)
- Učitelství výpočetní techniky pro střední školy (program FI, N-SS)
- Cíle předmětu
- Cílem předmětu je získat základní přehled o temporálních logikách, které jsou používány při verifikaci souběžných systémů. Důraz je v oblasti porovnání jejich vyjadřovací síly a rozhodnutelnosti.
- 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
- Literatura
- GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
- MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
- Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
- Metody hodnocení
- Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
- Informace učitele
- http://www.fimuni.cz/usr/brim/IA040
- Další komentáře
- Předmět je vyučován každoročně.
- Statistika zápisu (podzim 2004, nejnovější)
- Permalink: https://is.muni.cz/predmet/fi/podzim2004/IA040