本文介绍了一种名为 Storm 的概率模型检查器，它支持 Markov 链和 Markov 决策过程的离散和连续时间变体，并且支持多个输入语言，包括 JANI 和 PRISM 建模语言，动态故障树，广义随机 Petri 网络和概率保护命令语言。它的特点是具有模块化的设置，在其中求解器和符号引擎可以轻松地交换，并且其 Python API 可以通过封装 Storm 的快速可扩展算法进行快速原型设计。本文重点介绍了 Storm 的主要功能，并解释了如何有效地使用它们。最后，对 Storm 在 QComp 2019 基准集的不同配置进行了实证评估。

Feb, 2020

本文综述了概率模型检测在 PRISM 和 PRISM-games 模型检查器支持下的可观测和不可观测马尔可夫决策过程、顺序和并发随机博弈以及相关概率时态逻辑，以及其在自主系统中的应用，并探讨了未来研究方向和挑战。

Nov, 2021

我们介绍了一种验证随机强化学习政策的方法，该方法与任何强化学习算法兼容，只要算法及其对应的环境共同遵守马尔科夫属性。我们的方法将模型检验技术与强化学习相结合，利用马尔科夫决策过程、训练好的强化学习策略和概率计算树逻辑（PCTL）公式构建一个正式模型，并通过模型检验器 Storm 进行验证。我们在多个基准测试中展示了我们的方法的适用性，并与称为确定性安全估计和简单的整体模型检验方法进行了比较。我们的结果表明，我们的方法适用于验证随机强化学习政策。

Mar, 2024

Markov 决策过程和统计模型检测在未知转移概率、浓度不等式等方面的改进以及实验评估的重要性。

Apr, 2024

近年来，基于模型的强化学习算法在视觉输入环境中展现出了显著的效果。本研究介绍了一种名为 STORM 的高效世界模型架构，它将 Transformer 的强大序列建模和生成能力与变分自编码器的随机性结合起来，取得了 Atari 100k 基准测试的均值人类表现为 126.7％的成绩，同时在使用单个 NVIDIA GeForce RTX 3090 显卡进行 1.85 小时的实时交互训练时仅需 4.3 小时，证明其相对于之前的方法具有更高的效率。

Oct, 2023

本文介绍了一个用于验证机器人安全和可靠性需求的概率模型检查框架，并使用两种新型估计器（基于保守贝叶斯推断和不精确概率模型）从实际操作数据中学习未知的转移参数。在极端环境下的无人潜水器实际部署数据上演示了该方法。

Dec, 2018

介绍和证明了一个基于粒子马尔可夫蒙特卡罗的新的推理方法。该方法适用于图灵完备的概率编程语言，支持使用复杂控制流（包括随机递归）的模型的准确推理，并包括来自贝叶斯非参数统计的基元。实验证明，该方法比之前介绍的单一站点 Metropolis-Hastings 方法更有效。

Jul, 2015

我们提出了一种新技术，通过使用给定模型的 PRISM 程序构建一些模型的小版本并训练一个分类器，然后应用机器学习分类技术来近似相关分区，将分区结果作为标准双模拟技术的初始分区，以减少方法的运行时间。实验结果表明，该方法与最先进的工具相比，可以显著减少运行时间。

Jul, 2023

通过 Stormer，一种基于转换器模型的简单天气预报方法，我们能够以较少的训练数据和计算量实现与现有方法相媲美的准确性，在 7 天以上的天气预报中表现出色，并展示了其有利的扩展性。

Dec, 2023

基于参数不确定性的马尔可夫决策过程，引入 “雷不会击中同一个地方” 原则，对关联的不确定参数进行建模，给出概率保证，并设计出可行的算法以计算最优控制策略。

Jun, 2012