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.

Important Note: The given times are those at which the lectures will take place. The exercise sessions will precede the lectures, and will start at 12:30. There will be no exercise session before lecture 1, and after lecture 15.

Lecture 1, 3/2/04 at 14:30 (LA): Introduction to CCS;
Mandatory Reading Material: Milner, Chapter 1.
Supplementary Reading Material: Pages 1-15 in An Introduction to Milner's CCS by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen. (Important Note! I know that the figures in the tables are missing. However, you'll find them on the slides, and you should be able to fill in the details yourselves. Eventually, figures will be added.)
Optional Reading Material on the Importance of Verification:
- Formal Methods: State of the Art and Future Directions by Edmund M. Clarke and Jeannette M. Wing.
- System Verification by Joost-Pieter Katoen
Other interesting links:
- Two references of general philosophical interest that argue in a very lucid fashion about the connections that exist between the different strands of Computer Science are:
  - Is Computing an Experimental Science? by Robin Milner. This is the text of the inaugural lecture lecture of the Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh.
  - Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk by Glynn Winskel.
- An article on the Ariane V accident.
- Theory in Practice: Formal Methods for Software and Hardware, slides from a talk by Thomas Henzinger, one of the super-stars in the verification community, and in theoretical computer science as a whole.
Lecture 2, 5/2/04 at 14:30 (LA): More on CCS;
Reading Material: Milner, Chapter 2 (except Section 2.9).
Supplementary Reading Material: Section 4.2 in An Introduction to Milner's CCS by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen.
Lecture 3, 10/2/04 at 14:30: Bisimulation ;

Reading Material:

Milner, Sections 4.1-4.4.;
Pages on the Edinburgh Concurrency Workbench (Version 7.1) (CWB).

Supplementary Reading Material:

An Introduction to Milner's CCS

Lecture 4, 12/2/04 at 14:30: Weak Bisimulation and Observation Equivalence;
Reading Material: Milner, Sections 5.1, 5.3, 5.4, 5.5.
Supplementary Reading Material: Section 5.3 in An Introduction to Milner's CCS by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen.
Lecture 5, 17/2/04 at 14:30 in KS3 4.112 (note the non-standard room!): Hennessy-Milner Logic and its Relationship to Bisimulation Equivalence;
Reading Material:
- Milner 10.1, 10.2;
- Characterization Theorem by K.G. Larsen
Supplementary Reading Material: Section 6 in An Introduction to Milner's CCS by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen. Warning! This section has not been proof read yet.
Lecture 6, 19/2/04 at 14:30: Theory of Fixed-points. Bisimulation as fixed points. Hennessy-Milner Logic with Recursion ;

Reading Material:

A Note on Complete Lattices and Tarski's Fixed-point Theorem

Lecture 7, 24/2/04 at 14:30: Theory of Fixed-points. Hennessy-Milner Logic with Recursion ;

Reading Material:

Hennessy-Milner Logic with Recursion

(Warning! Updated versions of this note will be posted soon! Latest version posted on Tue Mar 4 09:17:51 MET 2003)

Lecture 8, 26/2/04 at 14:30: More on Hennessy-Milner Logic with Recursion; Bisimulation as a Fixed Point
Reading Material: Sections 1-6 in Hennessy-Milner Logic with Recursion by Anna Ingólfsdóttir and Kim G. Larsen
Section 4 of A Note on Complete Lattices and Tarski's Fixed Point Theorem by Luca Aceto, Anna Ingólfsdóttir and Kim G. Larsen. (PDF file with hyperreferences.) [New version posted on Fri Feb 28 11:40:59 MET 2003.]

Lecture 9, 2/3/04 at 14:30: Timed Automata and Uppaal.

Lecture 10, 4/3/04 at 14:30:
1. More on Timed Automata and Uppaal;
2. Introduction to the miniproject .

Lecture 11, 9/3/04, 12:30-16:30: There will be no lecture. You will be working on the mini project for the whole period.

Lecture 12, 11/3/04 at 14:30: A Taste of Behavioural Relations and Logics for Timed Automata.
Lecture 13, 16/3/04 at 14:30: Binary Decision Diagrams and the Compact Representation of Transition Systems.

Lecture 14, 18/3/04 at 14:30: Binary Decision Diagrams (Continued).
Lecture 15, 23/3/04 at 14:30: Binary Decision Diagrams (Completed). Round-up of Course .