《核外求解方法在马尔可夫模型中的应用》

《理论计算机科学电子札记》68卷第4期（2002年）URL：http://www.elsevier.nl/locate/entcs/volume 68. html16页s一种符号化的核外求解方法马尔可夫模型Marta Kwiatkowska、Rashid Mehmood、GethinNorman和David Parker计算机科学学院，伯明翰大学，伯明翰B15 2TT，英国摘要尽管有相当大的误差，状态空间爆炸问题仍然是马尔可夫模型分析中的一个问题。给定结构，符号表示可以导致模型的非常紧凑的编码。然而，符号方法的一个主要障碍是需要在主存储器中显式地存储概率向量。 在本文中，我们提出了一种新的算法，放宽这些内存限制存储在磁盘上的概率向量。该算法已实现使用基于MTBDD的数据结构来存储矩阵和数组来存储向量。我们报告两个基准模型的实验结果，看板制造系统和可伸缩的制造系统，模型高达1.33亿个国家。1介绍离散状态马尔可夫模型被广泛用于通信网络和计算机系统的分析。假设概率分布为指数分布，则将此类系统建模为连续时间马尔可夫链（CTMC）通常是方便的CTMC可以由一组状态和包含状态转换速率作为系数的转换速率矩阵Q可以使用概率模型检查来分析CTMC所需或期望的性能属性被指定为时态逻辑CSL中的公式，然后使用适当的模型检查算法自动验证。这些算法的一个核心组成部分是稳态概率的CTMC的计算。这可归结为求解Ax=b形式的线性方程组的经典问题，其中b= 0。存在一系列解决方案技术来对抗1电子邮件：rxm@cs.bham.ac.uk2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。维亚特科夫斯卡 等人2所谓状态空间爆炸（也称为大）问题。这些方法包括符号技术[8，13，15，25，14]，在-的-的方法[11]和克罗内克方法[22]。虽然一些新的发展，如矩阵Diagrams（MD）[5，4，20]和混合MTBDD方法[17]允许CTMC矩阵的非常紧凑和时间效率的编码，但它们受到数值求解阶段所需的概率向量的显式存储的阻碍马尔可夫模型领域的一个既定的研究方向涉及使用稀疏存储格式存储CTMC矩阵扩展的数值求解技术这些是最普遍适用的技术，速度快，但不像符号方法那样紧凑。通过使用磁盘（所谓的核外技术2）来存储CTMC矩阵[10]和并行化基于磁盘的数值解[16，2]，已经获得了改进然而，这些方法的核心内存需求也主要是由一个向量的存储与大小成比例的模型中的状态作者在[19]中提出了一种核外算法，该算法放宽了显式稀疏方法的上述内存限制在本文中，我们介绍了一种新的算法，它放宽了相同的内存限制的符号方法，我们称之为一个符号的核心算法。我们的符号核外算法背后的哲学是使用[17]的基于MTBDD的数据结构存储CTMC矩阵，并将概率向量显式存储在磁盘上。该算法将概率向量划分为一定数量的块用于此目的。由于矩阵存储在基于MTBDD的数据结构中，因此可以在计算中根据需要提取块它读入主存储器的概率向量的块，执行所需的计算，使用从基于MTBDD的数据结构中提取的矩阵块，并将概率向量的更新元素写回磁盘上。为了从算法中获得性能，将工作分为两个并发进程;一个执行计算，而另一个调度磁盘读写。该算法的内存需求取决于块的数量;概率向量被划分成的块的数量越高，则该算法以增加的运行时间为代价所需的内存就越少我们给出了应用于看板制造系统[6]和柔性制造系统（FMS）[7]的符号核外算法的实验结果2被设计成当其数据结构存储在磁盘上的算法被称为核外算法; Toledo在数值线性代数中对这种算法进行了调查，见[27]。维亚特科夫斯卡 等人31.1工具PRISM本文中使用的所有CTMC矩阵均由PRISM工具生成PRISM是伯明翰大学正在开发的一种概率模型检查器它支持三种模型：离散时间马尔可夫链，连续时间马尔可夫链和马尔可夫决策过程。对于数值求解阶段，它提供了三个引擎：一个使用纯MTBDD，一个基于核内稀疏迭代方法，第三个是前两个的混合。对一些案例进行了分析[23]。本文的一部分，一个eAterort，以提高范围的解决方案提供的方法PRISM。2数值考虑本文主要研究连续时间马尔可夫链的数值解法求解CTMC以获得稳态概率向量的任务可以在数学上写为：Σ−1πQ= 0，π = 1，（1）=零其中Q∈R×是CTMC的无穷小生成矩阵，并且π∈R是稳态概率向量。矩阵Q通常非常稀疏;关于这些矩阵的性质的进一步细节可以在[26].方程（1）可以重新表述为Q π= 0，并且可以使用用于解形式为Ax=b形式为Ax=b的线性方程组的数值解法大致分为直接法和迭代法。对于大型系统，直接方法变得不切实际，这是由于在因子分解阶段产生新条目而导致的填充现象迭代方法产生一系列近似，仅收敛于解的极限。从给定的近似解开始，这些方法在每次迭代中修改近似的分量，直到达到所需的精度。关于直接方法的更多信息见[12]，关于迭代方法见[24，26]。我们在这里集中在平稳迭代方法。例如，在Jacobi方法的每次迭代中，我们计算：x（）=1一.Σb −x（−1）a=/Σ、（二）对于0≤i n，其中a表示矩阵的第i行和第j列中的元素A. 我们注意到在方程（2）中，解向量的新近似维亚特科夫斯卡 等人4××（）下一页（x（））仅使用解（x（−1））的旧近似计算。Gauss-Seidel（GS）迭代法在实践中比Jacobi方法收敛得更快，它使用最新可用的解的近似：对于0≤i

下载后可阅读完整内容，剩余1页未读，立即下载