该研究旨在为线性动态的离散时间随机混合系统开发高效的抽象方法，通过不确定的 MARKOV 决策过程解决了现有形式方法的限制，可以计算精确的抽象误差，并应用于有限和无限时间范围内的合成步骤，大大缩减抽象误差，提高可缩放性。

Jan, 2019

本研究提出了基于抽象的分析方法，结合有限马尔科夫决策过程和多项式时间算法，用以验证多面体概率混合系统的稳定性。

Mar, 2023

本文提出了一种新的逻辑 PrSTL 作为表达随机性质和强制其概率保证的表现语言，并展示了如何使用这种逻辑对具有随机性质的智能物理系统进行控制器合成，其关键特点是适应性逻辑并随着系统遇到附加数据而变化，并通过合成多种情况下无人机和自主车辆的控制器来演示我们的方法。

Oct, 2015

本文提出了一种名为 AMYTISS 的软件工具，用于为大规模随机系统设计构造正确控制器。该工具利用高性能计算平台和云计算服务解决了状况膨胀问题，并以几个案例研究来验证了其性能表现。

May, 2020

应用形式化规范方法和自动验证技术，开发了一种检验统计程序正确性的新方法，可以避免在科学研究中广泛存在的统计方法滥用和误解问题。

May, 2024

自动化合成控制器，基于概率时间逻辑规范的随机动态模型，通过状态验证技术构建的 iMDP（带概率区间的马尔科夫决策过程），解决安全关键场景中面临的挑战。

Nov, 2023

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

Feb, 2020

本文介绍了一种基于采样的策略综合算法，用于处理具有复杂连续动态的非确定性混合系统在时间和可达性约束下的情况，其目的是综合出一个反应式策略以保证满足所有可能对手步骤的要求。实验表明，该算法具有广泛适用性并一直领先于现有技术。

Apr, 2023

我们推出了新的概率模型检查器 storm，支持分析离散和连续时间的 Markov 链和 MDPs 的变体，还支持多种建模语言和快速的可扩展算法。

Feb, 2017

使用马尔可夫链蒙特卡洛采样器快速探索所有可能的程序空间，将循环无关的二进制超级优化任务表示为随机搜索问题，将变换正确性和性能改进的竞争约束编码为成本函数，虽然我们的方法牺牲了完整性，但我们能够考虑到的程序范围和我们所生产的程序的质量远超过现有的超级优化器，我们的原型实现，STOKE，能够从 llvm -O0 编译的 64 位 X86 二进制代码开始，生成与或胜过启用全面优化的 gcc 生成的代码序列，并且在某些情况下能够胜过专家手写的汇编语言。

Nov, 2012