Résumé | We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in a Markov decision process with unknown probabilistic transition function and unknown reward function. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we show that in single end components two combinations of guarantees on the parity and mean-payoff objectives can be achieved depending on how much memory one is willing to use.
(i) For all epsilon we can construct an online-learning finite-memory strategy that satisfies the parity objective and which achieves an epsilon-optimal mean payoff, both almost surely.
(ii) Alternatively, for all epsilon and gamma there exists an online-learning infinite-memory strategy that satisfies the parity objective surely and which achieves an epsilon-optimal mean payoff with probability at least 1 - gamma.
We apply (i) to obtain safe and near optimal schedulers for a preemptible task scheduling problem. Our learning-based approach is compared against offline model checking and (shielded) model-free learning techniques based on shielded deep Q-learning. All the algorithms have been implemented to conduct experimental evaluations. |