用张量计算加速马尔可夫链的有限步概率验证
Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains (Extended Version)
- 将概率模型检测转化为稠密张量运算
- 在多个基准上实现显著速度提升
- 适合需要高效验证的系统安全研究者
我们重新审视有限时域内马尔可夫链的可达概率验证问题。现有方法依赖显式或符号化状态转移矩阵表示，虽对稀疏动态有效，但在稠密情形下扩展性较差。我们的核心思想是将马尔可夫链的概率模型检测建模为稠密张量上的计算，从而利用现成编译器工具链，在硬件加速器上优化执行这些张量操作。我们证明了该方法在映射概率模型检测到张量计算时的正确性，并实现了一个名为 Tessa 的工具。实验表明，Tessa 在文献中的若干基准测试中相较当前最优方法实现了巨大加速。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。