Séminaire

Possibilité de visio-conférence 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. Finally, we consider verification problem under local strategies, where we assume that each process in the network behaves the same according to its past.