MULTIGAIN 2.0: MDP controller synthesis for multiple
mean-payoff, LTL and steady-state constraints✱

D 2024

MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL

Základní údaje

Originální název

MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱

Autoři

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL

Vydání

Hong Kong SAR, China, Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, od s. 1-7, 7 s. 2024

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/24:00139092

Organizační jednotka

Fakulta informatiky

ISBN

979-8-4007-0522-9

DOI

https://doi.org/10.1145/3641513.3650135

EID Scopus

2-s2.0-85193855276

Klíčová slova anglicky

Markov decision process; quantitative verification; probabilistic model checking; controller synthesis

Štítky

firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 26. 3. 2025 16:20, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 multidimensional 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.

Návaznosti

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL. MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. Online. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024. Hong Kong SAR, China: ACM, 2024, s. 1-7. ISBN 979-8-4007-0522-9. Dostupné z: https://doi.org/10.1145/3641513.3650135.

@inproceedings{2484765,
   author = {Bals, Severin and Evangelidis, Alexandros and Křetínský, Jan and Waibel, Jakob},
   address = {Hong Kong SAR, China},
   booktitle = {Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024},
   doi = {https://doi.org/10.1145/3641513.3650135},
   keywords = {Markov decision process; quantitative verification; probabilistic model checking; controller synthesis},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Hong Kong SAR, China},
   isbn = {979-8-4007-0522-9},
   pages = {1-7},
   publisher = {ACM},
   title = {MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱},
   year = {2024}
}

TY  - CONF
ID  - 2484765
AU  - Bals, Severin - Evangelidis, Alexandros - Křetínský, Jan - Waibel, Jakob
PY  - 2024
TI  - MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱
PB  - ACM
CY  - Hong Kong SAR, China
SN  - 9798400705229
KW  - Markov decision process
KW  - quantitative verification
KW  - probabilistic model checking
KW  - controller synthesis
N2  - 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 multidimensional 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.
ER  -

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL. MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. Online. In \textit{Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024}. Hong Kong SAR, China: ACM, 2024, s.~1-7. ISBN~979-8-4007-0522-9. Dostupné z: https://doi.org/10.1145/3641513.3650135.

Přehled o publikaci