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

Severin Bals, Alexandros Evangelidis, Jan Křetínský, Jakob Waibel

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationHSCC 2024 - Proceedings of the 27th ACM International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control, HSCC 2024, part of CPS-IoT Week
PublisherAssociation for Computing Machinery, Inc
ISBN (Electronic)9798400705229
DOIs
StatePublished - 14 May 2024
Event27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024 - Hong Kong, China
Duration: 13 May 202416 May 2024

Publication series

NameHSCC 2024 - Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024, part of CPS-IoT Week

Conference

Conference27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024
Country/TerritoryChina
CityHong Kong
Period13/05/2416/05/24

Keywords

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

Fingerprint

Dive into the research topics of 'Poster Abstract: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints'. Together they form a unique fingerprint.

Cite this