IA041 Teorie a specifikace procesů

Fakulta informatiky
jaro 2004
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
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.
Předmět je zařazen také v obdobích jaro 2006, jaro 2010, jaro 2012, jaro 2014, jaro 2016, jaro 2018, jaro 2022.