Summary: | 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.
|