PV3 modeschecks properties of a model in presence of nondeterminism and rare events

a discrete-event simulator for deterministic STA

Application domain/field

Type of tool

Model checker

Expected input

One of the following types of models: One of the following types of properties:


Modest Toolset format or JANI format.


This is part of the Modest Toolset. It is described on the project page as a "statistical model checker for SHA, STA, PTA and MDP"
Automaton Model checking


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

Related papers

A Statistical Model Checker for Nondeterminism and Rare Events (TACAS 2018)

ProVerB specific

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