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

Fakulta informatiky
podzim 2021
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
Předpoklady
Doporučeno je absolvovat IV010 Komunikace a paralelismus
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 57 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
přednáška, domácí cvičení, samostatné studium
Metody hodnocení
Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
Informace učitele
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020.

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

Fakulta informatiky
podzim 2020
Rozsah
2/0. 2 kr. (plus ukončení). Ukončení: zk.
Vyučující
prof. RNDr. Luboš Brim, CSc. (přednášející)
Garance
prof. RNDr. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky
Rozvrh
Út 10:00–11:50 B411
Předpoklady
Doporučeno je absolvovat IV010 Komunikace a paralelismus
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 57 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
přednáška, domácí cvičení, samostatné studium
Metody hodnocení
Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
Informace učitele
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Předmět je vyučován jednou za dva roky.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 57 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 28 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 28 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 28 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 28 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 27 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 27 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 27 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 27 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 26 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 26 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 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
předmět má 19 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, 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.

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

Fakulta informatiky
podzim 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
předmět má 19 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.
  • 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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, 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.

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

Fakulta informatiky
podzim 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
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.
  • 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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, 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.

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

Fakulta informatiky
podzim 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
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.
  • 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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, 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.

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

Fakulta informatiky
podzim 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
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.
  • 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ě.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, 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.

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

Fakulta informatiky
podzim 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
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ě.
Předmět je zařazen také v obdobích podzim 2002, 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.

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.

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

Fakulta informatiky
podzim 2023

Předmět se v období podzim 2023 nevypisuje.

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
Předpoklady
Doporučeno je absolvovat IV010 Komunikace a paralelismus
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 58 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
přednáška, domácí cvičení, samostatné studium
Metody hodnocení
Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
Informace učitele
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.

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

Fakulta informatiky
podzim 2022

Předmět se v období podzim 2022 nevypisuje.

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
Předpoklady
Doporučeno je absolvovat IV010 Komunikace a paralelismus
Omezení zápisu do předmětu
Předmět je nabízen i studentům mimo mateřské obory.
Mateřské obory/plány
předmět má 58 mateřských oborů, zobrazit
Cíle předmětu
Cílem předmětu je získat základní přehled o modálních a temporálních logikách, které jsou používány při specifikaci, analýze a verifikaci počítačových systémů.
Na konci tohoto kurzu bude student schopen:
porozumět definicím logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů;
porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením;
porozumět výhodám a nevýhodám formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Výstupy z učení
Na konci tohoto kurzu bude student schopen: • pochopit a aplikovat definice logik a logických systémů prezentovaných v kurzu a pochopit hlavní myšlenky důkazů; • porozumět rozdílům mezi jednotlivými logikami, možnostem těchto logik a jejich omezením; • pochopit výhody a nevýhody formální verifikace, speciálně tzv. ověřování modelu, se zaměřením na logiky lieárního a větvícího se času.
Osnova
  • Modální logiky: výroková modální logika, modální mu-kalkulus.
  • Temporální logiky: výroková temporální logika, lineární a větvící se čas, temporální operátory.
  • Klasifikace vlastností procesů: lokální, globální vlastnosti, živost, bezpečnost.
  • Verifikace temporálních vlastností, ověřování modelu (model checking).
  • Automatizovaná verifikace, aplikace
Literatura
  • GRUMBERG, Orna, Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
  • MANNA, Zohar a A. PNUELI. Temporal verification of reactive systems : safety. New York: Springer, 1995, xviii, 512. ISBN 0387944591. info
  • Handbook of logic in computer science. Edited by Samson Abramsky - Dov M. Gabbay - Thomas S. E. Maibaum. Oxford: The Clarendon Press, 1992, 571 s. ISBN 0198537611. info
Výukové metody
přednáška, domácí cvičení, samostatné studium
Metody hodnocení
Zkouška je písemná a ústní. V případě zadání průběžných testů během semestru, mají tyto podíl nejvýše 30% na závěrečném hodnocení. Pomocné materiály nejsou povoleny.
Informace učitele
https://www.fi.muni.cz/usr/brim/home/#teaching
Další komentáře
Studijní materiály
Předmět je vyučován každoročně.
Výuka probíhá každý týden.
Předmět je zařazen také v obdobích podzim 2002, podzim 2003, podzim 2004, podzim 2005, podzim 2006, podzim 2007, podzim 2008, podzim 2009, podzim 2010, podzim 2011, podzim 2012, podzim 2013, podzim 2014, podzim 2015, podzim 2016, podzim 2017, podzim 2018, podzim 2019, podzim 2020, podzim 2021.