Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
This addresses the need for robust and constrained policy synthesis in planning and verification, though it appears incremental as it builds on existing methods for specific problem fragments.
The paper tackles the problem of computing reward-optimal policies for Markov decision processes (MDPs) that are both robust to perturbations and satisfy structural constraints, by introducing the first approach using a framework that integrates satisfiability solvers and probabilistic model checking, with experiments on hundreds of benchmarks showing feasibility and competitiveness with state-of-the-art methods.
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 MDP and (2) to satisfy additional structural constraints regarding, e.g., their representation or implementation cost. Computing such robust and constrained policies is indeed computationally more challenging. This paper contributes the first approach to effectively compute robust policies subject to arbitrary structural constraints using a flexible and efficient framework. We achieve flexibility by allowing to express our constraints in a first-order theory over a set of MDPs, while the root for our efficiency lies in the tight integration of satisfiability solvers to handle the combinatorial nature of the problem and probabilistic model checking algorithms to handle the analysis of MDPs. Experiments on a few hundred benchmarks demonstrate the feasibility for constrained and robust policy synthesis and the competitiveness with state-of-the-art methods for various fragments of the problem.