MAT-74006 Concurrency Theory, 7 cr

Additional information

The course is given every second year. The homepage of the course is http://www.cs.tut.fi/~ava/conctheory.html
Suitable for postgraduate studies

Person responsible

Antti Valmari

Lessons

Implementation 1: MAT-74006 2015-01

Study type P1 P2 P3 P4 Summer

Lectures
Excercises
4 h/week
2 h/week
+2 h/week
+4 h/week

Requirements

If the number of students is small, the course is passed by solving many enough weekly exercise problems. Otherwise there will be an examination.
Completion parts must belong to the same implementation

Learning Outcomes

The student can read scientific literature on process algebras. (S)he knows one theory of reactive concurrent systems that supports full abstraction a.k.a. externally observable behaviour and has an idea of how other theories differ.

Content

Content Core content Complementary knowledge Specialist knowledge

1. Modelling systems as co-operating state machines (labelled transition systems) with variables. Process-algebraic languages such as Lotos, CSP and CCS.

2. Bisimulation and bisimilarity. Algorithms for bisimilarity.

3. Unfolding.

4. Trace semantics and CFFD-semantics: equivalence and preorder. Branching bisimilarity, observation equivalence, CSP-semantics. Weakest congruence results. Non-existence results.

5. Verification algorithms and techniques. Computational complexity of verification.

Study material

Type Name Author ISBN URL Additional information Examination material

Other literature Composition and Abstraction Antti Valmari Yes

Other literature External Behaviour of Systems of State Machines with Variables Antti Valmari Yes

Other literature Scientific papers in the field Will be delivered to the students. No

Prerequisites

Course Mandatory/Advisable Description

MAT-02650 Algoritmimatematiikka Mandatory

MAT-71000 Tieto ja laskenta Advisable

TIE-02100 Johdatus ohjelmointiin Mandatory

Correspondence of content

There is no equivalence with any other courses

Last modified 10.02.2015

Study type	P1	P2	P3	P4	Summer
Lectures Excercises	4 h/week 2 h/week	+2 h/week +4 h/week

Content	Core content	Complementary knowledge	Specialist knowledge
1.	Modelling systems as co-operating state machines (labelled transition systems) with variables.	Process-algebraic languages such as Lotos, CSP and CCS.
2.	Bisimulation and bisimilarity.	Algorithms for bisimilarity.
3.	Unfolding.
4.	Trace semantics and CFFD-semantics: equivalence and preorder.	Branching bisimilarity, observation equivalence, CSP-semantics.	Weakest congruence results. Non-existence results.
5.	Verification algorithms and techniques.	Computational complexity of verification.

Type	Name	Author	ISBN	URL	Additional information	Examination material
Other literature	Composition and Abstraction	Antti Valmari				Yes
Other literature	External Behaviour of Systems of State Machines with Variables	Antti Valmari				Yes
Other literature	Scientific papers in the field				Will be delivered to the students.	No

Course	Mandatory/Advisable	Description
MAT-02650 Algoritmimatematiikka	Mandatory
MAT-71000 Tieto ja laskenta	Advisable
TIE-02100 Johdatus ohjelmointiin	Mandatory