Autonomous systems often operate in multi-agent settings and need to make concurrent, strategic decisions, typically in uncertain environments. Verification and control problems for these systems can be tackled with concurrent stochastic games (CSGs), but this model requires transition probabilities to be precisely specified - an unrealistic requirement in many real-world settings. We introduce *robust CSGs* and their subclass *interval CSGs* (ICSGs), which capture epistemic uncertainty about transition probabilities in CSGs. We propose a novel framework for *robust* verification of these models under worst-case assumptions about transition uncertainty. Specifically, we develop the underlying theoretical foundations and efficient algorithms, for finite- and infinite-horizon objectives in both zero-sum and nonzero-sum settings, the latter based on (social-welfare optimal) Nash equilibria. We build an implementation in the PRISM-games model checker and demonstrate the feasibility of robust verification of ICSGs across a selection of large benchmarks.

翻译：自主系统通常在多智能体环境中运行，需要在不确定环境下做出并发的策略性决策。这类系统的验证与控制问题可采用并发随机博弈（CSG）模型处理，但该模型要求精确指定转移概率——这在许多实际场景中是不切实际的要求。我们提出*鲁棒CSG*及其子类*区间CSG*（ICSG），用以刻画CSG中转移概率的认知不确定性。针对转移不确定性的最坏情况假设，我们为这些模型建立了*鲁棒*验证的新框架。具体而言，我们为零和与非零和场景（后者基于社会福利最优的纳什均衡）中的有限与无限时域目标，发展了基础理论体系与高效算法。我们在PRISM-games模型检测器中实现了该框架，并通过一系列大型基准案例验证了ICSG鲁棒验证的可行性。