TY - GEN
T1 - Fuel in Markov Decision Processes (FiMDP)
T2 - 24th International Symposium on Formal Methods, FM 2021
AU - Blahoudek, František
AU - Cubuktepe, Murat
AU - Novotný, Petr
AU - Ornik, Melkior
AU - Thangeda, Pranay
AU - Topcu, Ufuk
N1 - Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85119837676&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85119837676&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-90870-6_34
DO - 10.1007/978-3-030-90870-6_34
M3 - Conference contribution
C2 - 35072175
AN - SCOPUS:85119837676
SN - 9783030908690
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 640
EP - 656
BT - Formal Methods - 24th International Symposium, FM 2021, Proceedings
A2 - Huisman, Marieke
A2 - Păsăreanu, Corina
A2 - Zhan, Naijun
PB - Springer
Y2 - 20 November 2021 through 26 November 2021
ER -