Beyond Interval MDPs: Tight and Efficient Abstractions of Stochastic Systems

TL;DR

This paper introduces new abstraction frameworks for stochastic systems that provide tighter probabilistic guarantees and improved computational efficiency for control synthesis, surpassing existing methods.

Contribution

It proposes multi-interval MDPs and set-valued MDPs, offering tighter abstractions and more efficient algorithms for control synthesis in stochastic systems.

Findings

SMDPs are tighter than MI-MDPs and IMDPs.

Control synthesis reduces to linear optimization or can avoid it.

Experiments show improved trade-offs in accuracy and efficiency.

Abstract

This work addresses the general problem of control synthesis for continuous-space, discrete-time stochastic systems with probabilistic guarantees via finite abstractions. While established methods exist, they often trade off accuracy for tractability. We propose a unified abstraction framework that improves both the tightness of probabilistic guarantees and computational efficiency. First, we introduce multi-interval MDPs (MI-MDPs), a generalization of interval-valued MDPs (IMDPs), which allows multiple, possibly overlapping clusters of successor states. This results in tighter abstractions but with increased computational complexity. To mitigate this, we further propose a generalized form of MDPs with set-valued transition probabilities (SMDPs), which model transitions as a fixed probability to a state cluster, followed by a non-deterministic choice within the cluster, as a sound abstraction. We show that control synthesis for MI-MDPs reduces to robust dynamic programming via linear optimization, while SMDPs admit even more efficient synthesis algorithms that avoid linear programming altogether. Theoretically, we prove that, given the partitioning of the state and disturbance spaces, both MI-MDPs and SMDPs yield tighter probabilistic guarantees than IMDPs, and that SMDPs are tighter than MI-MDPs. Extensive experiments across several benchmarks validate our theoretical results and demonstrate that SMDPs achieve favorable trade-offs among tightness, memory usage, and computation time.