TCS / Research / Publications / A Comparative Study of the Methods for Efficient Reachability Analysis
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

A Comparative Study of the Methods for Efficient Reachability Analysis

Reference:

Marko Rauhamaa. A comparative study of the methods for efficient reachability analysis. Research Report A14, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, September 1990.

Abstract:

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, Petri systems

Suggested BibTeX entry:

@techreport{HUT-TCS-A14,
    address = {Espoo, Finland},
    author = {Marko Rauhamaa},
    institution = {Helsinki University of Technology, Digital Systems Laboratory},
    month = {September},
    number = {A14},
    pages = {61},
    title = {A Comparative Study of the Methods for Efficient Reachability Analysis},
    type = {Research Report},
    year = {1990},
}

NOTE: Reprint of Licentiate's thesis; see URL below.
PostScript (743 kB)
GZipped PostScript (143 kB)
See www.tcs.hut.fi ...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 19 January 2010.