Theory of concurrency

computer science

obligatory courses

Classroom

Development of concurrent systems is difficult which resulted in many mathematical formalism designed for moddeling and considered already from the beginning of computer science. The goal of the current course is to present the most important and most interesting of them, in particular, Petri nets and process algebras.

Much of the focus is devoted to the automatic analysis of concurrent systems models, in particular, its computational complexity. Some of the classes take place in laboratories and are devoted to working with selected tools that enable modeling and analysis of concurrent systems.

Development of concurrent systems is difficult. That is why computer science we consider various mathematical models of concurrent systems. The goal of the lecture is to present the most important of them including Petri Nets, process algebras. The main focus is put on the automatic analysis of modeled systems, in particular on the complexity of the above analysis. Some of the exercises require work with chosen tools for modeling and analysis of computer systems, which allow students to connect theoretical and practical aspects of concurrency.

Outline

I. Introduction

1 Motivations, classification of models, tools.

2 Linear and branching time: temporal properties (LTL, CTL).

II. Petri nets

3. Petri nets: concurrency, conflict, and causality.

4. Theory of Mazurkiewicz traces and its connection with Petri nets, asynchronous automata.

III. Process algebra

5. CCS: concurency and communication; other process algebras.

6. Bisimulation, as an process equivalence relation.

IV. Analysis of concurrent systems

7. Reachability for Petri nets.

8. Bisimulation checking.

Bergstra, J., Ponse, A., Smolka, S., ed. Handbook of Process Algebra, Elsevier, 2001

R. Milner, Communication and Concurrency, Prentice Hall 1995

W. Reisig, Petri nets: an introduction, Springer, 1985

W. Reisig, G. Rozenberg (ed), Lectures on Petri Nets I: Basic Models, Springer 1998

J. Esparza, M. Nielsen, Decidability Issues for Petri Nets - a survey, Bulletin of the EATCS 52:244-262 (1994)

C. Rackoff, The covering and boundedness problems for vector addition systems, Theoretical Computer Science:6(2), 1978

V. Sassone, M. Nielsen, G. Winskel, Models for Concurrency: Towards a Classification, Theoretical Computer Science:170(1–2), 1996

V. Diekert, G. Rozenberg (ed), The Book of Traces, World Scientific 1995

S. Rao Kosaraju, Decidability of Reachability in Vector Addition Systems (Preliminary Version), STOC 1982

J. Leroux, Vector Addition Systems Reachability Problem (A Simpler Solution), Turing-100 2012

Knowledge:

1. A student knows techniques for processes synchronization and communication between processes in centralized and distributed systems [K_W02].

2 A student knows algorithms for mutual exclusion and voting in distributed systems [K_W05].

3 A student knows main formalisms for modeling concurrent systems and their relations.

4 A student has a systematic knowledge on phenomena occurring in concurrent systems.

5. A student understands profits coming from formal modeling of concurrent systems as well as limitations of analysis of formal models.

6. A student knows complexities of main problems in the verification of concurrent systems.

Skills:

1. A student is able to use methods for synchronization of processes and threads in chosen technologies and depending on capabilities and architecture of a given computer [K_U06].

2 A student is able to use modern technologies for distributed computing and parallelization [K_U08].

3 A student knows the domain specific language on the B2 level[K_U14].

4. A student is able to formalize a concurrent system in a chosen modeling formalism.

5. A student is able to describe a chosen aspects of concurrency to non-specialists.

6. A student is able to express simple properties in temporal logic.

Expertise:

1. A student knows the limitations of his knowledge and understands the necessity of further studies [K_K01].

2. A student is able to formulate precise questions to better understand the topic or identify gaps in the reasoning. [K_K02].

3 A student is able to collaborate, including interdisciplinary collaborations; he/she understands a necessity of systematic work on all projects [K_K03].

4. A student is able to formulate his own statements on basic aspects of concurrency [K_K06].

Oral exam. 3 question randomly generated from the list published 1 month before the exam.