Rational verification with quantitative probabilistic goals

Conference item

We study the rational verification problem for multi-agent systems in a setting where agents have quantitative probabilistic goals. We use concurrent stochastic games to model multi-agent systems and assume players desire to maximise the probability of satisfying their goals, specified using Linear Temporal Logic (LTL). The main decision problem in this setting is whether a given LTL formula is almost surely satisfied on some pure Nash equilibrium of a given game. We prove that this problem is undecidable in the general case, and then characterise the complexity of this problem under various restrictions on strategies. We also study the problem of deciding whether a given strategy profile is a Nash equilibrium in a given game and show that, unlike the previous verification problem, this question is decidable for several common strategy models.

Authors: Hyland, D; Gutierrez, J; Shankaranarayanan, K; Wooldridge, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: International Foundation for Autonomous Agents and Multiagent Systems
• Host title: AAMAS '24: Proceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems
• Pages: 871-879
• Publication date: 2024-05-06
• Acceptance date: 2023-12-20
• Event title: 23rd International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2024)
• Event location: Auckland, New Zealand
• Event website: https://www.aamas2024-conference.auckland.ac.nz/
• Event start date: 2024-05-06
• Event end date: 2024-05-10
• EISSN: 1558-2914
• ISSN: 1548-8403
• ISBN: 9798400704864
• Language: English
• Keywords: computational game theory; formal verification; linear temporal logic; multi-agent systems; quantitative probabilistic goals