Course starts on 4th of April 2000, 10-12.
To receive 4 credit points two batches of exercises have to be solved
and presented at the exercises sessions (see the schedule below).
and course notes
All meetings are on Tuesdays 10-12, 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:
mu-calculus, CTL. Correctness of a model wrt specification. The verification
system. Pi-calculus: 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 value-passing
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 mu-calculus [UN] (transparencies)
A general view of model checking. Introduction to mu-calculus. mu-calculus
and temporal logic. Examples of model checking in CWB. A taste of CTL --
another temporal specification language.
16 May: Student presentations
23 May: Introduction to Pi-calculus [JM] (transparencies)
Motivation: describing mobility in CCS style (Chapter 8). A survey of Pi-calculus
(Chapter 9). Selected examples (Chapter 10)
30 May: No lecture
6 June: Student presentations