Address
Jakob-Haringer-Str. 2
5020 Salzburg, Austria
Room 2.17
Phone
+43 (0)662 8044 6417
+43 (0)662 8044 611 (fax)
Skype ana_sokolova
Address
Jakob-Haringer-Str. 2
5020 Salzburg, Austria
Room 2.17
Phone
+43 (0)662 8044 6417
+43 (0)662 8044 611 (fax)
Skype ana_sokolova
Many thanks to Silviu Craciunas for the photo (RTAS 2010 in Stockholm) and his help with iWeb!
Introduction to Concurrency and Verification, summer semester 2013/2014
Schedule: Wednesdays 9:30am-12noon in T06 see calendar
First meeting: Tuesday, March 11 at 10am in T05 (for once not a Wednesday)
Language: English
The course may also be taken by PhD students
Literature:
•Textbook: Reactive Systems: Modelling, Specification, and Verification, by Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, and Jiri Srba. Cambridge University Press, 2007.
•Lecture notes: Introduction to Process Theory, by Kees Middelburg and Michel Reniers. Technische Universiteit Eindhoven 2004.
The book can be ordered via Amazon.de . Some copies are available at the department library.
Prerequisites: None, the course material is self-contained, as is the textbook. 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 June/July/August. The exam is written consisting of several excersises from the material covered during the course. Additionally, the homework and the mini project will also contribute to the final grade.
Exam dates: discussed in class/via email
Mini projects: discussed in class/via email
Schedule:
•Week 1, Tuesday 11.3.14. Introduction (reactive systems, verification, concurrency). LTS. CCS informally (for sequential processes). Book p.1-9 & Lecture notes p.3-22 (although we did not cover all, it is nice to read).
•Week 2, Wednesday 19.3.14. CCS informally (continued), formal syntax and semantics of CCS, examples. Book p. 9-27. HW: Task 2.11 from the book.
•Week 3, Wednesday 26.3.14. More examples, value-pasing CCS, behavioral equivalences and preorders. Book p. 28-34, scriptum p. 22-25. HW: Task 2.13 from the book.
•Week 4, Wednesday 2.4.14. Behavioral equivalences continued (trace, completed trace, bisimilarity). Book p. 34-42 and 45 (we proved most of the statements given as exercises), scriptum p. 26-40. HW Task 3.5 from the book and Task 1.5.5. from the scriptum. Note that like in the book and unlike in the scriptum we do not consider explicit termination, and use the notation as in the book, but it is still good to read all and you find many additional examples/exercises in the scriptum.
•Week 5, Wednesday 9.4.14. Properties of bisimilarity and comparison to other equivalences. Book p. 42-49. HW: (1) Compare completed trace equivalence and bisimilarity (part of Task 3.11); (2) Find three CCS processes P, Q, and R such that (P+Q) | R is not bisimilar to (P|R) + (Q|R) (part of Task 3.12).
•Week 6, Wednesday 30.4.14. More properties of bisimilarity and meaningful examples (counters and bags), simulations and simulation equivalence, game characterisation of bisimilarity (just started). Book p. 49-53 and 65-66. HW: (1) Exercise 3.17.1. Prove, in addition, that if ≤ is a preorder and ∞ = ≤ ∩ ≤-1 then ∞ is an equivalence. Note that simulation equivalence is defined like this from simulation preorder. (2) Prove that simulation preorder implies trace preorder.
•Week 7, Wednesday 7.5.14. Game characterisation of bisimilarity, fixed points and bisimilarity (started), Tarski’s fixed point theorem. Today’s class was short, we exchanged the last hour for a guest lecture by Hannes Payer. Book p. 66-70 and 75-82. HW: Exercise 3.37.
•Week 8, Wednesday 14.5.14. We shift this class to Tuesday 20.5.14, 9:30am-12noon, as it fits better most of us. More on fixed points, bisimilarity as a fixed point, algorithm for bisimilarity and minimization (wrt bisimilarity), and weak bisimilarity (a bit). Book p. 82-89 and 53-58. HW: The complexity of the bisimilarity algorithm, read about other algorithms and compare.
•Week 9, Wednesday 21.5.14. Weak bisimilarity (continued) and Hennessy-Milner logic (started). Book p.58-65, 70-75 and 89-94. HW: Dijkstra’s dining-philosophers problem, Exercise 3.34.
•Week 10, Wednesday 28.5.14. Hennessy-Milner logic (continued). Book p. 94-101 with proofs of many auxilliary properties.
•Week 11, Wednesday 4.6.14. Hennessy-Milner logic with recursion (started). This was a short class that we continued with a guest lecture of Alfons Laarman. Book p. 102-109. HW: Exercise 5.11 and 6.3 from the book.
•Week 12, Wednesday 11.6.14. Hennessy-Milner logic with recursion, game characterization for HML with recursion. Book p. 109-120. HW: Exercise 6.5 and Exercise 6.7 (it is not obligatory to do the last question, last couple of lines).
•Week 13, Wednesday 18.6.2014. No class due to travelling.
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.
Ana Sokolova
Dr. TU Eindhoven, The Netherlands, 2005
Associate Professor
Department of Computer Sciences
Austria