PV1 ⊧ PrIC3checks if the Markov decision process is safe

Symbolic model checking of Markov decision processes (MDPs).

Application domain/field

• Model checking
• Symbolic model checking
• Probabilistic model checking
• Markov decision processes (MDPs)

Type of tool

Probabilistic model checker

Expected input

• Global MDP M
• Set of bad states B
• Threshold $\lambda$

Format:

• MDP: PRISM guarded command language
• Set of bad states: ?
• Threshold: ?

Expected output

true or false. If the tool returns false, it will provide a possible counterexample. This can be caused by two reasons: either the MDP is indeed unsafe, or the heuristic was inappropriate. The counterexample consists of a subsystem of states of the MDP witnessing $P{r}^{max}(s_I\vDash ◊B)>\lambda$

Internals

Extension of IC3, for quantitative reachability in MDPs. Uses efficient data structures from Storm and uses Z3.

Comments

It is called a 'prototypical implementation' in the CAV '20 paper.