# Abstraction-Refinement for Hierarchical Probabilistic Models

arXiv: https://arxiv.org/abs/2206.02653 · HTML: https://mlsanity.com/paper/2206.02653/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 38 references that are in the map.
- First posted on arXiv 6 Jun 2022.

## Builds on (most cited first, 11 of 11)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [Robust Finite-State Controllers for Uncertain POMDPs](https://mlsanity.com/paper/2009.11459/) (2020)
- [Hierarchical Solution of Markov Decision Processes using Macro-actions](https://mlsanity.com/paper/1301.7381/) (2013)
- [Parameter Synthesis for Markov Models: Faster Than Ever](https://mlsanity.com/paper/1602.05113/) (2016)
- [Accelerating Parametric Probabilistic Verification](https://mlsanity.com/paper/1312.3979/) (2013)
- [Fast Parametric Model Checking through Model Fragmentation](https://mlsanity.com/paper/2102.01490/) (2021)
- [Of Cores: A Partial-Exploration Framework for Markov Decision Processes](https://mlsanity.com/paper/1906.06931/) (2019)
- [Bounded Model Checking for Probabilistic Programs](https://mlsanity.com/paper/1605.04477/) (2016)
- [Fine-Tuning the Odds in Bayesian Networks](https://mlsanity.com/paper/2105.14371/) (2021)
- [Inductive Synthesis for Probabilistic Programs Reaches New Horizons](https://mlsanity.com/paper/2101.12683/) (2021)

## Built on by (most cited first, 6 of 6)

- [Efficient Sensitivity Analysis for Parametric Robust Markov Chains](https://mlsanity.com/paper/2305.01473/) (2023)
- [Composing Reinforcement Learning Policies, with Formal Guarantees](https://mlsanity.com/paper/2402.13785/) (2024)
- [Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement](https://mlsanity.com/paper/2506.17792/) (2025)
- [Spatio-temporal Value Semantics-based Abstraction for Dense Deep Reinforcement Learning](https://mlsanity.com/paper/2405.15829/) (2024)
- [An Algebraic Framework for Hierarchical Probabilistic Abstraction](https://mlsanity.com/paper/2502.21216/) (2025)
- [Scenario-Based Compositional Statistical Model Checking for Safety Specifications](https://mlsanity.com/paper/2610.05571/) (2026)

## Abstract (arXiv)

Markov decision processes are a ubiquitous formalism for modelling systems with non-deterministic and probabilistic behavior. Verification of these models is subject to the famous state space explosion problem. We alleviate this problem by exploiting a hierarchical structure with repetitive parts. This structure not only occurs naturally in robotics, but also in probabilistic programs describing, e.g., network protocols. Such programs often repeatedly call a subroutine with similar behavior. In this paper, we focus on a local case, in which the subroutines have a limited effect on the overall system state. The key ideas to accelerate analysis of such programs are (1) to treat the behavior of the subroutine as uncertain and only remove this uncertainty by a detailed analysis if needed, and (2) to abstract similar subroutines into a parametric template, and then analyse this template. These two ideas are embedded into an abstraction-refinement loop that analyses hierarchical MDPs. A prototypical implementation shows the efficacy of the approach.