FI:IA040 Modální a temporální logiky pr - Informace o předmětu

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

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

• Analýza a zpracování obrazu (program FI, N-VIZ)
• Aplikovaná informatika (program FI, N-AP)
• Bezpečnost informačních technologií (angl.) (program FI, N-IN)
• Bezpečnost informačních technologií (program FI, N-IN)
• Bioinformatika a systémová biologie (program FI, N-UIZD)
• Bioinformatika (program FI, N-AP)
• Computer Games Development (program FI, N-VIZ_A)
• Computer Graphics and Visualisation (program FI, N-VIZ_A)
• Computer Networks and Communications (program FI, N-PSKB_A)
• Cybersecurity Management (program FI, N-RSSS_A)
• Formální analýza počítačových systémů (program FI, N-TEI)
• Grafický design (program FI, N-VIZ)
• Graphic Design (program FI, N-VIZ_A)
• Hardware Systems (program FI, N-PSKB_A)
• Hardwarové systémy (program FI, N-PSKB)
• Image Processing and Analysis (program FI, N-VIZ_A)
• Informační bezpečnost (program FI, N-PSKB)
• Informační systémy (program FI, N-IN)
• Informatika (angl.) (program FI, D-IN4)
• Informatika (program FI, D-IN4)
• Informatika (program FI, M-IN)
• Informatika (program FI, N-IN)
• Information Security (program FI, N-PSKB_A)
• Kvantové a jiné neklasické výpočetní modely (program FI, N-TEI)
• Matematická informatika (program FI, B-IN)
• Paralelní a distribuované systémy (program FI, N-IN)
• Počítačová grafika a vizualizace (program FI, N-VIZ)
• Počítačová grafika (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, N-IN)
• Počítačové sítě a komunikace (program FI, N-PSKB)
• Počítačové systémy a technologie (angl.) (program FI, D-IN4)
• Počítačové systémy a technologie (program FI, D-IN4)
• Počítačové systémy (program FI, N-IN)
• Principy programovacích jazyků (program FI, N-TEI)
• Programovatelné technické struktury (angl.) (program FI, N-IN)
• Programovatelné technické struktury (program FI, N-IN)
• Řízení kyberbezpečnosti (program FI, N-RSSS)
• Řízení vývoje služeb (program FI, N-RSSS)
• Řízení vývoje softwarových systémů (program FI, N-RSSS)
• Services Development Management (program FI, N-RSSS_A)
• Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
• Služby - výzkum, řízení a inovace (program FI, N-AP)
• Sociální informatika (program FI, B-AP)
• Software Systems Development Management (program FI, N-RSSS_A)
• Software Systems (program FI, N-PSKB_A)
• Softwarové systémy (program FI, N-PSKB)
• Strojové učení a umělá inteligence (program FI, N-UIZD)
• Teoretická 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) (2)
• Umělá inteligence a zpracování přirozeného jazyka (program FI, N-IN)
• Vývoj počítačových her (program FI, N-VIZ)
• Zpracování a analýza rozsáhlých dat (program FI, N-UIZD)
• Zpracování obrazu (program FI, N-AP)
• Zpracování přirozeného jazyka (program FI, N-UIZD)

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.

• Statistika zápisu (podzim 2020, nejnovější)
  
• Permalink: https://is.muni.cz/predmet/fi/podzim2020/IA040