Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties

S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer +1

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 defi…