Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption

František Blahoudek, Murat Cubuktepe, Petr Novotný, Melkior Ornik, Pranay Thangeda, Ufuk Topcu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. We introduce FiMDP, a tool for controller synthesis in CMDPs with LTL objectives expressible by deterministic Büchi automata. The tool implements the recent algorithm for polynomial-time controller synthesis in CMDPs, but extends it with many additional features. On the conceptual level, the tool implements heuristics for improving the expected reachability times of accepting states, and a support for multi-agent task allocation. On the practical level, the tool offers (among other features) a new strategy simulation framework, integration with the Storm model checker, and FiMDPEnv - a new set of CMDPs that model real-world resource-constrained systems. We also present an evaluation of FiMDP on these real-world scenarios.

Original languageEnglish (US)
Title of host publicationFormal Methods - 24th International Symposium, FM 2021, Proceedings
EditorsMarieke Huisman, Corina Păsăreanu, Naijun Zhan
Number of pages17
ISBN (Print)9783030908690
StatePublished - 2021
Event24th International Symposium on Formal Methods, FM 2021 - Virtual, Online
Duration: Nov 20 2021Nov 26 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13047 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference24th International Symposium on Formal Methods, FM 2021
CityVirtual, Online

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Fuel in Markov Decision Processes (FiMDP): A Practical Approach to Consumption'. Together they form a unique fingerprint.

Cite this