Description and implementation of TPPAL: A timed and probabilistic process algebra

In this Phd Thesis, I present a timed and probabilistic process algebra which is used to specify the behaviour of concurrent system.;Also I present the translation of this process algebra to some graphical models which are easier to use to verify systems properties, concretely I use probabilistic dynamic states graph which is a kind of timed and probabilistic automata with some differences like the use of clocks. Other graphical models we use are timed automata and timed petrinets. Finally we present a tool to do automatically the translation from process algebra to the other models.