We are happy to present Lucie Guillou’s talk titled “Safety Analysis of Parameterized Networks with Non-Blocking Rendez-Vous and Broadcasts”.

I will present two recent joint works done with Arnaud Sangnier and Nathalie Sznajder. We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. We study two coverability problems with a parameterised number of processes (state coverability and configuration coverability). It is already known that these problem are Ackermann-hard (and decidable) in the general case. This already holds when the processes communicate only by broadcasts. We show that when forbidding broadcasts, the two problems are EXPSPACE-complete. We also study a restriction on the protocol: a Wait-Only protocol has no state from which a process can send and receive messages. We show that without broadcasts, both problems are PTIME-complete in this restriction, and with broadcasts, state coverability is PTIME-complete and configuration coverability PSPACE-complete.

Bio

Lucie is a final-year PhD student at IRIF, in Paris, France, where she is working with Arnaud Sangnier and Tali Sznajder on distributed systems with an unbounded number of agents. Her research focuses on distributed systems with an unbounded number of agents, particularly on the complexities of certain verification problems in these networks.