Synchronizing Objectives for Markov Decision Processes

TL;DR

This paper introduces synchronizing objectives for Markov decision processes, which ensure that over time, the system's state can be identified with high certainty, effectively making probabilistic systems behave deterministically.

Contribution

It establishes the decidability of enforcing synchronizing objectives in MDPs for various strategy types, including blind and pure strategies, and discusses the necessity of memory.

Findings

Decidable for general and blind strategies

Pure strategies are sufficient

Memory may be required for strategies

Abstract

We introduce synchronizing objectives for Markov decision processes (MDP). Intuitively, a synchronizing objective requires that eventually, at every step there is a state which concentrates almost all the probability mass. In particular, it implies that the probabilistic system behaves in the long run like a deterministic system: eventually, the current state of the MDP can be identified with almost certainty. We study the problem of deciding the existence of a strategy to enforce a synchronizing objective in MDPs. We show that the problem is decidable for general strategies, as well as for blind strategies where the player cannot observe the current state of the MDP. We also show that pure strategies are sufficient, but memory may be necessary.