Exercises and Extra Materials

Obs!  The Monday and Wednesday lectures have been cancelled. On Wednesday, the exercises start at 11. 

•  Exercise 1.
• Some solutions of the exercise 1.
• Exercise 2
• Solutions of the exercise 2
• Exercise 3
• Solutions for  the tasks 2-4. Solution for the task 5.
• Exercise 4
• Solutions of the exercise 4
• Exercise 5;  in addition, you can still mark the CADP exercises of Exercise 4.
• Exercise 6.

    CADP software

 In order to use the CADP sofware, follow the following instructions:

1.  Log in to the machine melkki.cs.helsinki.fi with SSH -X command.
2. Write into .profife file in your home directory the commands     (syntax mistake corrected November 27)                                                                                                                                                     

        export CADP=/opt/cadp-2014

        export PATH=$PATH:/opt/cadp-2014/bin.x64:/opt/cadp-2014/com

       alias xeuca = $CADP/com/xeuca

    3. Now you can start the graphical interface of the verification software CADP with command xeuca.

Lotos programs are written in .lotos files. Then choose the option "Generate labelled transition system" with Aldebaran representation. The result appears in .aut file.  

    Lecture slides (basically the same as the lecture notes)

• Chapter 3
• Chapter 4 
• Chapter 5
• Chapter 6
• Chapter 7  Corrected and extended November 20, 2014.
• Chapter 8
• Chapter 9  The slide version of chapter 9 contains more than the lecture version. The extra material, however, is part of the course.
• Appendix to chapter 9 (especially, bisimulation equivalence for Kripke structures)
• Chapter 10
• Summary (i.e. what should you know in the exam)