<eng>Formal Models for Concurrency</eng> | Faculty of Technical Sciences

Subject: Formal Models for Concurrency (17.0M536)

Type of studies	Title
Master Academic Studies	Mathematics in Engineering (Year: 2, Semester: Winter)
Master Academic Studies	Information Engineering (Year: 1, Semester: Winter)

General information:

Category	Scientific-professional
Scientific or art field	Teorijska i primenjena matematika
ECTS	4

Acquiring knowledge and skills necessary for development of mathematical models for concurrent systems, with the aim of formally proving its properties, verify correctness and detect undesirable behaviors. The aim is that students learn the procedures of proof by induction by structure, by rules and methods for the application of co-induction. Students will gain a detailed insight into one formal calculus for concurrent systems, as a starting point for the study of more complex software systems.

Students are able to develop mathematical models for concurrent systems, formally prove their properties and formaly verify their correct behaviour. Students will have a good knowledge of basic models of concurrency.

Induction (structural, rule induction,...) and coinduction. Calculus for concurrent communicating systems CCS: syntax, reduction semantics, labeled transition systems, examples. Behavioural equivalences, weak and strong bisimulations.

The presentation of the theoretical part during the lectures is followed by the characteristic examples which contribute to better understanding of the subject matter. The students are expected to individually study the additional literature which they discuss with the teacher at the consultation classes.

Authors	Title	Year	Publisher	Language
Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba	Reactive Systems: Modelling, Specification and Verification	2007	Cambridge University Press	English
Sangiorgi, D., Walker, D.	The Pi-Calculus : A Theory of Mobile Processes	2001	Cambridge University Press	English

Course activity	Pre-examination	Obligations	Number of points
Test	Yes	Yes	10.00
Theoretical part of the exam	No	Yes	30.00
Written part of the exam - tasks and theory	No	Yes	40.00
Test	Yes	Yes	10.00
Lecture attendance	Yes	Yes	5.00
Exercise attendance	Yes	Yes	5.00