Date: September 1990
Pages: 61
Six recently proposed methods for efficient reachability analysis of distributed systems are studied and compared: symmetry method (Huber et al.), parameterising method (Lindqvist), stubborn set method (Valmari), reduction theory (Berthelot, Haddad), symbolic model checking (Burch et al.), and incomplete state-space generation (Holzmann). 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 summarise in brief that the stubborn set method, reduction theory and incomplete state-space generation are found very promising and they provide 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 analysed with it but it is likely that for most practical systems the method performs far worse than the conventional methods. The parameterising 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.
Keywords: reachability analysis, distributed systems, Petrisystems.