PV3 ⊧ mcstachecks LTL/CTL properties of a model

Application domain/field

• Model checking
• Markov decision processes (MDPs)
• Reachability properties

Type of tool

Model checker

Expected input

One of the following types of models:

• STA (stochastic timed automaton)
• PTA (probabilistic timed automaton)
• MDP (Markov decision process)
• DTMC (discrete-time Markov chain)

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)."