随机马尔可夫奖励模型上可达性问题的算法

我们研究并发展了随机马尔可夫奖励模型（sMRM），它扩展了将转移时间/奖励建模为随机变量的马尔可夫链。本文给出了相关技术，使得在单台计算机上求解规模适中的系统时，能够以高精度计算首次通过时间分布（或奖励分布）。相比之下，朴素模拟技术具有良好的可扩展性，且对于大量不要求高精度的问题已足够；但当需要极高精度解且能够被精确建模时（这可能是一个很大的前提限制），本工作或许具有价值。所述工作与时态逻辑理论交织在一起，虽非主要贡献，但实现了本工作与自动概率分析/验证领域的联系。尽管其引入也掩盖了作为主体的算法细节。我们给出了计算首次通过奖励密度、期望值问题及其他可达性问题的方程。重点在于为首次通过时间/奖励密度寻找严格的数值解。我们改造了高斯消去等线性代数算法，以及幂法、Jacobi 和 Gauss-Seidel 等迭代方法。我们针对离散奖励 sMRM（所有奖励为离散（格点）随机变量）和连续奖励 sMRM（所有奖励为严格连续随机变量）均给出了求解方案。我们的方案使用快速傅里叶变换（FFT）以加速计算，并能够改造已有的卷积求积规则（如梯形法则、Simpson 法则和 Romberg 方法）以获得更精确的解。