We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm benefits from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions on the models that can be analyzed; no restrictions on the way states are distributed; and no restrictions on the way work is shared among processors. We evaluate the performance of different versions of our algorithm and compare our results with those obtained using other parallel model checking tools. One of the most novel contributions of this work is to study a space-efficient variant for CTL model-checking that does not require to store the whole transition graph but that operates, instead, on a reverse spanning tree.
Comparison with DiVinE. We now compare our algorithms with DiVinE @cite_0 , which is the state of the art tool for parallel model checking of LTL. The results given here have been obtained with DiVinE 2.5.2, considering only the best results given by the owcty or map, separately. This benchmark (experimental data and examples are available in report @cite_1 ) is based on the set of models borrowed from DiVinE on which, for a broader comparison, we check both valid and non valid properties. Figure shows the exact set of models and formulas that are used. All experiments were carried out using 16 cores and with an initial hash table sized enough to store all states. The DiVinE experiments were executed with flag () to remove counter-example generation.
@cite_0 @cite_1
2533662917 2889067012
Model checking became a standard method of analyzing complex systems in many application domains. No doubt, a number of applications is placing great demands on model checking tools. The process of analysis of complex and real-life systems often requires vast computation resources, memory in particular. This phenomenon, referred to as the state space explosion problem, has been tackled by many researchers during the past two decades. A plethora of more or less successful techniques to fight the problem have been introduced, including parallel and distributed-memory processing. DiVinE is a tool for LTL model checking and reach ability analysis of discrete distributed systems. The tool is able to efficiently exploit the aggregate computing power of multiple network-interconnected multi-cored workstations in order to deal with extremely large verification tasks. As such it allows to analyze systems whose size is far beyond the size of systems that can be handled with regular sequential tools. While the main focus of the tool is on high-performance explicit state model checking, an emphasis is also put on ease of deployment and usage. Additionally, the component architecture and publicly available source code of Divine allow for its usage as a platform for research on parallel and distributed-memory model checking techniques. In this work, we present new algorithms for exhaustive parallel model checking that are as efficient as possible, but also ''friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.