IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866909183503237120 |
|---|---|
| author | Mathiesen, Frederik Baymler Lahijanian, Morteza Laurenti, Luca |
| author_facet | Mathiesen, Frederik Baymler Lahijanian, Morteza Laurenti, Luca |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_04068 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes Mathiesen, Frederik Baymler Lahijanian, Morteza Laurenti, Luca Systems and Control Logic in Computer Science 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. |
| title | IntervalMDP.jl: Accelerated Value Iteration for Interval Markov Decision Processes |
| topic | Systems and Control Logic in Computer Science |
| url | https://arxiv.org/abs/2401.04068 |