Document Open Access Logo

Synthesizing Safe Coalition Strategies

Authors Nathalie Bertrand , Patricia Bouyer , Anirban Majumdar

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.39.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Nathalie Bertrand
  • Université Rennes, Inria, CNRS, IRISA, Rennes, France
Patricia Bouyer
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, Gif-sur-Yvette, France
Anirban Majumdar
  • Université Rennes, Inria, CNRS, IRISA, Rennes, France
  • Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, Gif-sur-Yvette, France

Cite AsGet BibTex

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Synthesizing Safe Coalition Strategies. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.39

Abstract

Concurrent games with a fixed number of agents have been thoroughly studied, with various solution concepts and objectives for the agents. In this paper, we consider concurrent games with an arbitrary number of agents, and study the problem of synthesizing a coalition strategy to achieve a global safety objective. The problem is non-trivial since the agents do not know a priori how many they are when they start the game. We prove that the existence of a safe arbitrary-large coalition strategy for safety objectives is a PSPACE-hard problem that can be decided in exponential space.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • concurrent games
  • parameterized verification
  • strategy synthesis

Metrics

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

Related Versions

References

  1. Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS'98), pages 564-575. IEEE Computer Society Press, 1998. URL: https://doi.org/10.1109/SFCS.1998.743507.
  2. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49:672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
  3. Krzysztof Apt and Dexter C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307-309, May 1986. URL: https://doi.org/10.1016/0020-0190(86)90071-2.
  4. Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Concurrent parameterized games. In Proceedings o the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'19), volume 150 of LIPIcs, pages 31:1-31:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.31.
  5. Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Synthesizing safe coalition strategies, 2020. URL: https://arxiv.org/abs/2008.03770.
  6. Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, and Adwait Amit Godbole. Controlling a population. Logical Methods in Computer Science, 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:6)2019.
  7. Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Playing with probabilities in reconfigurable broadcast networks. In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS'14), volume 8412 of Lecture Notes in Computer Science, pages 134-148. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_9.
  8. Dietmar Berwanger, Lukasz Kaiser, and Bernd Puchala. A perfect-information construction for coordination in games. In Proceedings of the 31th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'11), volume 13 of LIPIcs, pages 387-398. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.387.
  9. Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
  10. Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash equilibria in concurrent games. Logical Methods in Computer Science, 11(2:9), 2015. URL: https://doi.org/10.2168/LMCS-11(2:9)2015.
  11. Tristan Charrier, Arthur Queffelec, Ocan Sankur, and François Schwarzentruber. Reachability and coverage planning for connected agents. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI'19), pages 144-150. ijcai.org, 2019. URL: https://doi.org/10.24963/ijcai.2019/21.
  12. Thomas Colcombet, Nathanaël Fijalkow, and Pierre Ohlmann. Controlling a random population. In Proceedings of the 23rd International Conference on Foundations of Software Science and Computation Structures (FOSSACS'20), volume 12077 of Lecture Notes in Computer Science, pages 119-135. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_7.
  13. Giorgio Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design, 23(3):257-301, 2003. URL: https://doi.org/10.1023/A:1026276129010.
  14. E. Allen Emerson and Vineet Kahlon. Reducing model checking of the many to the few. In Proceedings of the 17th International Conference on Automated Deduction (CADE'00), volume 1831 of Lecture Notes in Computer Science, pages 236-254. Springer, 2000. URL: https://doi.org/10.1007/10721959_19.
  15. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS'14), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
  16. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), volume 6015 of Lecture Notes in Computer Science, pages 190-201. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  17. Igor Konnov, Helmut Veith, and Josef Widder. What you always wanted to know about model checking of fault-tolerant distributed algorithms. In Proceedings of the 10th International Andrei Ershov Informatics Conference (PSI'15), volume 9609 of Lecture Notes in Computer Science, pages 6-21. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-41579-6_2.
  18. Corto Mascle, Mahsa Shirmohammadi, and Patrick Totzke. Controlling a random population is EXPTIME-hard, 2019. URL: https://arxiv.org/abs/1909.06420.
  19. Swarup Mohalik and Igor Walukiewicz. Distributed games. In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), volume 2914 of Lecture Notes in Computer Science, pages 338-351. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24597-1_29.
  20. Gary L. Peterson and John H. Reif. Multiple-person alternation. In Proceedings of the 20th Annual Symposium on Foundations of Computer Science (FOCS'79), pages 348-363. IEEE Computer Society Press, 1979. URL: https://doi.org/10.1109/SFCS.1979.25.
  21. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In Proceedings of the 31st Annual Symposium on Foundations of Computer Science (FOCS'90), volume 2, pages 746-757. IEEE Computer Society Press, 1990. URL: https://doi.org/10.1109/FSCS.1990.89597.
  22. Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time (preliminary report). In Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC'73), pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
  23. Michael Ummels and Dominik Wojtczak. The complexity of Nash equilibria in limit-average games. In Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, pages 482-496. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_32.
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