MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909186786328576 |
|---|---|
| author | Bals, Severin Evangelidis, Alexandros Křetínský, Jan Waibel, Jakob |
| author_facet | Bals, Severin Evangelidis, Alexandros Křetínský, Jan Waibel, Jakob |
| contents | We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN, built on top of the probabilistic model checker PRISM. This new version extends MULTIGAIN's multi-objective capabilities, by allowing for the formal verification and synthesis of controllers for probabilistic systems with multi-dimensional long-run average reward structures, steady-state constraints, and linear temporal logic properties. Additionally, MULTIGAIN 2.0 can modify the underlying linear program to prevent unbounded-memory and other unintuitive solutions and visualizes Pareto curves, in the two- and three-dimensional cases, to facilitate trade-off analysis in multi-objective scenarios. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2305_16752 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints Bals, Severin Evangelidis, Alexandros Křetínský, Jan Waibel, Jakob Artificial Intelligence Logic in Computer Science We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN, built on top of the probabilistic model checker PRISM. This new version extends MULTIGAIN's multi-objective capabilities, by allowing for the formal verification and synthesis of controllers for probabilistic systems with multi-dimensional long-run average reward structures, steady-state constraints, and linear temporal logic properties. Additionally, MULTIGAIN 2.0 can modify the underlying linear program to prevent unbounded-memory and other unintuitive solutions and visualizes Pareto curves, in the two- and three-dimensional cases, to facilitate trade-off analysis in multi-objective scenarios. |
| title | MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints |
| topic | Artificial Intelligence Logic in Computer Science |
| url | https://arxiv.org/abs/2305.16752 |