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

a discrete-event simulator for deterministic STA

Application domain/field

• Model checking
• Nondeterminism

Type of tool

Model checker

Expected input

One of the following types of models:

• Timed automaton (STA or MA)
• Probabilistic timed automaton (RegionPTA, RepresentativePTA or ZonePTA)
• Markov decision process (MDP)

One of the following types of properties:

• Confidence interval (CI)
• Approximate probabilistic model checking (APMC)
• Sequential probability ratio test (SPRT)

Format:

Modest Toolset format or JANI format.

Internals

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"