A Lazy Abstraction Algorithm for Markov Decision Processes: Theory and Initial Evaluation
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_ | 1866929370978844672 |
|---|---|
| author | Szekeres, Dániel Marussy, Kristóf Majzik, István |
| author_facet | Szekeres, Dániel Marussy, Kristóf Majzik, István |
| contents | Analysis of Markov Decision Processes (MDP) is often hindered by state space explosion. Abstraction is a well-established technique in model checking to mitigate this issue. This paper presents a novel lazy abstraction method for MDP analysis based on adaptive simulation graphs. Refinement is performed only when new parts of the state space are explored, which makes partial exploration techniques like Bounded Real-Time Dynamic Programming (BRTDP) retain more merged states. Therefore, we propose a combination of lazy abstraction and BRTDP. To evaluate the performance of our algorithm, we conduct initial experiments using the Quantitative Verification Benchmark Set. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_00824 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Lazy Abstraction Algorithm for Markov Decision Processes: Theory and Initial Evaluation Szekeres, Dániel Marussy, Kristóf Majzik, István Logic in Computer Science Analysis of Markov Decision Processes (MDP) is often hindered by state space explosion. Abstraction is a well-established technique in model checking to mitigate this issue. This paper presents a novel lazy abstraction method for MDP analysis based on adaptive simulation graphs. Refinement is performed only when new parts of the state space are explored, which makes partial exploration techniques like Bounded Real-Time Dynamic Programming (BRTDP) retain more merged states. Therefore, we propose a combination of lazy abstraction and BRTDP. To evaluate the performance of our algorithm, we conduct initial experiments using the Quantitative Verification Benchmark Set. |
| title | A Lazy Abstraction Algorithm for Markov Decision Processes: Theory and Initial Evaluation |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.00824 |