Document Open Access Logo

Controlling a Population

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.12.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Nathalie Bertrand
Miheer Dewaskar
Blaise Genest
Hugo Gimbert

Cite AsGet BibTex

Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a Population. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.12

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.
Keywords
  • Model-checking
  • control
  • parametric systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Abdulla, Giorgio Delzanno, Othmane Rezine, Arnaud Sangnier, and Riccardo Traverso. On the verification of timed ad hoc networks. In Proceedings of Formats'11, volume 6919 of Lecture Notes in Computer Science, pages 256-270. Springer, 2011. Google Scholar
  2. Parosh Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theoretical Computer Science, 290(1):241-263, 2003. Google Scholar
  3. S. Akshay, Blaise Genest, Bruno Karelovic, and Nikhil Vyas. On regularity of unary probabilistic automata. In Proceedings of STACS'16, volume 47 of Leibniz International Proceedings in Informatics, pages 8:1-8:14. Leibniz-Zentrum für Informatik, 2016. Google Scholar
  4. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. In Proceedings of PODC'04, pages 290-299. ACM, 2004. Google Scholar
  5. André Arnold, Aymeric Vincent, and Igor Walukiewicz. Games for synthesis of controllers with partial observation. Theoretical Computer Science, 1(303):7-34, 2003. Google Scholar
  6. Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a population. Technical report, HAL, 2017. URL: https://hal.archives-ouvertes.fr/hal-01558029.
  7. Nathalie Bertrand and Paulin Fournier. Parameterized verification of many identical probabilistic timed processes. In Proceedings of FSTTCS'13, volume 24 of Leibniz International Proceedings in Informatics, pages 501-513. Leibniz-Zentrum für Informatik, 2013. Google Scholar
  8. Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Playing with probabilities in reconfigurable broadcast networks. In Proceedings of FoSSaCS'14, volume 8412 of Lecture Notes in Computer Science, pages 134-148. Springer, 2014. Google Scholar
  9. Tomás Brázdil, Petr Jančar, and Antonín Kučera. Reachability games on extended vector addition systems with states. In Proceedings of ICALP'10, volume 6199 of Lecture Notes in Computer Science, pages 478-489. Springer, 2010. Google Scholar
  10. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proceedings of STOCS'17, pages 252-263. ACM, 2017. Google Scholar
  11. Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Infinite synchronizing words for probabilistic automata (erratum). Technical report, CoRR abs/1206.0995, 2012. Google Scholar
  12. Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Limit synchronization in Markov decision processes. In Proceedings of FoSSaCS'14, volume 8412 of Lecture Notes in Computer Science, pages 58-72. Springer, 2014. Google Scholar
  13. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proceedings of STACS'14, volume 25 of Leibniz International Proceedings in Informatics, pages 1-10. Leibniz-Zentrum für Informatik, 2014. Google Scholar
  14. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In Proceedings of LICS'99, pages 352-359. IEEE Computer Society, 1999. Google Scholar
  15. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of population protocols. In Proceedings of CONCUR'15, volume 42 of Leibniz International Proceedings in Informatics, pages 470-482. Leibniz-Zentrum für Informatik, 2015. Google Scholar
  16. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. Google Scholar
  17. Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In Proceedings of ICALP'10, volume 6199 of Lecture Notes in Computer Science, pages 527-538. Springer, 2010. Google Scholar
  18. Marcin Jurdzinski. Small progress measures for solving parity games. In Proceedings of STACS'00, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. Google Scholar
  19. Marcin Jurdziński, Ranko Lazić, and Sylvain Schmitz. Fixed-dimensional energy games are in pseudo polynomial time. In Proceedings of ICALP'15, volume 9135 of Lecture Notes in Computer Science, pages 260-272. Springer, 2015. Google Scholar
  20. Panagiotis Kouvaros and Alessio Lomuscio. Parameterised Model Checking for Alternating-Time Temporal Logic. In Proceedings of ECAI'16, volume 285 of Frontiers in Artificial Intelligence and Applications, pages 1230-1238. IOS Press, 2016. Google Scholar
  21. Pavel Martyugin. Computational complexity of certain problems related to carefully synchronizing words for partial automata and directing words for nondeterministic automata. Theory of Computing Systems, 54(2):293-304, 2014. Google Scholar
  22. Mahsa Shirmohammadi. Qualitative analysis of synchronizing probabilistic systems. PhD thesis, ULB, 2014. Google Scholar
  23. Jannis Uhlendorf, Agnès Miermont, Thierry Delaveau, Gilles Charvin, François Fages, Samuel Bottani, Pascal Hersen, and Gregory Batt. In silico control of biomolecular processes. In Computational Methods in Synthetic Biology, chapter 13, pages 277-285. Humana Press, Springer, 2015. Google Scholar
  24. Mikhail V. Volkov. Synchronizing automata and the Černý conjecture. In Proceedings of LATA'08, volume 5196 of Lecture Notes in Computer Science, pages 11-27. Springer, 2008. Google Scholar
  25. Wieslaw Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(98)00009-7.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact