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

Fakulta informatiky
podzim 2020
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. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 10:00–11:50 B411
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á 57 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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.
  • 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
Výukové metody
přednáška, domácí cvičení, samostatné studium
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
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, 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 2021.