Syllabus
1. Mathematical structures for behavior modeling, labeled transition systems, Kripke structures.
2. Equivalence checking.
3. Model checking.
4. Software tools for model checking.
5. Specification and verification of real time systems.
6. Process algebras.
Annotation
Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking techniques and tools.