PV3 mcstachecks LTL/CTL properties of a model

Application domain/field

Type of tool

Model checker

Expected input

One of the following types of models: And properties that should be checked (LTL or CTL)


Modest Toolset format or JANI format.


This is part of the Modest Toolset. It is described on the project page as a "disk-based explicit-state model checker for STA (stochastic timed automata), PTA (probabilistic timed automata) and MDP (Markov decision processes)."
Automaton CTL LTL Model checking


Related papers

Optimistic Value Iteration (CAV '20)

Last publication date

14 July 2020

ProVerB specific

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