Markov decision processes can be viewed as transformers of probability distributions, giving rise to a sequence of distributions over MDP states. This view is useful in many applications, e.g., modeling robot swarms or chemical reaction networks, where the behavior is naturally interpreted as probability distributions over states. Somewhat surprisingly, in this setting basic reachability and safety problems turn out to be computationally intractable. The issue is further complicated by the question of how much memory is allowed: even for simple examples, policies for safety objectives over distributions can require infinite memory and randomization.

In light of this, we ask what can one do to tackle these problems in theory and in practice? After taking a look at some theoretical insights, we adopt an over-approximation route to approach these questions. Inspired by the success of invariant synthesis in program verification, we develop a framework for inductive template-based synthesis of certificates and policies for safety and reach-avoidance objectives in MDPs. We show the effectiveness of our approach as well as explore limitations and extensions to omega-regular properties.