We introduce a parallel model checker for checking Markov decision Processes against linear time properties. The model checker extends the parallel model checker DiVinE and supports verification of qualitative properties.
We introduce a parallel model checker for checking Markov decision Processes against linear time properties. The model checker extends the parallel model checker DiVinE and supports verification of qualitative properties. (en)