概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。
Aug, 2023
本文介绍了一个用于验证机器人安全和可靠性需求的概率模型检查框架，并使用两种新型估计器（基于保守贝叶斯推断和不精确概率模型）从实际操作数据中学习未知的转移参数。在极端环境下的无人潜水器实际部署数据上演示了该方法。
Dec, 2018
我们介绍了一种验证随机强化学习政策的方法，该方法与任何强化学习算法兼容，只要算法及其对应的环境共同遵守马尔科夫属性。我们的方法将模型检验技术与强化学习相结合，利用马尔科夫决策过程、训练好的强化学习策略和概率计算树逻辑（PCTL）公式构建一个正式模型，并通过模型检验器 Storm 进行验证。我们在多个基准测试中展示了我们的方法的适用性，并与称为确定性安全估计和简单的整体模型检验方法进行了比较。我们的结果表明，我们的方法适用于验证随机强化学习政策。
Mar, 2024
针对由马尔可夫决策过程建模的概率系统，考虑在部分已知环境下综合控制策略，环境由一组马尔可夫链建模，其中每个马尔可夫链描述了环境的不同模式，但环境的模式对于系统是未知的。控制目标为最大化系统满足给定规范的期望概率和最大化最坏情况下满足规范的概率。
Mar, 2012
提出了一种在部分可观察的马尔可夫决策过程（POMDP）中实现满足线性时间逻辑公式的策略的方法，该方法使用基于点的价值迭代方法来高效地近似满足所需逻辑公式的最大概率，并计算相应的置信状态策略。证明该方法适用于大型 POMDP 领域，并为最终策略的性能提供了强大的边界。
Jan, 2020
本文介绍了一种验证方法，用于分析基于代理的混合系统中的决策制定组件，该方法包括适用于基于代理的逻辑组件的模型检查技术，并且该技术与连续部分的混合系统的单独分析相结合，从而允许使用程序模型检查器来验证混合自主系统中决策制定的实际实现。
Oct, 2013
自动化合成控制器，基于概率时间逻辑规范的随机动态模型，通过状态验证技术构建的 iMDP（带概率区间的马尔科夫决策过程），解决安全关键场景中面临的挑战。
Nov, 2023
本文讲述了一种基于特定约束的自主系统与多智能体的优化控制方法，以实现其最大化收益并同时满足时间逻辑约束的概率足够高。
May, 2023
本文提出了一个基于高斯过程回归的验证框架，将连续空间系统抽象为有限状态不确定马尔可夫决策过程，利用模型检测工具验证抽象的不确定性，并将结果扩展到基础的部分可观测系统，有效地应用于线性、非线性和切换系统等多种情况下。
Dec, 2021
使用模型检验创建差分驱动轮式机器人的多步计划，以避免即时危险，并以近实时的方式改善局部障碍物避免的效果。