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.

翻译：针对已知有限马尔可夫决策过程（MDP）计算奖励最优策略的能力，支撑了规划、控制器综合与验证等领域的多种应用。然而，我们通常期望策略（1）具备鲁棒性，即在MDP的扰动下仍能保持良好性能；（2）满足额外的结构约束，例如在表示形式或实现成本方面的限制。计算此类兼具鲁棒性与约束条件的策略确实在计算上更具挑战性。本文提出了首个利用灵活高效框架有效计算满足任意结构约束的鲁棒策略的方法。我们通过允许在一组MDP的一阶理论中表达约束来实现灵活性，而效率的核心在于紧密整合可满足性求解器（以处理问题的组合复杂性）与概率模型检验算法（以处理MDP的分析）。在数百个基准测试上的实验证明了约束与鲁棒策略综合的可行性，并在该问题的多个子领域展现了与前沿方法的竞争力。