发表机构
University of Waterloo（滑铁卢大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对步长有界可达概率的马尔可夫链验证问题，提出将概率模型检测转化为稠密张量计算的方法，实现为工具Tessa，在基准测试上较现有方法大幅加速。
AI 中文摘要
我们重新研究了关于步长有界可达概率的马尔可夫链验证问题。现有主流方法依赖于用显式或符号表示法编码状态转移矩阵，这些方法在转移动态稀疏时有效，但在稠密场景下扩展性较差。我们的核心思路是将马尔可夫链的概率模型检测转化为稠密张量上的计算，该方法可利用现成编译器工具链在硬件加速器上优化执行张量计算。我们证明了将概率模型检测映射为张量计算这一方法的正确性，并在名为Tessa的工具中实现了该方法。实证评估显示，在从文献中选取的基准测试上，Tessa相比现有最优方法实现了大幅加速。
英文摘要
We reexamine the problem of verifying Markov chains with respect to step-bounded reachability probabilities. Prevailing approaches rely on encoding the state-transition matrix using either explicit or symbolic representations. While these approaches are effective for sparse transition dynamics, they scale less favorably in the dense regime. Our insight is to cast probabilistic model checking of Markov chains as computations over dense tensors. This methodology enables the use of off-the-shelf compiler toolchains for optimized execution of these tensor computations on hardware accelerators. We prove the soundness of the methodology of mapping probabilistic model checking to tensor computations. We implement our approach in a tool called Tessa . Empirical evaluation shows that Tessa unlocks massive speedups over state-of-theart methods on selected benchmarks from the literature.
CommentsExtended version of a CAV 2026 paper
DOI：10.1007/978-3-032-32537-2_24
