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.
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.
| 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.
| 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 |