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.>

This paper presents the basis of PDIL, a language designed for specifying protocols and services and allowing automatic implementation. The main objectives of the language are unambiguous description, simulation and automatic implementation. The first part presents the objects that PDIL allows to manipulate : machines, channels, contexts, automata, interactions. The second part gives an overview of a PDIL description unit in its language aspect. This paper also introduces general ideas about the description of simulation and automatic implementation of protocols or services.