Verification and Synthesis of Parameterized Concurrent Systems
by Anirban Majumdar
Thursday 30 September 2021 at 14h00
Room 1Z68 ENS Paris-Saclay as well as online
Zoom link: https://cnrs.zoom.us/j/99606315744
Meeting ID: 996 0631 5744
Passcode: anirb1
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 reconfigurable 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, CNRS, Université Paris-Saclay, France - Examiner
- Patricia BOUYER-DECITRE, CNRS, Université Paris-Saclay, France - PhD supervisor
- Nathalie BERTRAND, Inria Rennes Bretagne-Atlantique, France - PhD co-supervisor