Corto Mascle (LaBRI)
Title: Verification of Population Protocols with Unordered Data
Abstract:
Population protocols are a well-studied model of distributed computation in which a crowd of anonymous finite-state agents communicate via pairwise interactions. Together they decide whether their initial configuration, i.e., the initial distribution of agents in each state, satisfies a property. We will start with a reminder on Population protocols.
Population protocols with unordered data (PPUD) is an extension introduced by Blondin and Ladouceur (ICALP'23) where processes carry a piece of data from an infinite data domain. We consider the decidability and complexity of formally verifying these protocols. We show that checking if a PPUD is well-specified, i.e., whether it correctly computes some function, is undecidable in general. By contrast, we consider a subclass of PPUD, called Immediate-Observation, on which the problem is decidable. Moreover, we exhibit a large yet natural class of problems on IOPPUD, which are all decidable in EXPSPACE. We will also see some intriguing open problems on this model.