METHOD AND APPARATUS FOR SYMMETRY REDUCTION IN DISTRIBUTED MODEL CHECKING

摘要

A method for a model checking algorithm is provided. The method includes determining whether a class representative for a state has been processed, and generating a successor state for the state when the class representative for the state has not been processed. The method also includes determining which of a plurality of nodes is assigned to process the successor state, and processing the successor state at a node of the plurality of nodes that is assigned to process the successor state. Additionally another method for checking a model of a system is provided. This method processes a plurality of states for the model with a plurality of nodes using a distributed model checking technique. Each of the plurality of nodes uses symmetry reduction techniques to check if a representative state for a first state has been processed prior to processing the first state.