Parameterized Reachability in Networks with Many Identical Processes

Arnaud Sangnier
Université Paris Diderot - Paris VII
Friday, 12 December, 2014 - 14:00
NO Solvay (5th floor)

In this talk, we will study the decidability and complexity of reachability problems in networks where the number of entities is a priori unknown but where each process follows the same behavior. I will first describe algorithmic methods to analyze such networks considering different means of communication between the processes such as rendez-vous communication (with or without a central controller), broadcast communication or reconfigurable broadcast communication (where the broadcast messages are not received by all the processes of the networks). I will then present some considerations on how local strategies can be considered in such networks and I will end  by providing some future research directions for the field of parameterized verifications motivated by concrete examples.