10.23638/LMCS-16(4:13)2020
https://lmcs.episciences.org/5968
Brihaye, Thomas
Thomas
Brihaye
Delgrange, Florent
Florent
Delgrange
Oualhadj, Youssouf
Youssouf
Oualhadj
Randour, Mickael
Mickael
Randour
Life is Random, Time is Not: Markov Decision Processes with Window Objectives
The window mechanism was introduced by Chatterjee et al. to strengthen
classical game objectives with time bounds. It permits to synthesize system
controllers that exhibit acceptable behaviors within a configurable time frame,
all along their infinite execution, in contrast to the traditional objectives
that only require correctness of behaviors in the limit. The window concept has
proved its interest in a variety of two-player zero-sum games because it
enables reasoning about such time bounds in system specifications, but also
thanks to the increased tractability that it usually yields.
In this work, we extend the window framework to stochastic environments by
considering Markov decision processes. A fundamental problem in this context is
the threshold probability problem: given an objective it aims to synthesize
strategies that guarantee satisfying runs with a given probability. We solve it
for the usual variants of window objectives, where either the time frame is set
as a parameter, or we ask if such a time frame exists. We develop a generic
approach for window-based objectives and instantiate it for the classical
mean-payoff and parity objectives, already considered in games. Our work paves
the way to a wide use of the window mechanism in stochastic models.
episciences.org
Computer Science - Logic in Computer Science
Computer Science - Artificial Intelligence
Computer Science - Formal Languages and Automata Theory
Computer Science - Computer Science and Game Theory
Mathematics - Probability
Attribution 4.0 International (CC BY 4.0)
2020-10-17
2020-12-14
2020-12-14
eng
journal article
arXiv:1901.03571
10.48550/arXiv.1901.03571
1860-5974
2001.03894
10.4230/lipics.concur.2020.24
10.46298/lmcs-18(1:11)2022
10.48550/arxiv.2001.03894
https://lmcs.episciences.org/5968/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 16, Issue 4
Researchers
Students