Předmět Modální a temporální logiky procesů (IA040)
Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu IA040 - Modální a temporální logiky procesů, Fakulta informatiky, Masarykova univerzita (MU).
Top 10 materiálů tohoto předmětu
Materiály tohoto předmětu
| Materiál | Typ | Datum | Počet stažení |
|---|
Další informace
Cíl
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.
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 PELED a Edmund M. CLARKE. Model checking. Cambridge: MIT Press, 1999. xiv, 314 s. ISBN 0-262-03270-8. infoMANNA, Zohar a Amir PNUELI. Temporal verification of reactive systems :safety. New York: Springer, 1995. xviii, 512. ISBN 0-387-94459-1. infoHandbook of logic in computer science. Edited by S. Abramsky - Dov M. Gabbay - T. S. E. Maibaum. Oxford: The Clarendon Press, 1992. 571 s. ISBN 0-19-853761-1. info
Požadavky
Doporučeno je absolvovat IV010 Komunikace a paralelismus
Garant
prof. RNDr. Mojmír Křetínský, CSc.
Vyučující
prof. RNDr. Luboš Brim, CSc.