本文研究了参数化马尔可夫链的一些任务，包括计算可达性概率和符号表示，提出了一种方法来提高计算有理函数的实现，同时，对参数化马尔可夫链和概率计算树逻辑的模型检查问题进行了复杂度理论讨论，得出了多项式和指数时间算法的边界。

Sep, 2017

我们提出了一种简单的技术，用于验证具有参数转换概率的概率模型，通过将参数转换替换为极值的不确定选择，可以分析结果，在此基础上利用现成的方法计算区域在参数空间中的概率的上下界，其优美之处在于其适用于各种概率模型，特别是提供了执行参数综合的马尔可夫决策过程的第一个完整的有效方法。

Feb, 2016

ProbReach 是一种用于验证随机混合系统中概率可达性的工具。它采用了 delta - 可达性的弱化概念，并实现了一个适用于混合系统的概率版本，在多个基准测试中表现出令人满意的结果，并且有并行实现的概率。

Oct, 2014

本文提出了一种新颖的敏感性分析方法，针对参数健壮的马尔可夫链，基于概率分布，对转移概率的偏导数进行度量，并提出了高效的方法来计算这些偏导数，同时展示了一个扩展方法来选择具有最大偏导数的 k 个参数，该方法基于线性规划并绕过参数值计算这些程序的不同部分。实验表明，该方法具有扩展性和应用性，适用于具有数百万状态和数千参数的模型，并应用于从敏感性分析中获取迭代学习方案中的收益。

May, 2023

本研究开发了一种双向算法来估计马尔可夫链的多步转移概率，该方法适用于离散状态空间上的任何马尔可夫链，可以用于计算多步转移概率的函数，并且在 “稀疏” 马尔可夫链中，该方法的运行时间比 Monte Carlo 和功率迭代算法更小。

Jul, 2015

提出了一个泛用的框架，应用学习算法和启发式指导来验证马尔可夫决策过程 (MDP)，主要关注概率可达性问题，包括精确和近似的情况，不受时间限制或折扣因子等条件的限制。

Mar, 2024

使用强化学习方法，我们通过特征化随机定向图中的可达性概率，展示了随机定向图中的转移概率动态可以被建模成一个差分包含，进而被理解为一个 Markov 决策过程。通过这个框架，我们提出了一种确定奖励功能的方法，以提供随机定向图中一组节点的可达性概率上下限。该方法的有效性通过应用于由移动代理的接近模式生成的时间变化的接触网络的流行病疾病扩散得到证明。

Feb, 2022

在无向图中，基于 “簇弹出” 算法的期望运行时间受输入规模的多项式限制，得到了全多项式时间随机逼近方案 (FPRAS) 来解决全终端网络可靠性问题。

Sep, 2017

介绍了一种使用共轭先验和仿射变换降低蒙特卡罗估计方差的动态机制，该机制适用于解决概率程序中可分析子结构的问题，并加以应用于顺序蒙特卡罗推断和 Anglican 等编程语言。

Aug, 2017

使用符合推断进行基于数据驱动的离散时间随机动态系统的可达性分析，将数据集转化为代理预测模型，通过符合推断量化预测模型的误差，从而提供概率可达性保证。该方法适用于复杂闭环动态难以使用符号模型建模的学习增强控制系统。

Sep, 2023