Administration
Course starts on 4th of April 2000, 1012.
Examination
To receive 4 credit points two batches of exercises have to be solved
and presented at the exercises sessions (see the schedule below).
Exercises
Literature
and course notes
Alternative readings:
Links
Schedule
All meetings are on Tuesdays 1012, in Eliten.

4 April: Introduction [JM] (transparencies)

Motivation: modeling of concurrent communicating systems and automatic
verification of the models. General discussion about the approach. Modelling
language: CCS. What are models. Checking equivalence of models: kinds of
equivalences considered. Properties to be described, specification languages:
mucalculus, CTL. Correctness of a model wrt specification. The verification
system. Picalculus: extending CCS for modeling mobility.

11 April: Reactive sequential processes [JM] (transparencies)

From Finite Automata to Reactive Systems. Why the concept of equivalent
FA is not suitable for comparing reactive systems. (Chapter 2).

Labeled transition systems (LTS). Nondeterministic sequential processes
and strong bisimulation (Chapter3).

18 April: Concurrent communicating systems [JM] (transparencies)

Interacting sequential processes: labels and synchronizations. The process
description language: syntax and semantics. (Chapter 4). A comment on valuepassing
CCS.

Structural equivalence, Strong bisimulation for concurrent processes, Strong
equivalence (Chapter 4, 5).

2 May: Observational equivalence [JM] (transparencies)

What we can observe? Weak bisimulation. Observational equivalence. Examples.
(Chapter 6, 7)

9 May: Model checking with mucalculus [UN] (transparencies)

A general view of model checking. Introduction to mucalculus. mucalculus
and temporal logic. Examples of model checking in CWB. A taste of CTL 
another temporal specification language.

16 May: Student presentations

Homework 1

23 May: Introduction to Picalculus [JM] (transparencies)

Motivation: describing mobility in CCS style (Chapter 8). A survey of Picalculus
(Chapter 9). Selected examples (Chapter 10)

30 May: No lecture

6 June: Student presentations

Homework 2

