2-INF-126 Modely konkurentných systémov
| Odporúčaný ročník: | 1. |
| Semester: | letný |
| Rozsah: | P3,C1 |
| Hodnotenie: | 20/80 |
| Počet kreditov: | 6 |
| Vyučujúci: | prednáša doc. RNDr. Damas Gruska PhD. |
| www stránka: |
Cieľ:
Prezentovať základné modely paralelných a súbežných procesov. Analyzovať rôzne špecifikačné a verifikačné nástroje a techniky.
Sylabus:
- modely súbežných a paralelných procesov - hlavne procesové algebry (Petriho siete atď.)
- štandardná procesorová algebra, procesorové algebry ako základ špecifikačných (verifikačných) jazykov
- kalkul komunikujúcich systémov (CCS) - základné konštruktory a princípy
- operačná sémantika CCS - značkované prechodové systémy, odvodzovacie pravidlá
- stopová sémantika a bisimulácia - definície, ich vzájomný vzťah
- vlastnosti bisimulácie - kongruentnosť, expanzná veta
- axiomatizácia - systémy axióm charakterizujúcich slabú a silnú bisimuláciu
- charakterizácia bisimulácie pomocou temporálnej logiky - popis logiky, charakterizačné vety
- Pi-kalkulus a jeho zovšeobecnenie - pi-kalkulus ako sémanticky model pre mobile computing, polyadický pi-kalkulus
- Petriho siete - základné definície, vzťah Petriho sietí k procesovým algebrám
- Henessy-Milnerova logika a modálny Mu-kalkulus
Literatúra:
Milner, R.: Communication and Concurrency. Prentice Hall, 1989
Henessy, M. C.: Algebraic Theory of Processes. MIT Press, 1988
Olderog, E. R.: Nets, Terms and Formulas. Cambridge University Press,1991
Stirling, C.: Modal and Temporal Properties of Processes. Springer Verlag, 2002