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)

Format:

Modest Toolset format or JANI format.

Internals

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

Links

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

Last commit date

27 August 2021 (last build in changelog)

Related papers

https://doi.org/10.1007/978-3-030-53291-8_26 (CAV '20)

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.