PV3 ⊧ STLmcchecks whether STL properties hold for a given hybrid system

Application domain/field

• Signal Temporal Logic (STL)
• Hybrid systems
• Bounded model checking

Type of tool

Model checker

Expected input

• Model of hybrid system, i.e. hybrid automaton
• STL properties

Format:

• Model: .model file, STLmc modelling language
• STL property: also specified in the model file, STLmc modelling language

Expected output

Whether the properties hold or not. If not, a counterexample can be shown.

Internals

The tool can be used to verify that, up to given bounds, the robustness degree of an STL formula $\phi$ is greater than a robustness threshold $ϵ>0$ for all possible behaviors of the ysstem. This is done by reducing the STL model checking problem to Boolean STL model checking using $ϵ$-strengthening. It uses SMT solvers such as Z3, Yices2 and dReal.