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
5/26/2023
cs.AIcs.LO

No confident code implementation found for this paper.

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

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Deductive Controller Synthesis for Probabilistic Hyperproperties

80% match2023

Controller synthesis method for multi-agent system based on temporal logic specification

78% match2025

Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions

78% match2023

Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions

76% match1 repo72023

Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games

75% match2024

RoboCertProb: Property Specification for Probabilistic RoboChart Models

74% match2024

Cite this paper

@article{bals2023multigain,
  title  = {MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints},
  author = {Severin Bals and Alexandros Evangelidis and Jan Křetínský and Jakob Waibel},
  year   = {2023},
  eprint = {2305.16752},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2305.16752v2}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2305.16752.svg)](https://codeofpaper.com/paper/2305.16752)

Discussion