Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking

TL;DR

This paper introduces a novel framework for synthesizing reward-optimal policies for finite MDPs that are both robust to perturbations and satisfy complex structural constraints, leveraging satisfiability solvers and probabilistic model checking.

Contribution

It presents the first effective method to compute robust, constrained policies for MDPs using a flexible first-order constraint formulation integrated with satisfiability and probabilistic model checking.

Findings

Demonstrates feasibility on hundreds of benchmarks.

Achieves competitiveness with state-of-the-art methods.

Handles arbitrary structural constraints efficiently.

Abstract

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.