mlsanityData to 7 Oct 2026

Abstraction-Refinement for Hierarchical Probabilistic Models

arXiv 2206.02653 ↗First posted 6 Jun 2022cs.AI cs.LOcited by 5

Not on the map. Why?

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.

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

Builds on

11 of 38 references.

References · 11

  1. 2020The Probabilistic Model Checker Stormcited by 64
  2. 2014Verification of Markov Decision Processes using Learning Algorithmscited by 38
  3. 2020Robust Finite-State Controllers for Uncertain POMDPscited by 23
  4. 2013Hierarchical Solution of Markov Decision Processes using Macro-actionscited by 19
  5. 2016Parameter Synthesis for Markov Models: Faster Than Evercited by 12
  6. 2013Accelerating Parametric Probabilistic Verificationcited by 6
  7. 2021Fast Parametric Model Checking through Model Fragmentationcited by 6
  8. 2019Of Cores: A Partial-Exploration Framework for Markov Decision Processescited by 4
  9. 2016Bounded Model Checking for Probabilistic Programscited by 3
  10. 2021Fine-Tuning the Odds in Bayesian Networkscited by 3
  11. 2021Inductive Synthesis for Probabilistic Programs Reaches New Horizonscited by 2

Built on by

Cited by year

Citing papers per year: 2023: 1; 2024: 2; 2025: 2.

5 papers.

  1. 2023Efficient Sensitivity Analysis for Parametric Robust Markov Chainscited by 2
  2. 2024Composing Reinforcement Learning Policies, with Formal Guaranteescited by 2
  3. 2025Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinementcited by 1
  4. 2024Spatio-temporal Value Semantics-based Abstraction for Dense Deep Reinforcement Learningcited by 0
  5. 2025An Algebraic Framework for Hierarchical Probabilistic Abstractioncited by 0