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

Application domain/field

• Strategy synthesis
• Controller synthesis
• Resource-constrained systems
• Probabilistic systems

Type of tool

Synthesis tool

Expected input

• a Consumption Markov Decision Process
• Capacity $cap$
• Set of accepting states $T$

Format:

• CMDP: either as a PRISM model, Storm model, or it can be constructed in Python.
• $cap$: passed as an argument when calling the algorithm in Python
• $T$: passed as an argument when calling the algorithm in Python

Expected output

If it exists, then it returns a strategy $\sigma$ 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$

Internals

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.