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

Fakulta informatiky
podzim 2007
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 16:00–17:50 B011
Předpoklady
Doporučeno je absolvovat IV010 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
předmět má 19 mateřských oborů, zobrazit
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.