Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

Raphaël Berthon, Joost-Pieter Katoen, Tobias Winkler

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.

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives

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 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 . Strategy complexities as well as algorithms are provided for all cases.
Paper Structure (8 sections, 1 equation, 1 figure, 1 table)

This paper contains 8 sections, 1 equation, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Running example
  3. This paper
  4. Contributions
  5. Related work
  6. Preliminaries
  7. MDPs, Strategies, and Objectives
  8. Multi-Objectives and Pareto Frontiers

Figures (1)

  • Figure 1: An MDP with $Act = \{\textcolor{red}{a}, \textcolor{green!50!black}{b}, pair_1, pair_2, *\}$, target sets $F_1$, $F_2$, and parity condition $\mathop{\mathrm{\rho}}\nolimits$ assigning 0 to the sinks and 1 to the non-sinks. Right: The Pareto frontier.

Theorems & Definitions (1)

  • definition thmcounterdefinition: Pareto frontier