zbMATH — the first resource for mathematics

Randomization helps in LTL model checking. (English) Zbl 1007.68519
De Alfaro, Luca (ed.) et al., Process algebra and probabilistic methods. Performance modelling and verification. Joint international workshop, PAPM-PROBMIV 2001, Aachen, Germany, September 12-14, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2165, 105-119 (2001).
Summary: We present and analyze a new probabilistic method for automata based LTL model checking of non-probabilistic 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.
For the entire collection see [Zbl 0971.00028].
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link