Properties of State Spaces and Their Applications

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek

Year of publication 2008
Type Article in Periodical
Magazine / Source International Journal on Software Tools for Technology Transfer (STTT)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords state space; explicit model checking; graph; experimental evaluation
Description Explicit model checking algorithms explore the full state space of a system. State spaces are usually treated as directed graphs without any specific features. We gather a large collection of state spaces and extensively study their structural properties. Our results show that state spaces have several typical properties, i.e., they are not arbitrary graphs. We also demonstrate that state spaces differ significantly from random graphs and that different classes of models (application domains, academic vs industrial) have different properties. We discuss consequences of these results for model checking experiments and we point out how to exploit typical properties of state spaces in practical model checking algorithms.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.