PV1 ⊧ prohvercomputes safe upper bounds for probabilistic reachability probabilities

Application domain/field

• Model checking
• Hybrid systems

Type of tool

Model checker

Expected input

Stochastic Hybrid Automaton

Format:

Modest Toolset format or JANI format.

Internals

This is part of the Modest Toolset. It is described on the project page as a "safety model checker for SHA"

Comments

In the paper the language covered by ProHVer is called HModest.