摘要：The window mechanism was introduced by Chatterjee et al. to strengthenclassical game objectives with time bounds. It permits to synthesize systemcontrollers that exhibit acceptable behaviors within a configurable time frame,all along their infinite execution, in contrast to the traditional objectivesthat only require correctness of behaviors in the limit. The window concept hasproved its interest in a variety of two-player zero-sum games because itenables reasoning about such time bounds in system specifications, but alsothanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments byconsidering Markov decision processes. A fundamental problem in this context isthe threshold probability problem: given an objective it aims to synthesizestrategies that guarantee satisfying runs with a given probability. We solve itfor the usual variants of window objectives, where either the time frame is setas a parameter, or we ask if such a time frame exists. We develop a genericapproach for window-based objectives and instantiate it for the classicalmean-payoff and parity objectives, already considered in games. Our work pavesthe way to a wide use of the window mechanism in stochastic models.
关键词：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
