PV2 FiMDP: Fuel in MDPsynthesises a controller for a resource-constrained Markov Decision Process

Application domain/field

Type of tool

Synthesis tool

Expected input


Expected output

If it exists, then it returns a strategy σ such that when starting with resource level d, the resource level never drops below 0 and the system infinitely often visits some state in T


This technique focuses on synthesizing controllers for resource-constrained Markov decision processes (MDPs). This controller must ensure that (1) some linear-time property is satisfied and (2) that the system's operation is not compromised by lack of resources (e.g. power). Consumption Markov Decision Processes (CMDPs) are used to represent the resource-constrained MDPs.


Related papers

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.