Decidability issues in reduced reachability analysis

Reachability analysis, which is the most used technique in protocol validation, is based on the construction of a graph called the reachability graph. However this technique has two serious drawbacks: the undecidability of the finiteness of the reachability graph and the state explosion when it is finite. To cope with the latter problem, reduction techniques are required. After a brief presentation of their reduced reachability graph the authors deal with related decidability issues and show how decidability results can be applied to the global reachability graph