MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
Authors:
Severin Bals,
Alexandros Evangelidis,
Jan Křetínský,
Jakob Waibel
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…
▽ More
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.
△ Less
Submitted 2 May, 2024; v1 submitted 26 May, 2023;
originally announced May 2023.
Optimistic and Topological Value Iteration for Simple Stochastic Games
Authors:
Muqsit Azeem,
Alexandros Evangelidis,
Jan Křetínský,
Alexander Slivinskiy,
Maximilian Weininger
Abstract:
While value iteration (VI) is a standard solution approach to simple stochastic games (SSGs), it suffered from the lack of a stop** criterion. Recently, several solutions have appeared, among them also "optimistic" VI (OVI). However, OVI is applicable only to one-player SSGs with no end components. We lift these two assumptions, making it available to general SSGs. Further, we utilize the idea i…
▽ More
While value iteration (VI) is a standard solution approach to simple stochastic games (SSGs), it suffered from the lack of a stop** criterion. Recently, several solutions have appeared, among them also "optimistic" VI (OVI). However, OVI is applicable only to one-player SSGs with no end components. We lift these two assumptions, making it available to general SSGs. Further, we utilize the idea in the context of topological VI, where we provide an efficient precise solution. In order to compare the new algorithms with the state of the art, we use not only the standard benchmarks, but we also design a random generator of SSGs, which can be biased towards various types of models, aiding in understanding the advantages of different algorithms on SSGs.
△ Less
Submitted 28 July, 2022;
originally announced July 2022.
