Course starts on 4th of April 2000, 10-12.

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

• How to run CWB-NC 
• Exercises
• Batch 1
• Batch 2 (source to alternating bit protocol)
  Paper on Strategic directions in concurrency

• R. Milner. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, May 1999. 
• R. Cleaveland and S. Sims. The Concurrency Workbench of North Carolina: User's Manual, version 1.11, 1998. 
• Additional articles
• Colin Stirling. An introduction to modal and temporal logics for CCS. LNCS 491, Springer-Verlag, 1991.

• R. Milner. Communication and Concurrency. Prentice Hall, 1989/1995. 
• R. Milner. The Polyadic pi-Calculus: A Tutorial. 
• R. Milner, J. Parrow, and D. Walker. A Calculus for Mobile Processes. Information and Computation 100(1) pp.1-40, Sept 1992. 

• Virtual library of Concurrent Systems 
• Virtual library of Formal Methods 
• Concurrency Workbench of the New Century 
• Calculi for Mobile Processes 
• The Edinburgh Concurrency Workbench (a companion to CWB-NC) 
• Protocols for WAN, LAN, ATM 
• Course page: Theory of Distributed Systems at KTH. 
• Formal Methods Education Resources 

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