Methodology for obtaining abstract views of state graphs labeled with probabilities and times. An example of application to a communication protocol

This paper presents a methodology for automatically obtaining abstract views of state graphs labeled with probabilities and times. An abstract view of a graph is a reduced graph obtained from a projection over a subset of states of the initial graph (observed states): the world of observed states is equivalent to the subworld of these states in the context of the initial graph on the basis of the so called notion of “first passage” An abstract view is a very important concept for modelling, verifying and evaluating points of views of the behaviour of a system. As an example of application, we consider an unidirectional data transfer protocol between a producer and a consumer