Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

arXiv (Cornell University)

Abstract

This paper considers the problem of finding strategies that satisfy a mixture of sure and threshold objectives in Markov decision processes. We focus on a single $ω$-regular objective expressed as parity that must be surely met while satisfying $n$ reachability objectives towards sink states with some probability thresholds too. We consider three variants of the problem: (a) strict and (b) non-strict thresholds on all reachability objectives, and (c) maximizing the thresholds with respect to a lexicographic order. We show that (a) and (c) can be reduced to solving parity games, and (b) can be solved in $\sf{EXPTIME}$. Strategy complexities as well as algorithms are provided for all cases.

Authors 3

1. Raphaël Berthon Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , 52062 Aachen , Germany

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , 52062 Aachen , Germany

3. Tobias Winkler Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , 52062 Aachen , Germany