Verification of stochastic multi-agent systems with forgetful strategies
File(s)p160.pdf (1.19 MB)
Published version
Author(s)
Belardinelli, F
Jamroga, W
Mittelmann, M
Murano, A
Type
Conference Paper
Abstract
Intelligent autonomous agents need to reason about different kinds of uncertainty in a Multi-Agent System (MAS): first, due to the occurrence of randomization and, second, their inability to completely observe the state of the system. In this paper, we investigate the verification of system specifications in probabilistic variants of the logics ATL and ATL∗ under imperfect information (II). The resulting setting combines these two sources of uncertainty and captures the situation in which agents have qualitative uncertainty about the local state as well as quantitative uncertainty about the occurrence of future events. Since the model-checking problem is undecidable when considered in the context of strategies with perfect recall, we focus on memoryless (positional) strategies. As the main result, we show that, in stochastic MAS under II, model-checking Probabilistic ATL is in EXPTIME when agents play probabilistic strategies. Filling the gap in recent work, we also show that model-checking Probabilistic ATL∗ is PSPACE-complete when the proponent coalition is restricted to deterministic strategies.
Date Issued
2024-05-06
Date Acceptance
2024-05-01
Citation
Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS, 2024, pp.160-169
ISBN
979-8-4007-0486-4
ISSN
1548-8403
Publisher
International Foundation for Autonomous Agents and Multiagent Systems
Start Page
160
End Page
169
Journal / Book Title
Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
Volume
2024-May
Copyright Statement
© 2024 International Foundation for Autonomous Agents and Multiagent Systems. This work is licensed under a Creative Commons Attribution International 4.0 License (https://creativecommons.org/licenses/by/4.0/).
License URL
Source
AAMAS '24
Subjects
Stochastic Multi-Agent Systems
Probabilistic Model Checking
Logics for Strategic Reasoning
Publication Status
Published
Start Date
2024-05-06
Finish Date
2024-05-10
Coverage Spatial
Auckland New Zealand