2026
Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
AAAI 2026technical
The ability to compute reward-optimal policies for given and known finite Markov decision processes (MDPs) underpins a variety of applications across planning, controller synthesis, and verification. However, we often want policies (1) to be robust, i.e., they perform well on perturbations of the M