Theory of concurrency 1000-218bTW
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.
Main fields of studies for MISMaP
Type of course
Mode
Course coordinators
Learning outcomes
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].
Assessment criteria
Oral exam. 3 question randomly generated from the list published 1 month before the exam.
Bibliography
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
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes:
- Bachelor's degree, first cycle programme, Computer Science
- Master's degree, second cycle programme, Computer Science
Additional information (registration calendar, class conductors, localization and schedules of classes), might be available in the USOSweb system: