Informace o předmětu

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

St 16. 2. až St 11. 5. St 16:00–17:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 48 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

St 16:00–17:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 19 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 16:00–17:50 B410

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 19 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Čt 16:00–17:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 14:00–15:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 14:00–15:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

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á 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Rozvrh

Út 10:00–11:50 B011

Předpoklady

! I041 Teorie a specifikace procesů && IA006 Automaty

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

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

viz anotace

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející), prof. RNDr. Antonín Kučera, Ph.D. (zástupce)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Mojmír Křetínský, CSc.

Rozvrh

Čt 16:00–17:50 B411

Předpoklady

! I041 Teorie a specifikace procesů && IA006 Automaty

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

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

viz anotace

Další komentáře

Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

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

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 49 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2021 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 48 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2020 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Rozvrh

Po 17. 2. až Pá 15. 5. St 16:00–17:50 B411

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 48 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Studijní materiály
Předmět je vyučován jednou za dva roky.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2019 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 19 mateřských oborů, zobrazit

Cíle předmětu

Student má nastudovat, porozumět, prezentovat a aplikovat metody a nástroje používané při modelování, analýze a verifikaci souběžných procesů.

Výstupy z učení

Na konci tohoto semináře bude student schopen:
rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů.
Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2017 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 19 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2015 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2013 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Dodavatelské pracoviště: Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

Omezení zápisu do předmětu

Předmět je nabízen i studentům mimo mateřské obory.
Předmět si smí zapsat nejvýše 20 stud.
Momentální stav registrace a zápisu: zapsáno: 0/20, pouze zareg.: 0/20, pouze zareg. s předností (mateřské obory): 0/20

Mateřské obory/plány

předmět má 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2011 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty
Znalost problematiky v rozsahu předmětu IA006 - Vybrané kapitoly z teorie automatů, IB107 - Vyčíslitelnost a složitost

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á 18 mateřských oborů, zobrazit

Cíle předmětu

Na konci tohoto semináře bude student schopen rozumět a aplikovat základní techniky používané při modelování, analýze a verifikaci souběžných procesů. Na základě nabytých znalostí je student schopen odvozovat rozhodnutí relevantní v předmětné oblasti.

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Výukové metody

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Počet účastníků je omezen.

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2009 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty

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á 15 mateřských oborů, zobrazit

Cíle předmětu

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

semináře, aktivní účast (presentace a diskuse)

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2008 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Předpoklady

IA006 Automaty

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á 18 mateřských oborů, zobrazit

Cíle předmětu

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

viz anotace

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2007 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: k. Jiná možná ukončení: zk, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky

Předpoklady

! I041 Teorie a specifikace procesů && IA006 Automaty

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

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

viz anotace

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2005 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející), prof. RNDr. Antonín Kučera, Ph.D. (zástupce)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Mojmír Křetínský, CSc.

Předpoklady

! I041 Teorie a specifikace procesů && IA006 Automaty

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

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Metody hodnocení

viz anotace

Informace učitele

http://www.fi.muni.cz/usr/kretinsky/

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

IA041 Teorie a specifikace procesů

Předmět se v období jaro 2003 nevypisuje.

Rozsah

0/2. 2 kr. (plus ukončení). Doporučované ukončení: zk. Jiná možná ukončení: k, z.

Vyučující

prof. RNDr. Mojmír Křetínský, CSc. (přednášející), prof. RNDr. Antonín Kučera, Ph.D. (zástupce)

Garance

prof. RNDr. Mojmír Křetínský, CSc.
Katedra teorie programování – Fakulta informatiky
Kontaktní osoba: prof. RNDr. Mojmír Křetínský, CSc.

Předpoklady

! I041 Teorie a specifikace procesů && IA006 Automaty

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

Jedná se o seminář, kde jako hlavní náplň se předpokládá aktivní účast členů semináře, tj. nastudování a přednesení problematiky (podkapitola z knihy, článek z časopisu, referát z konference atp. -- vesměs psáno v angličtině) zadané po dohodě s vedoucím semináře. Po referátu bude následovat diskuse k problematice. Náplň semináře lze přizpůsobit požadavkům/přáním účastníků při respektování uvedeného rámcového obsahu - viz "Osnova".

Osnova

• Procesy, přechodové systémy s návěštími a jejich (konečná) specifikace. Operační sémantika. Caucalova a Mayrova hierarchie procesů.
• Vybrané sémantické ekvivalence procesů na přechodových systémech, jejich vzájemné vztahy (linear time - branching time spectrum).
• Možnosti algoritmické verifikovatelnosti sémantických ekvivalencí na vybraných třídách nekonečně stavových procesů (equivalence checking) -- nerozhodnutelnost, rozhodnutelnost a složitost.

Literatura

• BAETEN, J.C.M. a W.P. WEIJLAND. Process Algebra. Cambridge: Cambridge University Press, 1990, 248pp. Cambridge Tracts in Theoret.Computer Science. ISBN 0-521-40043-0. info
• Handbook of process algebra. Edited by J. A. Bergstra - A. Ponse - Scott A. Smolka. Amsterdam: Elsevier, 2001, xiv, 1342. ISBN 0444828303. info
• BURKART, Olaf. Automatic verification of sequential infinite-state processes. Berlin: Springer, 1997, 163 s. ISBN 3540639829. info
• Články z časopisů a sborníků konferencí, dle specifikace vyučujícího

Další komentáře

Předmět je vyučován jednou za dva roky.
Výuka probíhá každý týden.

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