MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator o…
Multiple Mean-Payoff Optimization under Local Stability Constraints
The long-run average payoff per transition (mean payoff) is the main tool for specifying the performance and dependability properties of discrete systems. The problem of constructing a controller (strategy) simultaneousl…
Symbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications
We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives…
Fast Synthesis for Symbolic Self-triggered Control under Right-recursive LTL Specifications
We extend previous work on symbolic self-triggered control for non-deterministic continuous-time nonlinear systems without stability assumptions to a larger class of specifications. Our goal is to synthesise a controller…
Formal Synthesis of Analytic Controllers for Sampled-Data Systems via Genetic Programming
This paper presents an automatic formal controller synthesis method for nonlinear sampled-data systems with safety and reachability specifications. Fundamentally, the presented method is not restricted to polynomial syst…