  Automated synthesis of provably correct controllers for cyber-physical
systems is crucial for deployment in safety-critical scenarios. However, hybrid
features and stochastic or unknown behaviours make this problem challenging. We
propose a method for synthesising controllers for Markov jump linear systems
(MJLSs), a class of discrete-time models for cyber-physical systems, so that
they certifiably satisfy probabilistic computation tree logic (PCTL) formulae.
An MJLS consists of a finite set of stochastic linear dynamics and discrete
jumps between these dynamics that are governed by a Markov decision process
(MDP). We consider the cases where the transition probabilities of this MDP are
either known up to an interval or completely unknown. Our approach is based on
a finite-state abstraction that captures both the discrete (mode-jumping) and
continuous (stochastic linear) behaviour of the MJLS. We formalise this
abstraction as an interval MDP (iMDP) for which we compute intervals of
transition probabilities using sampling techniques from the so-called 'scenario
approach', resulting in a probabilistically sound approximation. We apply our
method to multiple realistic benchmark problems, in particular, a temperature
control and an aerial vehicle delivery problem.
