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

• URL: http://arxiv.org/abs/2511.08078v2
• Date: Sat, 15 Nov 2025 14:59:10 GMT
• Title: Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
• Authors: Linus Heck, Filip Macák, Milan Češka, Sebastian Junges,
• Abstract summary: This paper contributes the first approach to effectively compute robust policies subject to arbitrary structural constraints.<n> Experiments on a few hundred benchmarks demonstrate the feasibility for constrained and robust policy synthesis.
• Score: 4.064849471241967
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Rectified Robust Policy Optimization for Model-Uncertain Constrained Reinforcement Learning without Strong Duality [53.525547349715595]
  We propose a novel primal-only algorithm called Rectified Robust Policy Optimization (RRPO)<n>RRPO operates directly on the primal problem without relying on dual formulations.<n>We show convergence to an approximately optimal feasible policy with complexity matching the best-known lower bound.
  arXiv  Detail & Related papers  (2025-08-24T16:59:38Z)
• Efficient Solution and Learning of Robust Factored MDPs [57.2416302384766]
  Learning r-MDPs from interactions with an unknown environment enables the synthesis of robust policies with provable guarantees on performance.<n>We propose novel methods for solving and learning r-MDPs based on factored state representations.
  arXiv  Detail & Related papers  (2025-08-01T15:23:15Z)
• Efficient Strategy Synthesis for MDPs via Hierarchical Block Decomposition [47.123254940289726]
  Software product lines and robotics utilise Markov decision processes (MDPs) to capture uncertainty and analyse sequential decision-making problems.<n>Despite the usefulness of conventional policy synthesis methods, they fail to scale to large state spaces.<n>Our approach addresses this issue and accelerates policy synthesis in large MDPs by dynamically refining the MDP and iteratively selecting the most fragile MDP regions for refinement.
  arXiv  Detail & Related papers  (2025-06-21T19:03:03Z)
• Scalable Chain of Thoughts via Elastic Reasoning [61.75753924952059]
  Elastic Reasoning is a novel framework for scalable chain of thoughts.<n>It separates reasoning into two phases--thinking and solution--with independently allocated budgets.<n>Our approach produces more concise and efficient reasoning even in unconstrained settings.
  arXiv  Detail & Related papers  (2025-05-08T15:01:06Z)
• Efficiently Training Deep-Learning Parametric Policies using Lagrangian Duality [55.06411438416805]
  Constrained Markov Decision Processes (CMDPs) are critical in many high-stakes applications.<n>This paper introduces a novel approach, Two-Stage Deep Decision Rules (TS- DDR) to efficiently train parametric actor policies.<n>It is shown to enhance solution quality and to reduce computation times by several orders of magnitude when compared to current state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-05-23T18:19:47Z)
• Recursively-Constrained Partially Observable Markov Decision Processes [13.8724466775267]
  We show that C-POMDPs violate the optimal substructure property over successive decision steps. Online re-planning in C-POMDPs is often ineffective due to the inconsistency resulting from this violation. We introduce the Recursively-Constrained POMDP, which imposes additional history-dependent cost constraints on the C-POMDP.
  arXiv  Detail & Related papers  (2023-10-15T00:25:07Z)
• Probabilistic Reach-Avoid for Bayesian Neural Networks [71.67052234622781]
  We show that an optimal synthesis algorithm can provide more than a four-fold increase in the number of certifiable states. The algorithm is able to provide more than a three-fold increase in the average guaranteed reach-avoid probability.
  arXiv  Detail & Related papers  (2023-10-03T10:52:21Z)
• Multi-Objective Policy Gradients with Topological Constraints [108.10241442630289]
  We present a new algorithm for a policy gradient in TMDPs by a simple extension of the proximal policy optimization (PPO) algorithm. We demonstrate this on a real-world multiple-objective navigation problem with an arbitrary ordering of objectives both in simulation and on a real robot.
  arXiv  Detail & Related papers  (2022-09-15T07:22:58Z)
• Linear programming-based solution methods for constrained POMDPs [0.5156484100374059]
  Constrained partially observable Markov decision processes (CPOMDPs) have been used to model various real-world phenomena. We use grid-based approximations in combination with linear programming (LP) models to generate approximate policies for CPOMDPs.
  arXiv  Detail & Related papers  (2022-06-28T15:22:24Z)
• Risk-Averse Decision Making Under Uncertainty [18.467950783426947]
  A large class of decision making under uncertainty problems can be described via Markov decision processes (MDPs) or partially observable MDPs (POMDPs) In this paper, we consider the problem of designing policies for MDPs and POMDPs with objectives and constraints in terms of dynamic coherent risk measures.
  arXiv  Detail & Related papers  (2021-09-09T07:52:35Z)
• Robust Constrained-MDPs: Soft-Constrained Robust Policy Optimization under Model Uncertainty [9.246374019271935]
  We propose to merge the theory of constrained Markov decision process (CMDP) with the theory of robust Markov decision process (RMDP) This formulation allows us to design RL algorithms that are robust in performance, and provides constraint satisfaction guarantees. We first propose the general problem formulation under the concept of RCMDP, and then propose a Lagrangian formulation of the optimal problem, leading to a robust-constrained policy gradient RL algorithm.
  arXiv  Detail & Related papers  (2020-10-10T01:53:37Z)
• Partial Policy Iteration for L1-Robust Markov Decision Processes [13.555107578858307]
  This paper describes new efficient algorithms for solving the common class of robust MDPs. We propose partial policy iteration, a new, efficient, flexible, and general policy iteration scheme for robust MDPs. Our experimental results indicate that the proposed methods are many orders of magnitude faster than the state-of-the-art approach.
  arXiv  Detail & Related papers  (2020-06-16T19:50:14Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.