IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2021
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučováno prezenčně. - 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 - 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 každoročně.
Výuka probíhá každý týden.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2020
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučováno online. - 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.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2019
- 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
- St 14:00–15:50 B410
- 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2018
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Út 12:00–13: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
- 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 (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2017
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Út 12:00–13: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
- 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 (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2016
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Út 10:00–11:50 B410
- 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
- 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 (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2015
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Čt 12:00–13:50 B410
- 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
- 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 (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2014
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- St 12:00–13:50 B410
- 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fi.muni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2013
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Čt 14:00–15: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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fimuni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2012
- 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.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky - Rozvrh
- Čt 14:00–15: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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fimuni.cz/usr/brim/ia040.html
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2011
- 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 14:00–15:50 G123
- 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- 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)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- seminář, 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
- http://www.fimuni.cz/usr/brim/IA040
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2010
- 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 13:00–14:50 B410
- 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
- Služby - výzkum, řízení a inovace (program FI, N-AP)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- 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
- http://www.fimuni.cz/usr/brim/IA040
- Další komentáře
- Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2009
- 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 10:00–11: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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- 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)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- 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)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- Programovatelné technické struktury (program FI, N-IN)
- Služby - výzkum, řízení a inovace (angl.) (program FI, N-AP)
- Služby - výzkum, řízení a inovace (program FI, N-AP)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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
- 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
- http://www.fimuni.cz/usr/brim/IA040
- Další komentáře
- Studijní materiály
Předmět je vyučován každoročně.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2008
- 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 13:00–14:50 B410
- 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- Informační systémy (program FI, N-IN)
- Informatika (program FI, M-IN)
- Informatika (program FI, N-IN)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- Počítačové systémy (program FI, N-IN)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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. - 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 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
- Aplikovaná informatika (program FI, N-AP)
- Bezpečnost informačních technologií (program FI, N-IN)
- Bioinformatika (program FI, N-AP)
- Informační systémy (program FI, N-IN)
- Informatika (program FI, M-IN)
- Informatika (program FI, N-IN)
- Matematická informatika (program FI, B-IN)
- Paralelní a distribuované systémy (program FI, N-IN)
- Počítačová grafika (program FI, N-IN)
- Počítačové sítě a komunikace (program FI, N-IN)
- Počítačové systémy (program FI, N-IN)
- Programovatelné technické struktury (angl.) (program FI, N-IN)
- 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)
- Zpracování obrazu (program FI, N-AP)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2006
- 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 12:00–13:50 B204
- Předpoklady
- ! I040 Modální a temporální logiky pr
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
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- 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)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2005
- 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 12:00–13:50 B411
- Předpoklady
- ! I040 Modální a temporální logiky pr
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
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- 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)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2004
- 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 14:00–15:50 B410
- Předpoklady
- ! I040 Modální a temporální logiky pr
Doporučeno je absolvovat IV010 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
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- 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)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2003
- 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
- St 10:00–11:50 B411
- Předpoklady
- ! I040 Modální a temporální logiky pr
Doporučeno je absolvovat IV010 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
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- 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, N-SS)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 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
- Aplikovaná informatika (program FI, N-AP)
- Informatika (program FI, M-IN)
- Informatika (program FI, N-IN)
- Učitelství výpočetní techniky pro střední školy (program FI, M-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, N-SS)
- 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ě.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2023
Předmět se v období podzim 2023 nevypisuje.
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučováno prezenčně. - 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 - 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)
- Diskrétní algoritmy a modely (program FI, N-TEI)
- 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 každoročně.
Výuka probíhá každý týden.
IA040 Modální a temporální logiky procesů
Fakulta informatikypodzim 2022
Předmět se v období podzim 2022 nevypisuje.
- Rozsah
- 2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučováno prezenčně. - 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 - 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)
- Diskrétní algoritmy a modely (program FI, N-TEI)
- 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
- Studijní materiály
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
- Statistika zápisu (nejnovější)