Generating the syntactic and semantics graphs for a Markovian process algebra

ROSA is a Markovian process algebra for the description and analysis of probabilistic and non-deterministic concurrent processes. ROSA allows us to evaluate performance indexes as well as to check some temporal requirements. As application, we analyse the alternating bit protocol obtaining the average time to send a message, considering that channels may fail with a known probability.