Room 206 (2nd floor, badged access)
17 November 2022 - 14h00
Parameterized verification of Networks with selective broadcast
by Arnaud Sangnier from IRIF
Abstract: We study decision problems for parameterized verification of a formal model of networks with broadcast communication in which the number of participants as the communication topoloby are paramters. The configuration of such a model can be represented thanks to graphs where nodes are labelled with states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. We show that for such a model simple reachability questions are undecidable, but that decidability can be regained by either restricting the set of topologies or by allowing some processes not to receive the emitted messages.
