MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives

2015/01/13 by Tomáš Brázdil, Brázdil, Tomáš, Krishnendu Chatterjee +5 · 1 citation
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.AI #cs.LO

paper · pdf · doi:10.48550/arxiv.1501.03093

Extended version for a TACAS 2015 tool demo paper

arxiv created 2015/01/13 · arxiv updated 2015/01/14

Abstract

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.

Cited by

• Steady-State Strategy Synthesis for Swarms of Autonomous Agents

Related

• MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
• Simple Strategies in Multi-Objective MDPs (Technical Report)
• MDP Geometry, Normalization and Reward Balancing Solvers
• Policies Grow on Trees: Model Checking Families of MDPs
• Efficient Strategy Iteration for Mean Payoff in Markov Decision\n Processes