Randomization Helps in LTL Model Checking

Investor logo
Investor logo

Warning

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

BRIM Luboš ČERNÁ Ivana NEČESAL Martin

Year of publication 2001
Type Article in Proceedings
Conference Process Algebra and Probabilistic Methods. Proceedings of PAPM-PROBMIV 2001
MU Faculty or unit

Faculty of Informatics

Citation
Field Information theory
Keywords Model checking; randomized algorithm; depth-first search
Description We present and analyze a new probabilistic method for automata based LTL model checking of non-proba\-bi\-listic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be stored during a computation and which could be omitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The method has been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice.
Related projects:

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