PV3 modyshchecks properties of a Markov decision process with dynamic search and heuristic planning

Application domain/field

Type of tool

Model checker

Expected input


Modest Toolset format or JANI format.


This is part of the Modest Toolset. It is described on the project page as a "probabilistic model checker for MDP based on dynamic search and heuristic planning techniques"
Automaton Model checking


Project page (of the Modest Toolset): https://www.modestchecker.net

Related papers

A Modest Approach to Dynamic Heuristic Search in Probabilistic Model Checking (QEST 2021)

ProVerB specific

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