Introduction Cyber-physical systems (CPS), such as automated vehicles or robotics systems, are often characterized by two common features: i) they are safety-critical, hence formal guarantees of correctness are required, ii) they are affected by uncertainty, which is generally modeled through stochastic noise. Various formal verification and synthesis algorithms have been developed for these systems, with approaches including stochastic barrier functions…