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

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2024
Druh Článek ve sborníku
Konference Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1145/3641513.3652535
Klíčová slova Markov decision process; quantitative verification; probabilistic model checking; controller synthesis
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info