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).


Literature and course notes Alternative readings: Links Schedule
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 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 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 
Homework 1 
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 
Homework 2