[MTV] Corto Mascle - Parameterized Broadcast Networks with Registers
We consider the parameterized verification of arbitrarily large networks of agents which communicate
through unreliable broadcasts. In addition, agents have local registers which are initially distinct and may therefore be thought of as identifiers.
Agents may append register values to their messages, store the ones they receive and apply (in)equality tests.
In the talk, we will see how we can apply well quasi-orders to obtain decidability of the coverability problem for such systems, starting with a relevant easier subcase.
On the other hand, we will see that other classical problems, such as the target problem, where all processes must synchronize on a given state, are undecidable.
By contrast, those problems fall in NP when processes only have access to one register.
This is joint work with Lucie Guillou and Nicolas Waldburger.