Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes

Han Bao, Shinsaku Sakaue, Kazuki Watanabe

Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler.…