Bounds for Synchronizing Markov Decision Processes

TL;DR

This paper studies synchronizing objectives in Markov decision processes, introduces new modes, and provides algorithms and complexity results for deciding these properties, including explicit bounds and complexity classifications.

Contribution

It introduces two new qualitative synchronizing modes and offers tight algorithms and complexity bounds for their decision problems.

Findings

Deciding positive and bounded synchronizing from some point is coNP-complete.

Algorithms and tight complexity results are provided for various synchronizing modes.

Explicit bounds on the parameter epsilon are established for all modes.

Abstract

We consider Markov decision processes with synchronizing objectives, which require that a probability mass of $1-\epsilon$ accumulates in a designated set of target states, either once, always, infinitely often, or always from some point on, where $\epsilon = 0$ for sure synchronizing, and $\epsilon \to 0$ for almost-sure and limit-sure synchronizing. We introduce two new qualitative modes of synchronizing, where the probability mass should be either positive, or bounded away from $0$. They can be viewed as dual synchronizing objectives. We present algorithms and tight complexity results for the problem of deciding if a Markov decision process is positive, or bounded synchronizing, and we provide explicit bounds on $\epsilon$ in all synchronizing modes. In particular, we show that deciding positive and bounded synchronizing always from some point on, is coNP-complete.