2017, Balasubramanian’s internship

A.R. Balasubramanian focused on the verification of parametric-size networks of identical components broadcasting messages to their neighbours (as given by the topology of the network). More precisely, he studied the problem of synchronizing all components to a subset of states in settings where the topology of the network may evolve (under various constraints) over time. After proving that the generic problem is undecidable when bounded number of changes between two message exchanges, he obtained a number of decidability results (e.g. when considering topologies of bounded degree).

We are currently writing a paper summarizing those results.