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

Jan, 2019

对于未知动态系统与开关线性系统，我们通过几何分析、机会限制优化和联合谱半径等稳定性分析工具，可以在有限的观测数基础上给出概率上的稳定性保证，并提供了计算最佳稳定性保证的方法，可以平衡保证质量和置信水平。

Mar, 2018

本文介绍了一种通过层次化结构和抽象 - 细化循环来加速分析马尔科夫决策过程，针对重复部分具有局部影响的概率程序，将类似的子程序抽象成参数化模板，在需要时对其进行详细分析，从而缓解著名的状态空间爆炸问题。

Jun, 2022

该研究论文提出了一种新颖的控制器合成方法，它不需要任何明确表示噪声分布的方式，而是通过将控制系统抽象为捕捉噪声的有限状态模型，然后使用从场景方法中的工具来计算可能正确的限制，基于一些噪声的有限数量样本。通过缩小合成过程的复杂性，该方法在实际控制系统上的应用具有广泛的适用性。

Jan, 2023

提出了一种新的方法来解决马尔可夫决策过程（MDPs）和概率超性质的控制器合成问题，该方法在超级概率计时逻辑（HyperPCTL）的基础上增加了合成控制器的结构约束，采用逐步修正策略修剪搜索空间并与先前的 SMT 模型检查工具相比取得了显著的性能改进。

Jul, 2023

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

Nov, 2023

本文提出了一个基于高斯过程回归的验证框架，将连续空间系统抽象为有限状态不确定马尔可夫决策过程，利用模型检测工具验证抽象的不确定性，并将结果扩展到基础的部分可观测系统，有效地应用于线性、非线性和切换系统等多种情况下。

Dec, 2021

该论文提出了一种使用 POMDP 模型进行基础设施维护规划的方法，通过使用 MCMC 采样来从实际监控数据中直接估计模型参数并解决模型不确定性问题，最终成功地应用于铁路轨道资产的维护规划。

Dec, 2022

基于数据驱动的方法，我们提出了一种用于端口 - 哈密顿微分代数方程 (DAE) 系统的识别方法，该方法利用输入和状态空间数据来估计 pH-DAE 系统的非线性努力函数。

Jun, 2024

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

Nov, 2021