CTL model checking algorithm using mapreduce

Abstract

Model checking is a promising automated verification technique. The state space explosion is the major difficulty of model checking. To deal with this problem, researchers present a new model checking algorithm for the temporal logic CTL based on MapReduce framework. And the algorithm's data structure is defined for the Kripke structure. This MapReduce algorithm outputs the set of states of the model that satisfies the formula by giving a model and a CTL formula. Researchers justify its correctness by an example with the EU formula. Finally, an example illustrates the validity of this algorithm, and the result shows this method is feasible. © 2013 Springer Science+Business Media New York.