Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.

概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。

多智能体验证与控制的概率模型检验