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

Fakulta informatiky
podzim 2002
Rozsah
0/2. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: z.
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 15:00–16:50 B411
Předpoklady
! I040 Modální a temporální logiky pr
Doporučeno je absolvovat I010 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
předmět má 6 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.
  • Dokazování vlastností sekvenčních programů (Hoareova logika).
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností: metoda tabel, prověřování modelu (model checking).
Literatura
  • 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
Další komentáře
Předmět je vyučován každoročně.
Předmět je zařazen také v obdobích 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 2020, podzim 2021.