Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, however, transition probabilities are only estimated from data and may therefore be partially unknown or subject to perturbations. In this paper, we study the verification of robust strategies in stochastic multi-agent systems with imperfect information, in which coalitions must satisfy a temporal specification while dealing with uncertain system transitions, partial observation, and adversarial agents. By focusing on bounded-memory strategies, we introduce a robust variant of the model-checking problem for a probabilistic, observation-based extension of Alternating-time Temporal Logic. We characterize the complexity of this problem under different notions of perturbation, thereby clarifying the computational cost of robustness in stochastic multi-agent verification and supporting the use of bounded-memory strategies in uncertain environments.

翻译：随机多智能体系统是自主控制器、通信协议和网络物理基础设施的核心建模框架。然而，在许多此类系统中，转移概率仅从数据中估计得出，因此可能部分未知或易受扰动影响。本文研究了具有不完美信息的随机多智能体系统中鲁棒策略的验证问题，其中联盟必须在满足时序规约的同时，处理不确定的系统转移、部分可观测性以及对抗性智能体。通过聚焦于有限记忆策略，我们针对概率化、基于观测的交替时序逻辑扩展，引入了模型检测问题的鲁棒变体。我们刻画了该问题在不同扰动概念下的计算复杂度，从而阐明了随机多智能体验证中鲁棒性的计算代价，并支持在不确定环境中使用有限记忆策略。