Distributed Explicit Bounded LTL Model Checking

Pavel Krcal


Abstract

Formal verification becomes a significant part of an industrial design process. Favourite formal verification method -- model checking -- is strongly limited by the size of the verified systems. It suffers from so called state explosion problem. We fight this problem by applying the idea of bounding the examined state space to explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We propose several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate and compare their behaviour.