HTML-4.0 Checked! Last modified: Wed Feb 6 12:39:59 MET 2002

Ecole Polytechnique Fédérale de Lausanne (EPFL)
School of Computer and Communication Sciences (IC)
Institute of Core Computing Science (IIF)
Programming Methods Laboratory (LAMP)
Prof. Uwe Nestmann (UN)
Ecole Polytechnique Federale de Lausanne

Theorie des systèmes mobiles et communicants

winter 01/02

Wednesdays, 14:15-17:00, INM 203

Objectives

The student will learn how to use calculi for communicating processes - in particular name-passing process calculi, which are suitable for mobile systems - in order to formally describe and reason about reactive systems. As particular applications, we look at aspects of communication protocols that underly mobile phone networks as well as security protocols. Much information on this (lively research) subject can be found through http://move.to/mobility. Note that this course is not about the fundamentals of GSM networks etc.

Feedback

Participants are encouraged to provide feedback either by email, if the problem/question/criticism is meant to be kept private, or through a message on the newsgroup for this course, if it is of public interest.

Course Material

In the following, we refer to Milner, Robin: "communicating and mobile systems: the pi-calculus", 1999, Cambridge University Press [Milner 99] as the book.
When referring to Sect. n, I mean Section n of the book.

Accompanying the lectures, I will provide access to the course slides in various formats:

  • .pdf for convenient online browsing,
  • 2on1.ps with space for your own notes (recommended!),
  • 4on1.ps filling up the whole page.

They should usually appear before 13:00 on the day of the lecture (at the latest).
I usually also change the downloadable files after the sessions, in particular the .pdf version.
Check out the time-stamps (mentioned in the title or footer)!

Course Protocol

1 - October 24, 2001: Initiation ( 4on1 )
  • presentation of the course objectives and layout

2 - October 31, 2001: Models for Concurrent Behaviors ( pdf , 2on1 , 4on1 )
  • from automata to labeled transition systemes
    from language equivalence to strong simulation (Sect 2-3.2)

3 - November 07, 2001: Equivalence Notions ( pdf , 2on1 , 4on1 )
  • repetition
  • mutual simulation (not in the book)
  • bisimulation (Sect 3.3)

4 - November 14, 2001: Sequential Process Expressions ( pdf , 2on1 , 4on1 )
  • repetition
  • isomorphism (not in the book)
  • inductive syntax & structural congruence (Sect 3.4, but not exactly as in the book)

5 - November 21, 2001: Concurrent Process Expressions ( pdf , 2on1 , 4on1 )
  • LTSs & examples (Sect 3.5-7)
  • composition & products, reactions (Sect 4.1-2, but not as in the book)
  • inductive syntax, bound names, alpha-conversion, substitution (Sect 4.3)

6 - November 28, 2001: Congruence & Reaction ( pdf , 2on1 , 4on1 )
  • structural congruence, normal forms
  • linking structures (Sect 4.4)
  • reaction (Sect 4.5)

7 - December 05, 2001: Transitions and Strong Equivalence ( pdf , 2on1 , 4on1 )
  • several inductive proof techniques
  • transition rules (Sect 5.1)
  • properties of process expressions w.r.t. bisimulation (Sect 5.3-4)

8 - December 12, 2001: Observation Equivalence ( pdf , 2on1 , 4on1 )
  • strong bisimulation up to (Sect 5.2)
  • weak bisimulation (Sect 6.1-2)
  • unique solution of equations (Sect 6.3)

9 - December 19, 2001: Examples ( no slides today : student presentations )
  • scheduler (Sect 7.3)
  • buffer (Sect 7.4)

December 26, 2001
January 02, 2002

10 - January 09, 2002: Towards Mobility & Pi Calculus ( pdf , 2on1 , 4on1 )
  • unbounded structures: stacks (Sect 7.5)
  • Turing-power (not in the book)
  • mobility through name-passing (Sect 8.2, but not exactly as in the book)

11 - January 16, 2002: Basics of Mobile Processes ( pdf , 2on1 , 4on1 )
  • elastic structures (Sect 8.3, but not exactly as in the book)
  • syntax (Sect 9.1)
  • contexts, congruence, reaction semantics (Sect 9.2)
  • structure, scoping & mobility (Sect 9.3)
  • recursion vs replication (Sect 9.5)

12 - January 23, 2002: Reasoning about Mobile Processes ( pdf , 2on1 , 4on1 )
  • polyadism (Sect 9.4)
  • abstractions & concretions (Sect 9.6, 12.1)
  • commitment (Sect 12.2)
  • strong bisimulation (Sect 12.3)

13 - January 30, 2002: Applications & Mechanized Proofs ( pdf , 2on1 , 4on1 )

14 - February 06, 2002: Applications & Mechanized Proofs (II) ( pdf , 2on1 , 4on1 )

EXAM - February 19, 2002