D 2020

Qualitative Controller Synthesis for Consumption Markov Decision Processes

BLAHOUDEK, František, Tomáš BRÁZDIL, Petr NOVOTNÝ, Melkior ORNIK, Pranay THANGEDA et. al.

Basic information

Original name

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Authors

BLAHOUDEK, František (203 Czech Republic), Tomáš BRÁZDIL (203 Czech Republic, belonging to the institution), Petr NOVOTNÝ (203 Czech Republic, guarantor, belonging to the institution), Melkior ORNIK (191 Croatia), Pranay THANGEDA (356 India) and Ufuk TOPCU (792 Turkey)

Edition

Cham, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}, p. 421-447, 27 pp. 2020

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/20:00114617

Organization unit

Faculty of Informatics

ISBN

978-3-030-53290-1

ISSN

DOI

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

UT WoS

000695272500022

Keywords in English

decision making; Markov decision processes; controller synthesis; resource constraints

Tags

core_A, firank_1, formela-ver

Tags

International impact, Reviewed
Změněno: 29/4/2021 08:12, RNDr. Pavel Šmerk, Ph.D.

Abstract

V originále

Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. In a CMDP, the controller possesses a certain amount of a critical resource, such as electric power. Each action of the controller can consume some amount of the resource. Resource replenishment is only possible in special reload states, in which the resource level can be reloaded up to the full capacity of the system. The task of the controller is to prevent resource exhaustion, i.e. ensure that the available amount of the resource stays non-negative, while ensuring an additional linear-time property. We study the complexity of strategy synthesis in consumption MDPs with almost-sure Büchi objectives. We show that the problem can be solved in polynomial time. We implement our algorithm and show that it can efficiently solve CMDPs modelling real-world scenarios.

Links

GA19-15134Y, interní kód MU
Name: Verifikace a analýza pravděpodobnostních programů
Investor: Czech Science Foundation
GJ19-15134Y, research and development project
Name: Verifikace a analýza pravděpodobnostních programů
Displayed: 15/11/2024 04:10