Bounds for Synchronizing Markov Decision Processes
We consider Markov decision processes with synchronizing objectives, which require that a probability mass of $1-ε$ accumulates in a designated set of target states, either once, always, infinitely often, or always from some point on, where $ε= 0$ for sure synchronizing, and $ε\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 $ε$ in all synchronizing modes. In particular, we show that deciding positive and bounded synchronizing always from some point on, is coNP-complete.