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

Home

Papers

Talks

Teaching

Personal

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:


  1. •Textbook: Reactive Systems: Modelling, Specification, and Verification, by Luca Aceto, Anna Ingolfsdottir,  Kim G. Larsen, and Jiri Srba. Cambridge University Press, 2007.

  2. •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:


  1. •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).

  2. •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.

  3. •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.

  4. •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.

  5. •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).

  6. •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.

  7. •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.

  8. •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.

  9. •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.

  10. •Week 10, Wednesday 28.5.14. Hennessy-Milner logic (continued). Book p. 94-101 with proofs of many auxilliary properties.

  11. •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.

  12. •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).

  13. •Week 13, Wednesday 18.6.2014. No class due to travelling.

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 practically 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 Hennessy-Milner logic.http://cs.uni-salzburg.at/~anas/teaching/ConcurrencyVerification/ProcessTheory.ps

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


Computational Systems Group

Department of Computer Sciences

University of Salzburg

Austria


anas@cs.uni-salzburg.at