Jeudi 21 juin, 14h en salle Minquiers
Raphaël Berthon (ENS Rennes)
Threshold Constraints with Guarantees for Parity Objectives in Markov Decision Processes
The beyond worst case synthesis problem aims at designing controllers with a good expected performance, while giving a worst-case guarantee. In this talk, we focus on omega-regular conditions : given a Markov decision process, we show how to find strategies such that a first parity condition holds on all plays, and a second one holds with a probability greater than a threshold. Deciding if such a strategy exists lies in NP \cap coNP, and can in fact be reduced to parity games, leading to an efficient decision procedure.