Concurrency Theory and Time, 3p

Graduate Course at Mälardalen University with support from ARTES.

April-May 2002

Latest News (important to read)

Password protected page with additional material available here.
Monday April 29: Additional info concerning lecture 2.
Wenesday April 17: Additional info concerning lecture 1.
Monday July 22nd: Assignments graded. Results available here.

General

This course provides an introduction to concurrency theory and timed models,  and will provide a basis for the course Formalisms, Algorithms and Tools in Formal Methods for Real-Time, 3p.
The course can also be taken by those only wanting an introduction to concurrency.

Topics that will be covered include

  • Basic Concurrency Theory
    • Semantics and Transition systems
    • Process Algebra
    • Modal Logics
    • Petri-Nets
    • Modeling
    • Verification, in particular Model Checking
  • Timing extensions
  • Stochastic/Probabilistic extensions
The course is developed and given by Hans Hansson, who can be reached either by mail or phone.

Schedule

There are four meetings, approximately 3h each:
 
When Where What
April 17 1.15pm V222 at Vargens Vret, MdH, Västerås Intro, Models, Transition Systems (slides; also: see news above)
April 29 1.15pm Turing at Vargens Vret, MdH, Västerås Process Algebra, CCS (slides; also: see news above)
May 7 1.15pm Turing at Vargens Vret, MdH, Västerås Modal Logic, Model Checking (slides)
May 15 1.15pm V222 at Vargens Vret, MdH, Västerås Petri-nets, Timed and Stochastic Models (slides)

Course literature

The course will be based on the following articles/books (a few more will be added):
  • [HH94] H. Hansson: Time and Probability in Formal Design of Distributed Systems, ISBN 0 444 89940 5, Elsevier, 1994. 
  • [Milner89] R. Milner: Communication and Concurrency, ISBN 0 13 115007 3, Prentice Hall 1989.
  • [Jonsson02] B. Jonsson: Course Notes for Reactive Systems. The notes are available here.
  • [CES86] Clarke, Emerson, Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications, TOPLAS 8(2).
  • [HJ94] H. Hansson, B. Jonsson: A Logic for reasoning about time and reliability, Formal Aspects of Computing 6:512-535, 1994.
  • [Guidelines] Guidelines for Specification and Verification of Communication Protocols, SICS Perspective Report no. 1, 1991, Available here.
  • [cwb] Article presenting the concurrenct workbench. Available here.
  • [HV87] M.A. Holliday and M.K. Vernon: A generalized timed Petri net model for performance analysis. IEEE Transaction of Software Engineering TSE 13(12), 1987.
  • [Han96] H. Hansson: GTPNA-analysis - an example, 1996. (Available here.)

Recommended reading

  • Intro, Models, Transition Systems:
    • [Guidelines] gives an easy to read introduction. You may want to skip some technical details at the introductory reading.
    • Chapter 1 in [HH94] gives a compact, (hopefully) yet accessible, introductions to most topics covered in this course.
    • Chapter 1 and 2 in [Jonsson02] 
  • Process Algebra, CCS:
    • Chapter 1-6 in [Milner89] will be covered in various details.
    • Chapter 3 (up until 3.2 + 3.8.1) in [HH94] provides a very dense presentation of some of the main aspects covered.
  • Modal Logic, Model Checking:
    • [HH94] sections 1.2-1.3
    • [Jonsson02] Chapter 6 (in file book.pdf)
    • [CES86] concentrate on sections 1-4
    • [Milner] sections 10.1-10.2
    • [Katoen] and [Stirling] selected parts only
  • Petri-nets, Timed and Stochastic Models:
    • [HH94] Read Chapter 1 (again) and browse through Chapter 2. Read chapters 3-5 (possibly skipping some details and special cases)
    • [HJ94] Is essentially a simplified version of the logic and model-checking in [HH94] focusing on probability.
    • [HV87] Provides a presentation of the GTPN-formalism. You don't need to read all details; focus on the initial sections.
    • [Han96] Provides a concrete example of GTPN-analysis. Try to understand the example, and you have learnt enough (for this course;-) about GTPN and GTPNA.

Reference literature

The following is a list of (some) relevant literature that the interested student may want to look at (citations refere to the Bibliography in Hansson's book):
  • Process algebra: [BHR84], [BK84a], 
  • Modal/Temporal logic: [Eme90], [ES88], [CES83], [Pnu77]
  • [Katoen] J-P Katoen: Concepts, Algorithms and Yools for Model Checking
  • [Stirling] Colin Stirling: Model Checking and Other Games
  • Timed modelling: [EMSS92],
  • Stochastic modelling:

Examination

There will be several assignmens, at least one using the cwb and one using the tpwb tools. 

Assignments General

Assignments will be handed out (made available) at end of lectures. Deadline for solutions are two weeks later.
You may discuss assignments with others, but think self! Individual solutions, please.

The Assignments

  1. Intro,  Models, Transition Systems (click here)
  2. Process Algebra, CCS  (click here)
  3. Modal Logic, Model Checking (click here)
  4. Petri-nets, Timed and Stochastic Models (click here)
  5. All assignments

Some useful links

  • [Please mail me suggestions of new links to add to this list.]

    • Tools