Via this course a practicaly oriented student learns the need of abstraction, formal specification and verification; the student interested in theory gets a solid introduction to formal methods for specification and verification. In particular, we will: model simple systems using transition systems and (CCS) process expressions, deal with various notions of behaviour equivalences, learn the need of abstraction, formulate (and verify) properties of systems in Hennessi-Milner logic.

- Brand new textbook:
**Reactive Systems: Modelling, Specification and Verification**by Luca Aceto, Anna Ingolsfdottir, Kim G. Larsen and Jiri Srba. Cambridge University Press, 2007. Check the publishers web page here. The book can also be ordered via Amazon.co.uk . Several copies should be available at the department library in October. - Scriptum:
**Introduction to Process Theory**, by Kees Middelburg and Michel Reniers, Technische Universiteit Eindhoven 2004, available online. - Additional literature links will also be assembled here as needed, during the semester.

- Week 2, Tuesday 9.10.07: Introduction to reactive systems, LTS, CCS informally (for sequential processes). Book - up to page 10 and Section 2.2.1 (LTS), Scriptum - up to page 22 (Sections 1.1.-1.4.). HW: Exercise 2.3. Wednesday 10.10.07: CCS informally (continued). Book - up to page 21.
- Week 3, Tuesday 16.10.07: Formal syntax and semantics of CCS.
Book: pages 21-27. Wednesday 17.10.07: More examples. Value passing CCS. Book: pages 27-31.

HW: Exercise 2.13: Consider the process B defined as

B = push(x).(C(x)^B) + empty.B, C(x) = push(y).(C(y)^C(x)) + -pop-(x).D, D = o(x).C(x) + -e-.B where -pop-, and -e- denote co-names, and the linking combinator ^ is defined as:

P^Q = P[p'/p,e'/e, o'/o]|Q[p'/push, e'/empty, o'/pop]\{p',e',o'}.

Draw the initial part of the transition graph for this process. What behavior do you think B implements? - Week 4, Tuesday 23.10.07: Behaviour relations: isomorphism, trace equivalence, strong bisimilarity. Examples. HW: Exercise 3.2.2. Wednesday 24.10.07: Strong bisimilarity (continued), examples. Book: pages 31-42, Scriptum: pages 22-40 (Section 1.5). HW: Exercise 3.3 (book) and Exercise 1.5.5 (Scriptum).
- Week 5, Tuesday 30.10.07: Properties of bisimilarity. HW: Exercise 3.7. Book: pages 42-50. Wednesday 31.10.07: No class (Senatstag).
- Week 6, Tuesday 6.11.07: Counters, buffers, meaningful examples. Game characterization of bisimilarity. HW: Exercise 3.17.3. Book: pages 50 - 53 and 65 - 67. Wednesday 7.11.07: Bisimulation games (examples). Weak bisimulation. HW: Exercise 3.37 (part of). Book pages 67 - 70 and 53 - 57.
- Week 7, Tuesday 20.11.07: Weak bisimilarity (properties and examples), CWB (example). HW: Exercise 3.26 and Exercise 3.34. Book: pages 57 - 65. Wednesday 21.11.07: Weak bisimilarity games, decidability and complexity results (overview). Posets. Book: pages 70 - 76.
- Week 8, Tuesday 27.11.07: Fixed points and bisimilarity. Book: pages 76 - 87. Wednesday 28.11.07: Computing bisimilarity. Henessy-Milner logic, syntax and semantics. HW: Write an algorithm that computes bisimilarity on a given LTS. What is the worst case complexity of your algorithm? Book: pages 87 - 91.
- Week 9, Tuesday 4.12.07: Hennessy-Milner logic. Book: pages 91 - 98. Wednesday 5.12.07: Expressivity of Hennessy-Milner logic. HW: Exercise 5.11. Book: pages 98 - 102.
- Week 10, Tuesday 11.12.07: Hennessy-Milner logic with recursion. Book: pages 102-110. Wednesday 12.12.07: Hennessy-Milner logic with recursion. HW: Exercise 6.5. Book: pages 110 - 115.
- Week 11, Tuesday 18.12.07: Game characterization for HML with recursion. Mutually recursive equational systems. HW: Exercise 6.7 and 6.8.3. Book: pages 115-125. Wednesday 19.12.07: Characteristic properties. Book: pages 125 - 134.
- Week 12, Tuesday 8.1.08: Mixing largest and least fixed points. Modeling and anallysis of mutual exclusion. Book: pages 134-146. Wednesday 9.1.08: Specifying ME in HML and in CCS. HW: Using CWB check if Peterson's and Hyman's algorithm ensure ME (as expressed with several HML properties). Book: pages 146 - 151.
- Week 13, Tuesday 15.1.08: Specifying ME in CCS. Testing mutual exclusion. Book: pages 151-159. (End of the material) Wednesday, 16.1.08: Beyond LTS, CCS, HM Logic (Systems with time, with probabilities, coalgebras, coalgebraic modal logic, coalgebraic behavioral semantics) - an overview lecture.
- Week 14, Tuesday 22.1.08, 3pm-6pm: Exercises, Questions & Answers.
- Week 15, Tuesday 29.1.08, 3pm-6pm: The first exam.

Student ID | Exam points (<= 100) | HW points (*)(<= 11) | Project points (<= 25) | Total (mark) (**) | Exam date |

****240 | 96 | 9 | 25 | 1 | 29.1.8 |

****949 | 93 | 7 | 25 | 1 | 29.1.8 |

****744 | 90 | 1 | 20 | 1 | 29.1.8 |

****112 | 80 | 11 | 25 | 1 | 29.1.8 |

****016 | 75 | 6 | 25 | 1 | 29.1.8 |

****173 | 68 | 8 | 25 | 1 | 29.1.8 |

****810 | 56 | 6 | 20 | 3 | 29.1.8 |

****433 | - | 3 | 20 | 5 | - |

(*) There were 11 homeworks. Each delivered homework counts as one HW point.

(**) Total = Exam points + HW points + Project points. The final mark is given according to the following rules: 1 (Total >= 100), 2 (85<= Total < 100), 3 (70 <= Total < 85), 4 (60 <= Total < 70), 5 (Total < 60)

Exam problems from 29.1.8