xpelanek@fi.muni.cz

Masaryk University Brno

* 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.

- 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 reported results.
- To provide acces to more detailed statistics which cannot be included in a paper (detailed information about each state space, more statistics, correlation graphs).
- To provide acces to generated state spaces and so enable other researchers to perform more measurements.

- Typical Structural Properties of State Spaces - paper describing the measurements, results, and application.
- Detailed information - overview of investigated state spaces, listing of parameters for each graph
- Summary information - overall statistics, comparisons of parameters for different types of models, ...

- VLTS 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).
- Interactive Visualization of State Transition Systems: The goal of this project is to provide information about the state space by means of visualization techniques allowing users to interactively explore large state spaces.