Proceedings of the Thirty-ThirdInternational Joint Conference on Artificial Intelligence

Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty.Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP states.An increasingly popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states.For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defined in terms of probability distributions over states.Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verification techniques.In this work, we consider the…

• MO
  Ministry of Education, India