Abstraction-Refinement for Hierarchical Probabilistic Models

Sebastian Junges*, Matthijs T.J. Spaan

*Corresponding author for this work

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

3 Citations (Scopus)
22 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 34th International Conference, CAV 2022, Proceedings
EditorsSharon Shoham, Yakir Vizel
Place of PublicationCham
Number of pages22
EditionPart 1
ISBN (Electronic)978-3-031-13185-1
ISBN (Print)978-3-031-13184-4
Publication statusPublished - 2022
Event34th International Conference on Computer Aided Verification, CAV 2022 - Haifa, Israel
Duration: 7 Aug 202210 Aug 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13371 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference34th International Conference on Computer Aided Verification, CAV 2022


Dive into the research topics of 'Abstraction-Refinement for Hierarchical Probabilistic Models'. Together they form a unique fingerprint.

Cite this