License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2017.12
URN: urn:nbn:de:0030-drops-78000
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7800/
Go to the corresponding LIPIcs Volume Portal

Bertrand, Nathalie ; Dewaskar, Miheer ; Genest, Blaise ; Gimbert, Hugo

Controlling a Population

pdf-format:
LIPIcs-CONCUR-2017-12.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{bertrand_et_al:LIPIcs:2017:7800,
  author =	{Nathalie Bertrand and Miheer Dewaskar and Blaise Genest and Hugo Gimbert},
  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 =	{Roland Meyer and Uwe Nestmann},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7800},
  URN =		{urn:nbn:de:0030-drops-78000},
  doi =		{10.4230/LIPIcs.CONCUR.2017.12},
  annote =	{Keywords: Model-checking, control, parametric systems}
}

Keywords: Model-checking, control, parametric systems
Collection: 28th International Conference on Concurrency Theory (CONCUR 2017)
Issue Date: 2017
Date of publication: 01.09.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI