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.

SWS   Info

MPI Audience

English

120 Minutes

Kaiserslautern

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.

Lisa-Marie Lembach

+49 631 9303 9606

--email hidden