Informace o předmětu

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

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.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Út 10:00–11:50 B411

Předpoklady

Doporučeno je absolvovat IV010 Komunikace a paralelismus

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.

Mateřské obory/plány

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.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. Luboš Brim, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Luboš Brim, CSc.
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ě.

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

Rozsah

2/0. 2 kr. (plus ukončení). Ukončení: zk.

Vyučující

prof. RNDr. Luboš Brim, CSc. (přednášející)

Garance

prof. RNDr. 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ů

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ě.

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

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.

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

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.

• Statistika zápisu (nejnovější)