随机马尔可夫报酬模型的可达性问题的算法
Algorithms for reachability problems on stochastic Markov reward models
摘要：
我们研究和开发的随机马尔可夫奖励模型（sMRM），它扩展了马尔可夫链的过渡时间/奖励建模为随机变量。技术提出，使计算首次通过时间分布（或奖励分布），只有适度规模的系统时，在一台计算机上解决的高精度。相比之下，朴素模拟技术可以扩展，并且足以解决高精度不成问题的大量问题，但是如果可以精确建模（一个潜在的大警告），当需要非常精确的解决方案时，这项工作可能会很有价值。所提出的工作是交织在一起的时态逻辑理论，虽然不是主要的贡献的工作，实现了这项工作的自动概率分析/验证领域的连接。虽然它的承认确实混淆了算法的细节是主要的，但是。我们提出了计算第一通道奖励密度，期望值问题，和其他可达性问题的方程。重点是寻找严格的数值解的首次通过时间/奖励密度。我们采用线性代数算法，如高斯消去法，和迭代法，如功率法，雅可比和高斯-赛德尔。我们提供了两个离散奖励sMRM的解决方案，其中所有奖励离散（格）随机变量。对于连续奖励sMRM，其中所有奖励都是严格连续随机变量。我们的解决方案涉及使用快速傅里叶变换（FFT）进行更快的计算，我们能够适应现有的卷积求积规则，以获得更准确的解决方案，规则，如梯形规则，辛普森规则和龙伯格的方法。
英文摘要：
We study and develop the stochastic Markov reward model (sMRM), which extends the Markov chain where transition time/reward as modelled as random variables. Techniques are presented to enable computing first-passage time distributions (or reward distributions) with high accuracy for only modestly sized systems when solved for on a single computer. In contrast, naive simulations technique scale and are sufficient for a plethora of problems where high accuracy is not an issue, but this work perhaps would be valuable when extremely accurate solutions are demanded if it can be modelled precisely (a potentially big caveat). The work presented is intertwined with theory of temporal logics, although not the major contribution of the work, achieves the connection of this work to the field of automated probabilistic analysis/verification. Although its admittance does obfuscate the algorithmic details that are major, however. We present equations for computing first-passage reward densities, expected value problems, and other reachability problems. The focus was on finding strictly numerical solutions for first-passage time/reward densities. We adapted linear algebra algorithms such as Gaussian elimination, and iterative methods such as the power method, Jacobi and Gauss-Seidel. We provide solutions for both discrete-reward sMRMs, where all rewards discrete (lattice) random variables. And for continuous-reward sMRMs, where all rewards are strictly continuous random variables. Our solutions involve the use of fast Fourier transform (FFT) for faster computation, and we were able to adapt existing quadrature rules for convolution to gain more accurate solutions, rules such as the trapezoid rule, Simpson's rule and Romberg's method.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
