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.

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