ImpRator

This tool (standing for Inverse Method for Policy with Reward AbstracT behaviOR) is an implementation of the inverse method in the framework of Parametric Markov Decision Processes.

ImpRator takes as an input a Parametric Markov Decision Process, and a reference valuation for each parameter. It outputs a constraint on the parameters such that, for all parameter valuation satisfying the constraint, each optimal policy for the reference valuation is also optimal for this new parameter valuation (and conversely).

ImpRator uses matrix inversion to compute the parametric value in the algorithm. Note that ImpRator also allows the use of Markov Decision Processes with no absorbing state, by adding a discount.

ImpRator has been developed in OCaml by Étienne André in 2009-2010 at Laboratoire Spécification et Vérification, ENS Cachan, France. It is provided under the GNU-GPL license.

Using ImpRator

ImpRator takes as input a text file describing a Parametric Markov Decision Process, including the reference value for each parameter.

The syntax is described in a functional style, with OCaml-style (possibly nested) comments. Note that the name of the input file is hard-coded at the top of the file IMPERATOR.ml. This could be very easily improved.

Hence, the call syntax is directly:

./IMPRATOR

The result is given directly in the terminal.

Download and Install

Version Release Source (tar.bz2) Source (zip) Binary
0.1 22nd April 2009 ImpRator.tar.bz2 (29Ko) ImpRator.zip (39Ko) ImpRator (204Ko)

The binary is a standalone binary for Ubuntu; it has been compiled using Ubuntu 10.10. If it doesn’t work, please compile the source code.

Examples

Name File
Example from INFINITY’09 paper ExampleINFINITY2009.imp
Sample example sampleExample.imp
Sample example with 2 costs sampleExample2Costs.imp
Sample example with 2 costs and no loop sampleExample2CostsNoLoop.imp
Toy example exToy.imp
Example from "Sample solution for the MDP problem" exMDP.imp
Going from Paris to LSV ParisLSV.imp
Going from Paris to Bologna ParisBologna.imp
Going from Rennes to LSV RennesLSV.imp
Example from Rutgers exRutgers.imp
From slides "Markov Decision Process" by Stachniss and Burgard exSlidesMDP.imp
Dynamic Power Managment DynamicPowerManagment.imp

Contact

References