Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Policy Synthesis for Interval MDPs via Polyhedral Lyapunov Functions

Negar Monir, Sadegh Soudjani

TL;DR

This work addresses policy synthesis for multi-objective interval MDPs by recasting value iteration as a discrete-time switched affine system with interval uncertainties. It introduces polyhedral Lyapunov functions to define a tight invariant set of attraction (ISoA) and uses counterexample-guided inductive synthesis (CEGIS) with SMT or optimization to construct Polyhedral ISoAs, enabling robust policy synthesis without Pareto-front computations. The authors develop a robust VI algorithm that converges value vectors toward target values within a controllable neighborhood, validated on recycling robots and EV battery life-cycle cases. The approach improves convergence guarantees under uncertainty, offers tighter error bounds than quadratic certificates, and provides practical pathways for scalable MOIMDP control in safety-critical settings.

Abstract

Decision-making under uncertainty is central to many safety-critical applications, where decisions must be guided by probabilistic modeling formalisms. This paper introduces a novel approach to policy synthesis in multi-objective interval Markov decision processes using polyhedral Lyapunov functions. Unlike previous Lyapunov-based methods that mainly rely on quadratic functions, our method utilizes polyhedral functions to enhance accuracy in managing uncertainties within value iteration of dynamic programming. We reformulate the value iteration algorithm as a switched affine system with interval uncertainties and apply control-theoretic stability principles to synthesize policies that guide the system toward a desired target set. By constructing an invariant set of attraction, we ensure that the synthesized policies provide convergence guarantees while minimizing the impact of transition uncertainty in the underlying model. Our methodology removes the need for computationally intensive Pareto curve computations by directly determining a policy that brings objectives within a specified range of their target values. We validate our approach through numerical case studies, including a recycling robot and an electric vehicle battery, demonstrating its effectiveness in achieving policy synthesis under uncertainty.

Policy Synthesis for Interval MDPs via Polyhedral Lyapunov Functions

TL;DR

This work addresses policy synthesis for multi-objective interval MDPs by recasting value iteration as a discrete-time switched affine system with interval uncertainties. It introduces polyhedral Lyapunov functions to define a tight invariant set of attraction (ISoA) and uses counterexample-guided inductive synthesis (CEGIS) with SMT or optimization to construct Polyhedral ISoAs, enabling robust policy synthesis without Pareto-front computations. The authors develop a robust VI algorithm that converges value vectors toward target values within a controllable neighborhood, validated on recycling robots and EV battery life-cycle cases. The approach improves convergence guarantees under uncertainty, offers tighter error bounds than quadratic certificates, and provides practical pathways for scalable MOIMDP control in safety-critical settings.

Abstract

Decision-making under uncertainty is central to many safety-critical applications, where decisions must be guided by probabilistic modeling formalisms. This paper introduces a novel approach to policy synthesis in multi-objective interval Markov decision processes using polyhedral Lyapunov functions. Unlike previous Lyapunov-based methods that mainly rely on quadratic functions, our method utilizes polyhedral functions to enhance accuracy in managing uncertainties within value iteration of dynamic programming. We reformulate the value iteration algorithm as a switched affine system with interval uncertainties and apply control-theoretic stability principles to synthesize policies that guide the system toward a desired target set. By constructing an invariant set of attraction, we ensure that the synthesized policies provide convergence guarantees while minimizing the impact of transition uncertainty in the underlying model. Our methodology removes the need for computationally intensive Pareto curve computations by directly determining a policy that brings objectives within a specified range of their target values. We validate our approach through numerical case studies, including a recycling robot and an electric vehicle battery, demonstrating its effectiveness in achieving policy synthesis under uncertainty.
Paper Structure (19 sections, 3 theorems, 61 equations, 8 figures, 1 table, 3 algorithms)

This paper contains 19 sections, 3 theorems, 61 equations, 8 figures, 1 table, 3 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries and Problem Statement
  3. Multi-objective Interval Markov Decision Processes
  4. Problem Statement
  5. VI Algorithm as dt-SAS with Uncertainties
  6. Constructing a Feasible Set of Values
  7. Stability Analysis of the dt-USAS
  8. Policy Synthesis for MOIMDPs
  9. Synthesizing Polyhedral ISoA via CEGIS and SMT
  10. Synthesizing Polyhedral ISoA via Optimization-based CEGIS
  11. Robust Lyapunov-Based VI Algorithm
  12. Computational Complexities
  13. Case Studies
  14. Recycling Robot with an MDP Model
  15. An IMDP Example
  16. ...and 4 more sections

Key Result

Lemma 1

For any stationary policy $\pi$, any $\gamma_m\in(0,1)$ with $m \in \mathbb{N}_q$, and any initial value $\hat{W}_{0}$, $\hat{W}_k$ in eq:nominal_VI asymptotically converges to the corresponding steady-state values $\hat{W}_{\pi,ss} = (I-\hat{A}_\pi)^{-1}\hat{B}_\pi$.

Figures (8)

  • Figure 1: High-level representation of the proposed approach.
  • Figure 2: Representation of the CEGIS approach to find a valid PLF.
  • Figure 3: Recycling Robot. This illustration depicts the CEGIS procedure of Algorithm \ref{['alg learn cegis']} for computing the polyhedral ISoA. (a) The learner proposes an initial PLF candidate that creates a feasible region (yellow), but the verifier identifies a counterexample (red cross). (b)–(d) Each counterexample generates a new constraint that refines the feasible region, and the updated candidate is re-evaluated by the verifier. (e) After five iterations, no further counterexamples are found, indicating that the candidate PLF satisfies all the required conditions. (f) The final polyhedral ISoA is defined by the resulting feasible region.
  • Figure 4: Recycling Robot. Results of Algorithm \ref{['relax vi alg moimdp']}. (a) Iterative evolution of the value function $W_k$, which converges to $W_{\text{tar}}$, together with the synthesized policy $\pi_k$. (b) Error trajectories $E_k$ under the computed policy, all converging to the polyhedral ISoA and remaining inside thereafter. (c) Evolution of the PLF, which decreases monotonically, drops below $1$, and stays under $1$, confirming invariance.
  • Figure 5: IMDP Example adopted from hahn2019interval.
  • ...and 3 more figures

Theorems & Definitions (6)

  • Definition 1
  • Remark 1: Multi-objective MDPs
  • Lemma 1
  • Definition 2: ISoA
  • Theorem 1
  • Theorem 2