1. What?
2. To Whom?
3. Implementation
4. Requirements
5. Marking
6. Contents

CA = Composition …
EB = External …
Additional slides
The naive banking system
ASSET web page
Intro to ASSET
ASSET exercises

MAT-74006 In Curriculum Book
TCS Studies

MAT-74006 Concurrency Theory

Autumn 2017

Updated 2017-09-22

See below for a suggested marking system

The course begins on Tuesday, 2017-08-29 at 12:15 in classroom SG 312.

date Reading CA Reading EB exercises new topic
2017-10-12 Preparation for ASSET projects
2017-10-11 58, …, 65 These are new problems!
2017-10-10 47, …, 52, 56 Use new version of 52!
2017-10-05 49, …, 51
2017-10-04 22, …, 24 52, …, 57
2017-10-03 21, …, 22 44, …, 48Peterson's algorithm
2017-09-28 26, …, 28 44, …, 48 traces
2017-09-27 22, …, 26 36, …, 40
2017-09-26 29, 30, 32, …, 35 synchronization rules
2017-09-21 15, …, 22 28, …, 31 parallel composition, etc. of state machines
2017-09-20 14, …, 21 21, …, 27parallel composition, etc., of LTSs
2017-09-19 8, …, 1413, …, 15 17, …, 20modelling for ASSET
2017-09-14 16, …, 20 bisimilarity
2017-09-13 A sequence …rest of … 15
2017-09-12 ASSET 10, …, 13(8), 9, …, 15 (exercises)
2017-09-05 4, 5, 7 unfolding
2017-08-31 6, …, 8 7, …, 102, …, 7 state machines
2017-08-30 1, …, 61, …, 7 concurrent systems
2017-08-29 course practicalities, concurrency in programming

1. What?

At an abstract level, the purpose or meaning of a sequential program is clear: it computes a partial function from the inputs to the outputs1. There is, however, no common agreement as to what would be a similar abstract notion for concurrent programs. This course studies the purpose or meaning of concurrent programs, with applications to the checking of their correctness. The material also applies to some extent to hardware.

1. This is not always strictly true because of nondeterministic programming constructs, such as random number generators.

2. To Whom?

The course is intended for students who are interested in theoretical aspects of computer science or information technology. It is also suitable for students of discrete mathematics. Basic notation from set theory and logic will be used. Most of the material does not require deep mathematical skills. Knowledge of finite automata and their languages is useful but not a must.

Strong background in mathematics is not necessary, but willingness to think in abstract terms and learn to use mathematical concepts is necessary.

3. Implementation

The course is on periods 1 ja 2. Every week there are three meetings of two hours each. The meetings are flexibly used for lectures, exercises, and discussion.


Tuesdays 12:15–14:00SG 312first: 2017-08-29
Wednesdays15:15–17:00SG 312
Thursdays 08:15–10:00TB 206last: 2017-12-07

There are no meetings on 2017-09-06, 2017-09-07 (conference), 2017-10-17, 2017-10-18, 2017-10-19 (mid-term break), and 2017-12-06 (public holiday).

If the number of students is small, the course is passed by solving many enough weekly exercise problems. Otherwise there will be an examination.

The main reading material of the course are the following two tutorials:

The exercise problems and other material is distributed via this web page.

The teacher of the course is Antti Valmari.

4. Requirements

The goal is that the course is passed by being present, solving traditional and ASSET problems, and giving talks as follows, so that there is no examination.

The course is worth 7 credit units. Officially, that means 187 hours of student work (including both the meetings and the work done at home). That makes more than 13 hours / week! In my opinion that is too much, but ≈ 10 hours / week seems justified. That means 6 hours for the meetings and ≈ 4 hours homework / week.

There are altogether 39 meetings. Without any special arrangements, the student may be absent from at most 4 meetings and not from more than two successive meetings. Permission to be absent more than this may be negotiated, but then the student has to solve additional problems or give additional talks. The need for this may arise, for instance, if the student has to be absent every Thursday.

Problems and talk topics will be designed as the course goes on. The goal is to find problems and topics that are suitable for students at different levels. Every student must do at least one problem (or group of small problems) or talk each week except the first week. If the student fails a problem or talk, then (s)he may try again another day. It is also possible to change the topic if necessary. An incomplete solution of a medium-level or difficult problem may be accepted as a point at a lower level. The mark of the course is determined by the difficulty of the topics the student chose and the performance in them.

5. Marking

I suggest the following marking system. We should discuss at the meetings whether this is okay. At the time of making the suggestion, approximately ΒΌ of the meetings had taken place. The system has been designed to make it relatively easy to pass the course, while at the same time emphasizing M- and D-points when aiming at a high mark.

To pass the course, the student must do the following:

If the ASSET solution or talk is very weak, the student may have to improve it until it is acceptable.

Points are earned as follows:

Also the ASSET exercise and talk yield points, with the maximum being 30.

mark12 345
points ≥ 150210270 330390

6. Contents

  1. State machines
    • example: a cash dispenser system
    • example: a token ring system
    • definitions of labelled transition systems and state machines
    • labelled transition system as a state machine without variables
  2. Concrete behaviour
    • unfolding of variables
    • the behaviour of a state machine as a labelled transition system
    • equivalence, isomorphism
    • (strong) bisimilarity
  3. Putting state machines together
    • parallel composition, hiding, relational renaming
    • synchronization rules
    • input, output, and interaction
    • about other process-algebraic languages
  4. Linear-time semantics
    • traces
    • congruence requirement
    • deadlocks and stable failures
    • livelocks a.k.a. divergence
    • CFFD-equivalence
    • CFFD-preorder
    • other linear-time semantic models
  5. About branching-time semantics
    • weak bisimilarity
    • branching bisimilarity
  6. Verification
    • properties to be verified
    • equivalence and preorder
    • complexity of linear-time and branching-time verification
    • compositional LTS construction
    • interface specification
    • on-the-fly verification
    • induction
  7. Conclusion