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

Application domain/field

Type of tool

Synthesis tool

Expected input

Format:

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

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.
Synthesis

Links

Last commit date

15 March 2021

Related papers

https://doi.org/10.1007/978-3-030-53291-8_22

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.