We introduce a new setting where a population of agents, each modelled by a finite-state system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player chooses actions, and the second player resolves non-determinism for each agent. The game with m agents is called the m-population game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can playerone control the m-population game for all m in N whatever playertwo does? In this paper, we prove that the population control problem is decidable, and it is a EXPTIME-complete problem. As far as we know, this is one of the first results on parameterized control. Our algorithm, not based on cut-off techniques, produces winning strategies which are symbolic, that i they do not need to count precisely how the population is spread between states. We also show that if the is no winning strategy, then there is a population size cutoff such that playerone wins the m-population game if and only if m< \cutoff. Surprisingly, \cutoff can be doubly exponential in the number of states of the NFA, with tight upper and lower bounds.
@InProceedings{bertrand_et_al:LIPIcs.CONCUR.2017.12, author = {Bertrand, Nathalie and Dewaskar, Miheer and Genest, Blaise and Gimbert, Hugo}, title = {{Controlling a Population}}, booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)}, pages = {12:1--12:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-048-4}, ISSN = {1868-8969}, year = {2017}, volume = {85}, editor = {Meyer, Roland and Nestmann, Uwe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.12}, URN = {urn:nbn:de:0030-drops-78000}, doi = {10.4230/LIPIcs.CONCUR.2017.12}, annote = {Keywords: Model-checking, control, parametric systems} }
Feedback for Dagstuhl Publishing