Tarcali, Barnabás (2024) The Leader Election Problem in a Typed Pi-calculus. Bachelor's Thesis, Computing Science.
|
Text
bCS2024TarcaliB.pdf Download (425kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming_ Barnabás Tarcali _ degree programme_ Computing Science.pdf Restricted to Registered users only Download (137kB) |
Abstract
There are many versions of the pi-calculus, the calculus of interaction and concurrency. However, only a few variants based in linear logic can express the non-determinism of the full (untyped) pi-calculus while ensuring deadlock freedom. In this paper, we examine the expressive power of sπ+, a typed pi-calculus in which well-typed processes are deadlock-free by construction. We aim at establishing that sπ+ is as expressive as the full pi-calculus by considering the leader election problem, i.e., by exhibiting a well- typed system that describes a symmetric elective network of size five. This document details five attempts at modeling the leader election in sπ+: each attempt tries to solve the main challenge of the previous one, while revealing limitations of the typing system. Our results are negative: they provide evidence of the trade-off between expressiveness and strong correctness properties for typed processes. We conclude by identifying three key factors that limit the expressiveness of sπ+.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Perez Parra, J.A. and Frumin, D. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 17 Jul 2024 10:53 |
| Last Modified: | 17 Jul 2024 10:53 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/33494 |
Actions (login required)
 |
View Item |