This work package, led by Sabina Rossi and Marco Bernardo, is concerned with the advances in behavioral equivalences, inspired by the concepts of approximated, ordinary, and exact lumpability, that are necessary to conduct noninterference and reversibility analyses in a CTMC-based setting. All the three research units will be involved in this work package.

This work package, led by Sabina Rossi, Carla Piazza, and Alessandro Aldini, is concerned with the advances in noninterference analysis that will stem from considering, for systems with users at different security levels, also their time behavior. The research units of UniVe and UniUd will concentrate on this work package given their expertise in the field, without excluding collaborations with the other research unit.

This work package, led by Claudio Antares Mezzina and Andrea Marin, is about the advances in reversibility analysis that will arise from the combination of causal consistent reversibility typical of distributed systems and time reversibility of Markov chain theory. The research units of UniUrb and UniVe will focus on this work package due to their expertise in the field, not excluding collaborations with the other research unit.

This work package, led by Carla Piazza and Claudio Antares Mezzina, is about the implementation in the PEPA Eclipse plug-in, and possibly in other tools supporting PEPA, of the modeling languages and analysis techniques of the previous work packages. All the three research units will be involved in this work package.

This work package, led by Marco Bernardo and Francesco Fabris, has to do with the application to private blockchains of the modeling languages and analysis techniques implemented in WP4. All the three research units will be involved in this work package.