Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917568512524288 |
|---|---|
| author | Watanabe, Kazuki van der Vegt, Marck Hasuo, Ichiro Rot, Jurriaan Junges, Sebastian |
| author_facet | Watanabe, Kazuki van der Vegt, Marck Hasuo, Ichiro Rot, Jurriaan Junges, Sebastian |
| contents | Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_08377 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Pareto Curves for Compositionally Model Checking String Diagrams of MDPs Watanabe, Kazuki van der Vegt, Marck Hasuo, Ichiro Rot, Jurriaan Junges, Sebastian Logic in Computer Science Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally described in a high-level description formalism. In particular, this paper considers string diagrams, which specify an algebraic, sequential composition of subMDPs. Towards their compositional verification, the key challenge is to locally optimize schedulers on subMDPs without considering their context in the string diagram. This paper proposes to consider the schedulers in a subMDP which form a Pareto curve on a combination of local objectives. While considering all such schedulers is intractable, it gives rise to a highly efficient sound approximation algorithm. The prototype on top of the model checker Storm demonstrates the scalability of this approach. |
| title | Pareto Curves for Compositionally Model Checking String Diagrams of MDPs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.08377 |