Introduction to Concurrency and Verification, Winter semester 2007/2008
Lecturer: Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17
(maybe sometimes Prof. C.M. Kirsch)
Schedule: Tuesdays 3pm-5pm, Wednesdays 2pm-3pm
First meeting: Tuesday, 2.10.2007, 2pm, room T06
Language: English
The course may also be taken by PhD students
Course description: The aim of this course is to introduce advanced mathematical models for the formal description and
analysis of programs, with emphasis on parallel, reactive systems. The course consists of 3 hours lectures per
week and lasts for about 15 weeks.
It deals with semantic models for parallel systems, and logics for the description of their properties.
As part of the course material, we will also introduce automatic verification tools, and hint at some of
the implementation techniques underlying them. The teaching consists of lectures interspersed with exercises.
Via this course a practicaly oriented student learns the need of abstraction, formal specification and verification;
the student interested in theory gets a solid introduction to formal methods for specification and verification.
In particular, we will:
model simple systems using transition systems and (CCS) process expressions,
deal with various notions of behaviour equivalences, learn the need of abstraction,
formulate (and verify) properties of systems in Hennessi-Milner logic.
Literature:
- Brand new textbook: Reactive Systems: Modelling, Specification and Verification by
Luca Aceto, Anna Ingolsfdottir,
Kim G. Larsen and Jiri Srba. Cambridge University Press, 2007. Check the publishers web page
here. The book can also be ordered
via Amazon.co.uk . Several copies should be available at the department library in October.
- Scriptum: Introduction to Process Theory, by Kees
Middelburg and Michel Reniers, Technische Universiteit Eindhoven 2004,
available online.
- Additional literature links will also be assembled here as needed, during the semester.
What is this theory good for? A typical question asked by (practically oriented) students. The authors of the
book Reactive Systems have compiled a nice
webpage answering this question. Click on the corresponding link on the left to get to the needed subpage.
Prerequisites: None, the course material is self-contained, as is the textbook and the scriptum.
Knowledge of basics of theoretical computer science like logic for computer science or automata theory is an asset.
Exam: This is a VP course. There will be three exam possibilities in February/March.
The exam is written consisting of several excersises from the material covered during the course (we will do an open-book exam). Additionally,
the homeworks and the
mini project, will also contribute to the final grade.
(mini project = 25%, homeworks = 10%, exam - the rest)
Exam dates: Tuesday, 29.1.2008, during classes, duration 2-3 hours. Thursday, 14.2.2008, 10 am, duration 2-3 hours.
Wednesday, 5.3.2008, 2pm, duration 2-3 hours.
Mini project: The description of the mini project is given in the following pdf file.
Schedule:
- Week 2, Tuesday 9.10.07: Introduction to reactive systems, LTS, CCS informally (for sequential processes).
Book - up to page 10 and Section 2.2.1 (LTS), Scriptum - up to page 22 (Sections 1.1.-1.4.). HW: Exercise 2.3.
Wednesday 10.10.07: CCS informally (continued). Book - up to page 21.
- Week 3, Tuesday 16.10.07: Formal syntax and semantics of CCS.
Book: pages 21-27. Wednesday 17.10.07: More examples. Value passing CCS. Book: pages 27-31.
HW: Exercise 2.13:
Consider the process B defined as
B = push(x).(C(x)^B) + empty.B, C(x) = push(y).(C(y)^C(x)) + -pop-(x).D, D = o(x).C(x) + -e-.B
where -pop-, and -e- denote co-names, and the linking combinator ^ is defined as:
P^Q = P[p'/p,e'/e, o'/o]|Q[p'/push, e'/empty, o'/pop]\{p',e',o'}.
Draw the initial part of the transition graph for this process. What behavior do you think B implements?
- Week 4, Tuesday 23.10.07: Behaviour relations: isomorphism, trace equivalence, strong bisimilarity. Examples.
HW: Exercise 3.2.2.
Wednesday 24.10.07: Strong bisimilarity (continued), examples. Book: pages 31-42, Scriptum: pages 22-40 (Section 1.5).
HW: Exercise 3.3 (book) and Exercise 1.5.5 (Scriptum).
- Week 5, Tuesday 30.10.07: Properties of bisimilarity.
HW: Exercise 3.7. Book: pages 42-50.
Wednesday 31.10.07: No class (Senatstag).
- Week 6, Tuesday 6.11.07: Counters, buffers, meaningful examples. Game characterization of bisimilarity.
HW: Exercise 3.17.3. Book: pages 50 - 53 and 65 - 67. Wednesday 7.11.07: Bisimulation games (examples). Weak bisimulation.
HW: Exercise 3.37 (part of). Book pages 67 - 70 and 53 - 57.
- Week 7, Tuesday 20.11.07: Weak bisimilarity (properties and examples), CWB (example). HW: Exercise 3.26 and Exercise 3.34.
Book: pages 57 - 65. Wednesday 21.11.07: Weak bisimilarity games, decidability and complexity results (overview). Posets.
Book: pages 70 - 76.
- Week 8, Tuesday 27.11.07: Fixed points and bisimilarity. Book: pages 76 - 87. Wednesday 28.11.07: Computing bisimilarity.
Henessy-Milner logic, syntax and semantics. HW: Write an algorithm that computes bisimilarity on a given LTS. What is the worst case complexity of your algorithm?
Book: pages 87 - 91.
- Week 9, Tuesday 4.12.07: Hennessy-Milner logic. Book: pages 91 - 98. Wednesday 5.12.07: Expressivity of Hennessy-Milner logic.
HW: Exercise 5.11. Book: pages 98 - 102.
- Week 10, Tuesday 11.12.07: Hennessy-Milner logic with recursion. Book: pages 102-110. Wednesday 12.12.07: Hennessy-Milner logic with recursion.
HW: Exercise 6.5. Book: pages 110 - 115.
- Week 11, Tuesday 18.12.07: Game characterization for HML with recursion. Mutually recursive equational systems.
HW: Exercise 6.7 and 6.8.3. Book: pages 115-125. Wednesday 19.12.07: Characteristic properties.
Book: pages 125 - 134.
- Week 12, Tuesday 8.1.08: Mixing largest and least fixed points. Modeling and anallysis of mutual exclusion.
Book: pages 134-146. Wednesday 9.1.08: Specifying ME in HML and in CCS.
HW: Using CWB check if Peterson's and Hyman's algorithm ensure ME (as expressed with several HML properties). Book: pages 146 - 151.
- Week 13, Tuesday 15.1.08: Specifying ME in CCS. Testing mutual exclusion. Book: pages 151-159. (End of the material)
Wednesday, 16.1.08: Beyond LTS, CCS, HM Logic (Systems with time, with probabilities, coalgebras, coalgebraic modal logic,
coalgebraic behavioral semantics) - an overview lecture.
- Week 14, Tuesday 22.1.08, 3pm-6pm: Exercises, Questions & Answers.
- Week 15, Tuesday 29.1.08, 3pm-6pm: The first exam.
Results from the exam(s) and homeworks
|
Student ID
|
Exam points (<= 100)
|
HW points (*)(<= 11)
|
Project points (<= 25)
|
Total (mark) (**)
|
Exam date
|
|
****240
|
96
|
9
|
25
|
1
|
29.1.8
|
|
****949
|
93
|
7
|
25
|
1
|
29.1.8
|
|
****744
|
90
|
1
|
20
|
1
|
29.1.8
|
|
****112
|
80
|
11
|
25
|
1
|
29.1.8
|
|
****016
|
75
|
6
|
25
|
1
|
29.1.8
|
|
****173
|
68
|
8
|
25
|
1
|
29.1.8
|
|
****810
|
56
|
6
|
20
|
3
|
29.1.8
|
|
****433
|
-
|
3
|
20
|
5
|
-
|
(*) There were 11 homeworks. Each delivered homework counts as one HW point.
(**) Total = Exam points + HW points + Project points. The final mark is given according to the following rules:
1 (Total >= 100), 2 (85<= Total < 100), 3 (70 <= Total < 85), 4 (60 <= Total < 70), 5 (Total < 60)
Exam problems from 29.1.8