Document Open Access Logo

Concurrent Stochastic Lossy Channel Games

Authors Daniel Stan , Muhammad Najib , Anthony Widjaja Lin , Parosh Aziz Abdulla

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.46.pdf
  • Filesize: 0.88 MB
  • 19 pages

Document Identifiers

Author Details

Daniel Stan
  • EPITA, Le Kremlin-Bicêtre, France
Muhammad Najib
  • Heriot-Watt University, Edinburgh, UK
Anthony Widjaja Lin
  • University of Kaiserslautern-Landau, Germany
  • Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Parosh Aziz Abdulla
  • Uppsala University, Sweden

Funding

  • Lin, Anthony Widjaja: supported by European Research Council under European Union’s Horizon research and innovation programme (grant agreement no https://doi.org/10.3030/101089343).

Acknowledgements

We wish to thank Richard Mayr and all anonymous reviewers for their useful feedback.

Cite AsGet BibTex

Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla. Concurrent Stochastic Lossy Channel Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 46:1-46:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.46

Abstract

Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Verification by model checking
  • Theory of computation → Concurrency
  • Theory of computation → Solution concepts in game theory
Keywords
  • concurrent
  • games
  • stochastic
  • lossy channels
  • wqo
  • finite attractor property
  • cooperative
  • core
  • Nash equilibrium

Metrics

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

Related Versions

References

  1. Alessandro Abate, Julian Gutierrez, Lewis Hammond, Paul Harrenstein, Marta Kwiatkowska, Muhammad Najib, Giuseppe Perelli, Thomas Steeples, and Michael Wooldridge. Rational verification: game-theoretic verification of multi-agent systems. Applied Intelligence, 51(9):6569-6584, 2021. Google Scholar
  2. Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data communicating processes with unreliable channels. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 166-175. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934535.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, and Shankara Narayanan Krishna. Probabilistic total store ordering. In Ilya Sergey, editor, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, volume 13240 of Lecture Notes in Computer Science, pages 317-345. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_12.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. A load-buffer semantics for total store ordering. Logical Methods in Computer Science, 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:9)2018.
  5. Parosh Aziz Abdulla, Nathalie Bertrand, Alexander Moshe Rabinovich, and Philippe Schnoebelen. Verification of probabilistic systems with faulty communication. Inf. Comput., 202(2):141-165, 2005. URL: https://doi.org/10.1016/j.ic.2005.05.008.
  6. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 313-321. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561359.
  7. Parosh Aziz Abdulla, Lorenzo Clemente, Richard Mayr, and Sven Sandberg. Stochastic parity games on lossy channel systems. Log. Methods Comput. Sci., 10(4), 2014. URL: https://doi.org/10.2168/LMCS-10(4:21)2014.
  8. Parosh Aziz Abdulla, Noomene Ben Henda, Luca de Alfaro, Richard Mayr, and Sven Sandberg. Stochastic games with lossy channels. In Roberto M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, volume 4962 of Lecture Notes in Computer Science, pages 35-49. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78499-9_4.
  9. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), Montreal, Canada, June 19-23, 1993, pages 160-170. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287591.
  10. Parosh Aziz Abdulla and Bengt Jonsson. Model checking of systems with many identical timed processes. Theor. Comput. Sci., 290(1):241-264, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00330-9.
  11. Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. Probabilistic strategy logic. In Proceedings of the 28th International Joint Conference on Artificial Intelligence, pages 32-38, 2019. Google Scholar
  12. Benjamin Aminof, Axel Legay, Aniello Murano, Olivier Serre, and Moshe Y Vardi. Pushdown module checking with imperfect information. Information and Computation, 223:1-17, 2013. Google Scholar
  13. Robert J Aumann. Acceptable points in general cooperative n-person games. Contributions to the Theory of Games, 4(40):287-324, 1959. Google Scholar
  14. Robert J. Aumann. The core of a cooperative game without side payments. Transactions of the American Mathematical Society, 98(3):539-552, 1961. URL: http://www.jstor.org/stable/1993348.
  15. Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. A note on the attractor-property of infinite-state Markov chains. Inf. Process. Lett., 97(2):58-63, 2006. URL: https://doi.org/10.1016/j.ipl.2005.09.011.
  16. Christel Baier, Nathalie Bertrand, and Philippe Schnoebelen. Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. Comput. Log., 9(1):5, 2007. URL: https://doi.org/10.1145/1297658.1297663.
  17. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  18. B Douglas Bernheim, Bezalel Peleg, and Michael D Whinston. Coalition-proof Nash equilibria i. concepts. Journal of economic theory, 42(1):1-12, 1987. Google Scholar
  19. Nathalie Bertrand and Philippe Schnoebelen. Model checking lossy channels systems is probably decidable. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 120-135. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_8.
  20. Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci., 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:9)2015.
  21. Laura Bozzelli, Aniello Murano, and Adriano Peron. Module checking of pushdown multi-agent systems. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, volume 17, pages 162-171, 2020. Google Scholar
  22. Taolue Chen, Fu Song, and Zhilin Wu. Global model checking on pushdown multi-agent systems. In Dale Schuurmans and Michael P. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, pages 2459-2465. AAAI Press, 2016. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/11984, URL: https://doi.org/10.1609/AAAI.V30I1.10124.
  23. Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. Theor. Comput. Sci., 386(3):188-217, 2007. URL: https://doi.org/10.1016/j.tcs.2007.07.008.
  24. Javier Esparza, Antonín Kucera, and Stefan Schwoon. Model checking LTL with regular valuations for pushdown systems. Inf. Comput., 186(2):355-376, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00139-1.
  25. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  26. Julian Gutierrez, Lewis Hammond, Anthony W. Lin, Muhammad Najib, and Michael J. Wooldridge. Rational verification for probabilistic systems. In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, pages 312-322, 2021. URL: https://doi.org/10.24963/kr.2021/30.
  27. Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. From model checking to equilibrium checking: Reactive modules for rational verification. Artificial Intelligence, 248:123-157, 2017. Google Scholar
  28. Julian Gutierrez, Paul Harrenstein, and Michael J. Wooldridge. Expresiveness and complexity results for strategic reasoning. In Luca Aceto and David de Frutos-Escrig, editors, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, volume 42 of LIPIcs, pages 268-282. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.268.
  29. Julian Gutierrez, Szymon Kowara, Sarit Kraus, Thomas Steeples, and Michael Wooldridge. Cooperative concurrent games. Artificial Intelligence, 314:103806, 2023. Google Scholar
  30. Julian Gutierrez, Sarit Kraus, and Michael J. Wooldridge. Cooperative concurrent games. In Edith Elkind, Manuela Veloso, Noa Agmon, and Matthew E. Taylor, editors, Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS '19, Montreal, QC, Canada, May 13-17, 2019, pages 1198-1206. International Foundation for Autonomous Agents and Multiagent Systems, 2019. URL: http://dl.acm.org/citation.cfm?id=3331822.
  31. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. URL: https://doi.org/10.1016/j.artint.2020.103353.
  32. Graham Higman. Ordering by divisibility in abstract algebras. In Proc. London Math. Soc., volume 2, pages 326-336, 1952. Google Scholar
  33. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation, 2nd Edition. Addison-Wesley series in computer science. Addison-Wesley-Longman, 2001. Google Scholar
  34. Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis. Making weak memory models fair. Proc. ACM Program. Lang., 5(OOPSLA):1-27, 2021. URL: https://doi.org/10.1145/3485475.
  35. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. URL: http://www.jstor.org/stable/1971035.
  36. Richard Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 297(1-3):337-354, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00646-1.
  37. Aniello Murano and Giuseppe Perelli. Pushdown multi-agent system verification. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 1090-1097. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/158.
  38. John F. Nash. Equilibrium points in n-person games. Proceedings of the National Academy of Sciences of the United States of America, 36(1):48-49, 1950. Google Scholar
  39. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  40. Halsey L. Royden and Patrick M. Fitzpatrick. Real Analysis. Prentice Hall, 2010. URL: https://books.google.fr/books?id=H65bQgAACAAJ.
  41. Herbert E Scarf. The core of an n person game. Econometrica: Journal of the Econometric Society, pages 50-69, 1967. Google Scholar
  42. Philippe Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett., 83(5):251-261, 2002. URL: https://doi.org/10.1016/S0020-0190(01)00337-4.
  43. Tobias Winkler and Maximilian Weininger. Stochastic games with disjunctions of multiple objectives. In Pierre Ganty and Davide Bresolin, editors, Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, Padua, Italy, 20-22 September 2021, volume 346 of EPTCS, pages 83-100, 2021. URL: https://doi.org/10.4204/EPTCS.346.6.
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