FiMDP - Fuel in Markov Decision Processes

Python Package with Algorithms for Controller Synthesis in Resource-constrained Markov Decision Processes

FiMDP is a Python package for analysis and controller synthesis of Consumption Markov Decision Processes (ConsMDPs) — MDPs with resource constraints. The model of ConsMDPs and the basic algorithms implemented in FiMDP are described in our paper presented at CAV2020 [1].

Our related project called FiMDPEnv is a set of environments that work with FiMDP and can create animations like this one.

Multiple agents following energy-aware policies in UUVEnv from FiMDPEnv.

Installation

FiMDP can be installed using pip from PyPI

pip install -U fimdp

While the baseline package has minimal dependencies, FiMDP depends on several other tools for extended functionality. Some of the recommended dependencies are:

• Graphviz: for visualizations in Jupyter notebooks,
• Storm and Stormpy: for reading PRSIM, JANI, and Storm models,
• Spot: for support of labeled ConsMDPs and specifications given as deterministic Büchi automata or the recurrence fragment of Linear-time Temporal Logic (LTL).

Usage and documentation (work in progress)

The directory tut contains several notebooks that explain how to use FiMDP. The notebook Basics.ipynb is a good starting point.

For a complete overview of the tool, installation options, source code documentation, and interactive examples refer to FiMDP readthedocs.

Evaluations

Notebooks evaluationg performance of FiMDP are stored in a separate repository FiMDP-Evaluation.

Contact

If you have any trouble with the installation, or have any questions, raise an issue or email František (Fanda) Blahoudek or Pranay Thangeda.

References

[1] Blahoudek F., Brázdil T., Novotný P., Ornik M., Thangeda P., Topcu U. (2020) Qualitative Controller Synthesis for Consumption Markov Decision Processes. In proceeding of CAV 2020. Lecture Notes in Computer Science, vol 12225. Springer. https://doi.org/10.1007/978-3-030-53291-8_22