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

Anton\'in Ku\v{c}era; Krishnendu Chatterjee; Tom\'a\v{s} Br\'azdil; Vojt\v{e}ch Forejt

REVIEW

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

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1501.03093 v1 pith:TEK4PH4V submitted 2015-01-13 cs.AI cs.LO

Tomáš Brázdil , Krishnendu Chatterjee , Vojtěch Forejt , Antonín Kučera This is my paper

classification cs.AIcs.LO

keywords mean-payoffobjectivesmultipletoolmdpsprismstrategiesgenerating

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original 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.

Discussion (0). Sign in to comment.

Pith tools