MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives
Artificial Intelligence
2015-01-14 v1 Logic in Computer Science
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.
Cite
@article{arxiv.1501.03093,
title = {MultiGain: A controller synthesis tool for MDPs with multiple mean-payoff objectives},
author = {Tomáš Brázdil and Krishnendu Chatterjee and Vojtěch Forejt and Antonín Kučera},
journal= {arXiv preprint arXiv:1501.03093},
year = {2015}
}
Comments
Extended version for a TACAS 2015 tool demo paper