Résumé | I'll give an overview of my pd thesis result on parameterized verification of networks composed of many identical processes for which the number of processes is the parameter.
I'll present the decidability of the parameterized reachability problem in selective networks, where the messages only reach a subset of the components. This result is obtained thanks to a reduction to a new model of distributed two-player games for which we prove decidability in coNP of the game problem. Finally, I will present local strategies that enforce all processes to resolve the non-determinism only according to their own local knowledge. Under this assumption of local strategy, we were able to show that the parameterized reachability and synchronization problems are NP-complete. |