Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

Nov 28 14:00 ₂₀₂₃

Abstract: When verifying multiple properties, it is sufficient to verify each individually, but when synthesizing strategies that satisfy multiple objectives, these objectives must be considered together. We consider the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single omega-regular objective expressed as parity that must be surely met while satisfying n reachability objectives with some probability thresholds too. We consider three combinations with a sure parity objective: (a) strict and (b) non-strict thresholds on all reachability objectives, and (c) maximizing the thresholds under a lexicographic ordering on the reachability objectives. We highlight the notion of projection for combining multiple objectives. We show that the decision variants of (a) are in PTIME, (b) in EXPTIME, and (c) can be solved by considering n parity games, and give associated algorithms.