Here I will keep a brief record of the topics discussed in each lecture, as
the course proceeds.

For reference below you can see how the course went the last time I gave it,
in Autumn 2008.

- Week 18: January 18th
Lecture 1 : Admin. Gave introduction to the course

Lecture 2: Thurs 15.00 - 17.00. Labelled transition systems.
Communicating processes. An informal introduction. Chapter 2 of textbook.

- Week 2: January 25:
Lecture 1 : Wed 16.00 - 17.00 The language CCS: an informal introduction.
Chapter 2 of textbook.

Tutorial: Thurs 15.00 - 16.00. Worksheet 1, defining labelled Transition systems from English descriptions.
We did not get to consider Question 4.

Lecture 2: Thurs 16.00 - 17.00. The semantics of CCS processes. Using the rules in Table 2.2
of the textbook.

- Week 3: February 1:
Lecture 1 : Wed 16.00 - 17.00: An example of how to generate an LTS from a CCS description.

Tutorial: Thurs 15.00 - 16.00. Worksheet 2. CCs formally. Generating LTSs from CCS descriptions using the
formal semantics.

Lecture 2: Thurs 16.00 - 17.00. More on CCS descriptions and LTSs. Specifications versus
implementations. Intrduction to behavioural equivalences.

- Week 4: February 8:
Lecture 1 : Wed 16.00 - 17.00: Behavioural equivalences. Beginning Chapter three of textbook.
Trace equivalence. Strong bisimulation equivalence

Lecture 2: Thurs 15.00 - 16.00. Value-passing CCS. Section 2.2.3 of textbook.

Tutorial: Thurs 16.00 - 17.00. Worksheet 3.

- Week 5: February 15:
Lecture 1 : Wed 16.00 - 17.00: Using games to characterise strong bisimulation equivalence

Tutorial: Thurs 15.00 - 16.00. How to use the CWB

Lecture 2: Thurs 16.00 - 17.00. Milners workshop

- Week 6: February 22:
Lecture 1 : Wed 16.00 - 17.00: Weak bisimulation equivalence

Tutorial: Thurs 15.00 - 16.00. Deciding strong bisimulation equivalence using games

Lecture 2: Thurs 16.00 - 17.00. Understanding weak bisimulation equivalence.

- Week 7: March 1:
Study week. No lectures.

- Week 8: March 8:
Lecture 1 : Wed 16.00 - 17.00: Hennessy-Milner Logic. Sections 5.1 and 5.2 of textbook.

Tutorial: Thurs 15.00 - 16.00. Deciding weak bisimulation equivalence using games. Worksheet 4

Lecture 2: Thurs 16.00 - 17.00. Weak Hennessy-Milner Logic and its relation with weak
bisimulation equivalence.

- Week 9: March 15:
Lecture 1 : Wed 16.00 - 17.00: St patricks Day. No lecture.

Lecture 2: Thurs 15.00 - 16.00. Cancelled

Tutorial: Thurs 16.00 - 17.00. Cancelled

- Week 10: March 22:
Lecture 1 : Wed 16.00 - 17.00: No students

Lecture : Thurs 15.00 - 17.00. The alternating bit protocol (Vasileios Koutavas)

- Week 11: March 29:
Lecture 1 : Wed 16.00 - 17.00:

Tutorial: Thurs 15.00 - 16.00.

Lecture 2: Thurs 15.00 - 17.00.

- Week 12: April 05:
Lecture 1 : Wed 16.00 - 17.00.

Lecture 2: Thurs 15.00 - 17.00. Recursive HML formulae (Edsko deVries)

- Extra: April 21st: Two hour revision (Edsko DeVries)

Reactive Systems course Autumn 2008:

- Week 1: October 6th:
Tutorial 1 : (Monday) No show

Lecture 1: (Thursday) Labelled Transition Systems.
How to use them to descibe reactive systems

- Week 2: October 13th:
Tutorial 2: (Monday) We did first half of worksheet1.

Lecture 2: (Thursday) The language CCS

Covered the syntax and semantics of CCS.
Including the use of the SOS rules in Table 2.2 of the textbook
for defining the actions of a process.

All material taken from Section 2.1 and Section 2.2 of the textbook.

- Week 3: October 20th:
Tutorial 2: (Monday) : Working through worksheet2.

Lecture 3: (Thursday) Translating CCS expressions into LTSs; some examples

Behavioural equivalences: Sections 3.1 and 3.2 of textbook.

Trace equivalence.

Why trace equivalence is not adequate.

- Week 4: October 27th:
Tutorial: (Monday) Bank holiday

Lecture 4: (Thursday) We went through worksheet on how to use the CWB.

Then talked about strong bisimulations, and strong bisimulation
equivalence. Section 3.3 of textbook.

- Week 5: November 3rd:
Tutorial: (Monday) Worksheet 3

Lecture 5: (Thursday)
Value-passing CCS, Section 2.2.3 of
textbook

How to show processes are not equivalent
using games, Section 3.5 of textbook,

Weak bisimulations, Section 3.4 of
textbook.

- Week 6: November 10th:
Tutorial: (Monday) Finished worksheet3, started worksheet4

Lecture 6: (Thursday)

Finished Topic 4. Including properties of weak bisimulation equivalence.

Discussed the example protocol in Table 3.1 of textbook.

Started Topic 5.

- Week 7: November 17th:
Tutorial: (Monday) 15.00 - 16.00

More on Worksheet4.

Lecture 7: (Thursday) 16.00 - 18.00

Hennessy-Milner logic. Sections 5.1 and 5.2 of textbook.

- Week 8: November 24th:
Tutorial: (Monday) 14.00 - 15.0. Some questions
from Worksheet5

Lecture 8.1: (Monday) 15.00 - 16.00. Tarkski's fixpoint theorem. An overview of Sections 4.1 and 4.2 of textbook.

Lecture 8.2 : (Thursday) 16.00 - 18.00: The alternating bit protocol.

Modal formulae with maximal and minimal fixpoints. Sections 6.1 and 6.2 of textbook.

- Week 9: December 1st:
Tutorial: (Monday) 14.00 - 16.00: Worksheet6. Questions 1 to 4 were tackled.

Discussion of how to formulate interesting properties such as deadlock, livelock,
and eventually.

# ** THE END **