The VLPN benchmark suite is a collection of Nested-Unit Petri Nets (NUPNs) to be tackled by model checking tools.
The VLSAT benchmark suites are collections of logic formulas to be used in scientific experiments and software competitions. Three collections are available at the moment:
The VLTS benchmark suite is a collection of Labelled Transition Systems. It is designed to be a reference criterion for scientific assessment of algorithms and tools operating on large graphs.
The VLTS benchmark suite was a joint project of CWI/SEN2 and INRIA/VASY.
Temporal logics and mu-calculus is not always easy, especially for novice users. This can be solved, at least partially, by the use of predefined libraries. Two such libraries are provided below:
Library of usual properties expressed in the ACTL temporal logic
Library of usual properties expressed in the regular alternation-free mu-calculus language accepted by the EVALUATOR 3.0 model-checker of CADP
These two libraries have been developed by Radu Mateescu (INRIA/VASY).
This catalog lists a number of models, logics, and tools developed for modelling and verifying complex systems, the behaviour of which combines discrete aspects (namely, states and transitions) and continuous features (e.g., time, delays, probabilities, continuous laws, etc.).