Comparative Study of Methods for Efficient Reachability Analysis

摘要

Six recently proposed methods for efficient reachability analysis of distributedsystems are studied and compared: symmetry method, parameterizing method, stubborn set method, reduction theory, symbolic model checking, and incomplete state-space generation. Petri systems are used as the main presentation formalism. The methods are evaluated by how well they are suited for practical reachability graph generation by computer. One can summarize in brief that the stubborn set method, reduction theory and incomplete state-space generation are found very promising and they provide a useful aid to practical reachability analysis. The symmetry method yields a significant reduction in memory space but hardly in generation time. Symbolic model checking is a very general method and immense sample state-spaces have been analyzed with it but it is likely that for most practical systems the method performs far worse than the conventional methods. The parameterizing method is impractical and also its theoretical profits are questionable. Finally, it is observed that most of the methods are mutually independent, and it is considered how they can be combined to complement each other. Indeed, the symmetry method, stubborn set method, reduction theory and incomplete state-space generation can all be used simultaneously to obtain better results than with any of them alone.