IntervalMDP.jl：针对区间马尔可夫决策过程的加速值迭代
IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes
AI总结：
本文提出 Julia 包 IntervalMDP.jl，利用多线程 CPU 和 GPU 加速值迭代算法，高效支持区间马尔可夫决策过程的概率分析、策略综合与验证，在计算时间和内存消耗上显著优于现有工具。
摘要：
在本文中，我们提出了 IntervalMDP.jl，一个用于区间马尔可夫决策过程（IMDPs）概率分析的 Julia 包。IntervalMDP.jl 促进了最优策略的综合，以及针对可达性规范和折扣奖励属性对 IMDPs 的验证。该库支持稀疏矩阵，并兼容分析概率模型的常用工具（如 PRISM）的数据格式。IntervalMDP.jl 的一个关键特性是，它同时提供了用于 IMDPs 值迭代算法的多线程 CPU 和 GPU 加速实现。具体而言，IntervalMDP.jl 利用 Julia 类型系统和值迭代固有的可并行特性，提高了执行 IMDPs 分析的效率。在一组示例中，我们展示了 IntervalMDP.jl 在计算时间和内存消耗方面均大幅优于现有的 IMDPs 验证与策略综合工具。
英文摘要：
In this paper, we present IntervalMDP.jl, a Julia package for probabilistic analysis of interval Markov Decision Processes (IMDPs). IntervalMDP.jl facilitates the synthesis of optimal strategies and verification of IMDPs against reachability specifications and discounted reward properties. The library supports sparse matrices and is compatible with data formats from common tools for the analysis of probabilistic models, such as PRISM. A key feature of IntervalMDP.jl is that it presents both a multi-threaded CPU and a GPU-accelerated implementation of value iteration algorithms for IMDPs. In particular, IntervalMDP.jl takes advantage of the Julia type system and the inherently parallelizable nature of value iteration to improve the efficiency of performing analysis of IMDPs. On a set of examples, we show that IntervalMDP.jl substantially outperforms existing tools for verification and strategy synthesis for IMDPs in both computation time and memory consumption.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
