What do have state spaces in common? What are their typical properties?
Can state spaces be modeled by random graphs or by some class of regular
graphs in a satisfactory manner? Can we exploit these typical properties to
traverse or model check a state space more efficiently? Or at least to better
analyze complexity of algorithms? Can some information about a state space be
of any use to the user or to the developer of a model checker? Is there any
significant difference between toy academical models and real life case
studies? Are state spaces similar to such an extent that it does not matter
which models we choose for benchmarking our algorithms?
Collect large number of state spaces generated from different tools and
models from many different people.
Measure parameters of collected state spaces, compute statistics.
Try to answer the questions.
Aims of these web-pages:
To give information about what state spaces have been studied and about the
way in which they have been generated and so enable indepentent verification of
To provide acces to more detailed statistics which cannot be included in
a paper (detailed information about each state space, more statistics,
To provide acces to generated state spaces and so enable other
researchers to perform more measurements.
Summary information - overall statistics,
comparisons of parameters for different types of models, ...
benchmark suit: This is a collection of Very Large Transition Systems
(VLTS) stored in a compact bcg format. Compared to our collection, VLTS
benchmark suit have larger state spaces and edges are labeled by actions. On
the other hand, our collection contains state spaces for more different model
checkers and we provide detailed statistics for each example (this can be
usefull for making sense of results of experiments).