Course Overview
Disclaimer: The following list of topics
for the course lectures is preliminary and should be taken
with a large pinch of salt. The actual theme of each lecture
may vary, and will only be finalized before the lecture actually takes
place.
The lectures take place each day in room
K6 from 09:00 till 10:45.

Lecture 1, Monday, 27 April 2009:
Introduction to the Course; Labelled Transition Systems;
Introduction to CCS.
 Slides: See this PDF file.
 Reading:
 Sections 1, 2.1 and 2.2.1 in the textbook.
 Optional Reading Material on the
Importance of Verification:
 Other interesting links:
 Lecture 2, Tuesday, 28 April at 09:00: CCS
informally (continued); formal definition of CCS; semantics of CCS;
examples of CCS processes and their semantics.
 Slides: See this PDF file.
 Reading: Section 2.2.2 in the
textbook.
 Lecture 3, Wednesday 29 April 2009: Formal
definition of CCS; semantics of CCS; examples of CCS processes and
their semantics.
 Slides: See this PDF file.
 Reading: Section 2.2.2 in the
textbook.
 Lecture 4, Thursday 30 April 2009:
Strong bisimilarity: Definition and basic properties.
 Slides: See this PDF file.

Reading: Section 2.2.3 in the textbook. (Independent study on
valuepassing CCS. We will not cover this topic in the lecture, but I
encourage you to read this section of the book at your leasure.)
Sections 3.13.3 in the textbook.
 Lectures 58: Weak bisimilarity: Review of the definition
and examples. HennessyMilner logic and its relation to
bisimilarity. HennessyMilner logic with recursion and temporal
properties.
 The slides accompanying the lectures are now available here and here in
PDF format.
 Reading: Sections 3.4 and 3.5, and
Chapters 5 and 6 (up to Section 6.3, included) in the textbook.
 Lectures 9ff: Timed automata: definition, semantics,
region graph and decidability of reachability, timed behavioural
equivalences.
 The slides accompanying the lectures are available here in
PDF format.
 Reading: Chapters 10 and 11 in the textbook.