In this talk, I will give an overview of the main instruments that I encountered during my PhD to reason formally on the behaviour of processes exhibiting both nondeterministic and probabilistic behaviour. We will talk about behavioural equivalences, their approximated versions and behavioural metrics. If time permits, we will also discuss the logical characterisations of equivalences and metrics that I obtained in my PhD.
