Title - Verification and Synthesis of Parameterized Concurrent Systems

Abstract - 

This thesis is at the crossroad of verification and synthesis of parameterized concurrent systems. The parameterized model checking problem asks whether a system satisfies a given specification independently of the number of its components, whereas synthesis requires an algorithmic design of protocols for its components so that the specification is satisfied.

We study a parameterized model of networks where processes are distributed over an undirected graph, running the same broadcast protocol, and communicating via selective broadcasts of messages. The coverability problem asks whether a given state of the protocol is coverable. We show that for positive instances of the coverability problem in recon- figurable semantics, the size (cutoff) and the length (covering length) of a minimal covering execution
is linearly and quadratically bounded, respectively. We introduce loss-on-broadcast semantics, and show similar bounds for the cutoff and the covering length.

The interactions between agents can be modelled using games. We introduce and study two different settings of the so-called parameterized con- current games, a model of concurrent games with arbitrarily many agents. First, we consider a scenario of a distinguished player Eve trying to achieve a goal against arbitrarily many opponents, irrespective of their strategies. We prove the existence of a winning strategy for Eve is decidable, and show tight complexity bounds for reachability objectives. Second, we consider a coalition game where all players collectively try to achieve a common goal. We consider safety objectives and show the existence of a winning coalition strategy is decidable, and prove complexity bounds for the same.

Jury - 
Giorgio DELZANNO, Università di Genova, Italy - Reviewer
Emmanuel FILIOT, Université libre de Bruxelles, Belgium - Reviewer
Martin ZIMMERMANN, Aalborg Universitet, Denmark- Examiner
Benedikt BOLLIG, Université Paris-Saclay, France - Examiner
Patricia BOUYER-DECITRE, Université Paris-Saclay, France - PhD supervisor
Nathalie BERTRAND, Inria Rennes Bretagne-Atlantique, France - PhD co-supervisor