1. Home
  2. PROCESS ALGEBRAS

PROCESS ALGEBRAS

Degree course: 
Corso di Second cycle degree in COMPUTER SCIENCE
Academic year when starting the degree: 
2020/2021
Year: 
1
Academic year in which the course will be held: 
2020/2021
Course type: 
Supplementary compulsory subjects
Language: 
English
Credits: 
6
Period: 
First Semester
Standard lectures hours: 
48
Detail of lecture’s hours: 
Lesson (48 hours)
Requirements: 

In order to fruitfully attend the course of Process Algebras the student is required to have familiarity with the basic notions in the realm of formal languages. This requisite is surely respected by students with a 3-years degree in Mathematics or Computer Science

Final Examination: 
Orale

The scope of the exam is to certify that students have all knowledge and ability explained above, by evaluating the knowledge skill and, mainly, the ability to understand and evaluate the novelty in the area proposed in scientific papers.
The exam consists in an oral discussion in a classroom. This is, normally, a 30 minutes discussion requiring, normally, to exposing the content of a scientific paper. The evaluation focuses, in particular, on the ability to understand the results and the ability to understand how these results compare with respect the literature and can be applied in practice.
The knowledge of the technical terminology is implicitly checked, since the questions and specifications of problems use such a terminology.

Assessment: 
Voto Finale

The aim of the course is to allow students to know the theory of process algebras.
In particular, students will learn how this formalism can be employed in the formal modelling of concurrent processes (items 1,2,3,4,5 of section “Contents”), how this instrument provides algebraic laws allowing for process descriptions to be manipulated and analysed (items 9 and 10 of section “Contents”) and how the formalism allows for formal reasoning about equivalences over processes (item 6 of section “Contents”). Some examples will be provided (items 7,8 of section “Contents”) and extensions to the core of the formalism will be introduced (item 11 of section “Contents”).

The course is organised as follows:
Background, aiming to introduce students to the formal modelling of processes.
1. Introduction and Regular Expressions, seen as a preliminary case study (4h)
2. The operational semantics of a simple “while” language (6h)
3. The denotational semantics of a simple “while” language (6h)

The core essence of process algebras, aiming to deeply analyse the formal modelling of concurrent processes.
4. Models for concurrency (6h)
5. Main operators of process calculi (4h)

Equivalences, aiming to present the notion of behaviourally indistinguishable processes.
6. Equivalences between processes (6h)

Case study, aiming to present useful examples
7. ABP protocol (4h)
8. CCS (4h)

Formal reasoning, aiming to present how formals descriptions can be manipulated and analysed
9. Axiomatisations (2h)
10. Modal logic (4h)

Concluding remarks, aiming to describe how the core formalism can be extended
11. Extensions to quantitative aspects, like time and probability (2h)

Due to variety of the arguments, no textbook covering all of them is available.
The slides, in pdf format, are available in the e-learning platform.

Convenzionale

The course is organised in frontal lessons (48 h).
Frontal lessons are dedicated to illustrating the essence and principles of process algebras mentioned in the “Contents” section. In detail, frontal lessons are dedicated to describing the typical usage of process algebras, by illustrating what can be properly specified by using this formalism. Then, properties of these specifications will be discussed as well as the connections between the syntax of specifications and their meaning. The notion of equivalence and the way in which it can support verification will be also illustrated. Students will be required to interact with the teacher, to comment some definitions/results and to challenge the teacher with questions.

The lecturer will meet students upon appointment, proviso a request via e-mail to name.surname@uninsubria.it. The lecturer will answer only to e-mail that are signed and sent from the institutional domain studenti.uninsubria.it. Meeting are also possible via Skype or Teams, for those students that for several reason (e.g. work duties) prefer this kind of interaction.

Professors

TINI SIMONE

Borrowers