PV0 ⊧ LEVEL-UP

Application domain/field

• Markov decision processes (MDPs)
• Probabilistic behavior
• Probabilistic programs
• Subroutines
• Probabilistic model checking
• Model checking

Expected input

Two Markov decision processes:

1. MDP that encodes the (uncertain) macro-MDP
2. MDP that describes the parametric template for the subMDPs

Format:

Probabilistic program description in PRISM language

Expected output

Computed bounds (for what?)

Internals

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.