Application domain/field

Expected input

Two Markov decision processes:
  1. MDP that encodes the (uncertain) macro-MDP
  2. MDP that describes the parametric template for the subMDPs


Probabilistic program description in PRISM language

Expected output

Computed bounds (for what?)


The idea is to analyse an MDP by splitting it into two (hierarchical) levels. The first is a toplevel macro-MDP where they consider the subprocesses as some kind of uncertainty. They then use an analysis techniques for uncertain MDPs to approximate things. In this loop it removes uncertainty by analysing more and more of the previously unanalysed subprocesses. It is a technique that can be used for probabilistic model checking of MDPs. LEVEL-UP is a prototype built on top of Storm.
MDP Probabilistic programs


Related papers

Abstraction-Refinement for Hierarchical Probabilistic Models (CAV 2022)

Last publication date


ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.