Multigain: A controller synthesis tool for mdps with multiple mean-payoff objectives Conference Paper

Author(s): Brázdil, Tomáš; Chatterjee, Krishnendu; Forejt, Vojtěch; Kučera, Antonín
Title: Multigain: A controller synthesis tool for mdps with multiple mean-payoff objectives
Title Series: LNCS
Affiliation IST Austria
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.
Keywords: Controller synthesis; Markov Decision Processes; Markov processes; mean payoff; Memoryless strategies; Curve fitting; Prisms; Approximate pareto curve; Novel algorithm; Other properties; Tool use
Conference Title: TACAS: Tools and Algorithms for the Construction and Analysis of Systems
Volume: 9035
Conference Dates: April 11-18, 2015
Conference Location: London, UK
ISBN: 978-3-662-54580-5
Publisher: Springer  
Date Published: 2015-01-01
Start Page: 181
End Page: 187
DOI: 10.1007/978-3-662-46681-0_12
Notes: The authors were in part supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games) and the research centre Institute for Theoretical Computer Science (ITI), grant No. P202/12/G061.
Open access: yes (repository)
IST Austria Authors
Related IST Austria Work