Novinky

Konzultační hodiny
St: 9:00 - 10:00

jiný termín jen po domluvě

Cílem předmětu je získat základní dovednosti, které jsou používány pro formální specifikaci a analýzu komunikujících systémů, včetně teoretických základů příslušných formálních nástrojů. Po absolvování kurzu získají studenti schopnost specifikovat a implementovat v jazyce CCS jednoduché komunikační protokoly; analyzovat a formálně ověřovat korektnost návrhu; orientovat se v nejčastějších typech ekvivalencí mezi procesy a jejich omezení.

Osnova

  • Přehled modelů souběžných systémů. Modelování komunikace. Komunikační media, příklady komunikujících systémů, ekvivalence procesů.
  • Jazyk CCS. Synchronizace, akce a přechody, vnitřní akce, sémantika, synchronizační stromy, předávání hodnot, rekurze a indukce.
  • Rovnostní zákony a jejich aplikace. Klasifikace kombinátorů a zákonů, dynamické zákony, expanzní věta, statické zákony.
  • Bisimulace a ekvivalence. Silná bisimulace a její vlastnosti, silná kongruence, bisimulace a její vlastnosti, dokazování správnosti komunikujícího systému.
  • Teorie kongruence vzhledem k~pozorování. Experiment, rovnosti a jejich vlastnosti, řešení rovností, konečné procesy.
  • Pi-kalkul. Modelování mobilních procesů, polyadický Pi-kalkul, příklady aplikací, redukce na lamba-kalkul.

Požadavky na absolvování předmětu

Předmět je zakončen písemnou zkouškou. Použití literatury a poznámek není při písemce povoleno. Znalosti a dovednosti, které je potřeba zvládnout, jsou uvedeny v katalogu předmětů. Za písemku je možné získat 40 bodů, k absolvování předmětu zkouškou stačí zpravidla polovina. Každá písemka je ovšem jinak obtížná, proto nelze uvést generickou hodnotu. U každé písemky je vždy uveden konkrétní počet bodů pro jednotlivá hodnocení.

Doporučená literatura

  • Milner, Robin. Communication and concurrency. Prentice Hall, 1989.
  • Milner, Robin. Communicating and mobile systems : the Pi calculus. Cambridge University Press, 1999.
  • L. Aceto, A. Ingolfsdottir, K. G. Larsen, J. Srba. Reactive Systems: Modelling, Specification and Verification.. Cambridge University Press, 2007.
  • Učební text k přednáškám. (Materiály jsou dostupné pouze z domény .muni.cz)

Slidy k přednáškám

  1. Úvod (PDF)
  2. CCS na příkladech (PDF)
  3. CCS - syntaxe a sémantika (PDF)
  4. Silná bisimulace (PDF)
  5. Slabá bisimulace (PDF)
  6. Další příklady (PDF)
  7. Bisimulační kongruence (PDF)
  8. Rozšíření jazyka CCS (PDF)
  9. CWB (PDF)
  10. Temporální vlastnosti procesů (PDF)