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 of PRISM. Our tool extends PRISM by adding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i)~generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii)~generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
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 allowin…
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems
This paper is concerned with developing a software tool, called IMPaCT, for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov…
Cloud ComputingAMYTISS: Parallelized Automated Controller Synthesis for Large-Scale Stochastic Systems
In this paper, we propose a software tool, called AMYTISS, implemented in C++/OpenCL, for designing correct-by-construction controllers for large-scale discrete-time stochastic systems. This tool is employed to (i) build…
Cloud ComputingDeductive Controller Synthesis for Probabilistic Hyperproperties
Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable fo…
Multi-Objective Controller Synthesis with Uncertain Human Preferences
Complex real-world applications of cyber-physical systems give rise to the need for multi-objective controller synthesis, which concerns the problem of computing an optimal controller subject to multiple (possibly confli…