Courses – Fakultet tehničkih nauka u Novom Sadu

Subject: Formal Models for Concurrency (17.0M536)

Native organizations units: No data

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

General information:

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

Educational goal:

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.

Educational outcome:

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.

Course content:

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.

Teaching methods:

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.

Literature:

Authors	Title	Year	Publisher	Language
Sangiorgi, D., Walker, D.	The Pi-Calculus : A Theory of Mobile Processes	2001	Cambridge University Press	English
Luca Aceto, Anna Ingolfsdottir, Kim G. Larsen, Jiri Srba	Reactive Systems: Modelling, Specification and Verification	2007	Cambridge University Press	English
Janičić, P.	Matematička logika u računarstvu	2009	Matematički fakultet, Beograd	Serbian language

Knowledge evaluation:

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