1. What?

2. To Whom?

3. Implementation

4. Requirements

5. Marking

6. Contents

Points

CA = Composition …

EB = External …

Exercises

Additional slides

The naive banking system

ASSET web page

Intro to ASSET

ASSET exercises

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-12-07 | ||||
---|---|---|---|---|

2017-12-05 | RL OSc CL | |||

2017-11-30 | JH MT HT | |||

2017-11-29 | AK MK TS | |||

2017-11-28 | OSa LS MS | |||

2017-11-23 | 113, …, 116 | |||

2017-11-22 | 110, 111, 112, 106, 107, 108 | |||

2017-11-21 | 96, 98, 99, 102, 103, 105 | branching bisimilarity | ||

2017-11-16 | 103, …, 108 | branching bisimilarity | ||

2017-11-15 | 97, …, 102 | operational determinism | ||

2017-11-14 | 37, …, 39 | observation equivalence | ||

2017-11-09 | 90, 96 | observation equivalence | ||

2017-11-08 | 34, …, 37 | 85, 86, (87, 88, 89), 92, 94, 95 | CFFD-preorder | |

2017-11-07 | 29 | (79), 80, …, 84, 91, 93 | ||

2017-11-02 | 80, …, 84 | CFFD-preorder | ||

2017-11-01 | 25, …, 28 | 31, …, 34 | (62), (64), 76, …, 79 | congruence, CFFD-equivalence |

2017-10-31 | (62), (64), 69, 71, …, 75 | 62, 64 if there is time | ||

2017-10-26 | 25 | 28, …, 31 | 66, …, 71 | stable failures |

2017-10-25 | 24 | 27, …, 28 | 51, 62, …, 65 | traces |

2017-10-24 | ASSET again, intro to traces | |||

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, …, 48 | Peterson'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, …, 27 | parallel composition, etc., of LTSs | |

2017-09-19 | 8, …, 14 | 13, …, 15 | 17, …, 20 | modelling 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, …, 10 | 2, …, 7 | state machines |

2017-08-30 | 1, …, 6 | 1, …, 7 | concurrent systems | |

2017-08-29 | course practicalities, concurrency in programming |

At an abstract level, the purpose or meaning of a sequential program is clear:
it computes a partial function from the inputs to the outputs^{1}.
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.

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.

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.

**Meetings:**

Tuesdays | 12:15–14:00 | SG 312 | first: 2017-08-29 |

Wednesdays | 15:15–17:00 | SG 312 | |

Thursdays | 08:15–10:00 | TB 206 | last: 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.

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.

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:**

- Solve a medium-size or bigger ASSET exercise.
- Give one 30-minute talk on some scientific paper given by the teacher.
- Earn enough points.

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:**

- presence: 1 point
- E-solution: 3 points
- M-solution: 10 points
- D-solution: 30 points

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

mark | 1 | 2 | 3 | 4 | 5 |
---|---|---|---|---|---|

points ≥ | 150 | 210 | 270 | 330 | 390 |

- 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

- Concrete behaviour
- unfolding of variables
- the behaviour of a state machine as a labelled transition system
- equivalence, isomorphism
- (strong) bisimilarity

- Putting state machines together
- parallel composition, hiding, relational renaming
- synchronization rules
- input, output, and interaction
- about other process-algebraic languages

- Linear-time semantics
- traces
- congruence requirement
- deadlocks and stable failures
- livelocks a.k.a. divergence
- CFFD-equivalence
- CFFD-preorder
- other linear-time semantic models

- About branching-time semantics
- weak bisimilarity
- branching bisimilarity

- 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

- Conclusion