Sylabus
1. Matematické striktury pro modelování chování system, ling, labeled transition systems, Kripkeho struktury.
2. Equivalence checking.
3. Model checking.
4. Softwarové nástroje pro model checking.
5. Specifikace a verifice real-time systémů.
6. Procesové algebry.
Anotace
Základní principy popisu chování paralelních a distribuovaných systémů. Equivalence checking a model checking
- postupy a nástroje. Předmět je vyučován v anglickém jazyce.