  We present a data-driven framework for strategy synthesis for partially-known
switched stochastic systems. The properties of the system are specified using
linear temporal logic (LTL) over finite traces (LTLf), which is as expressive
as LTL and enables interpretations over finite behaviors. The framework first
learns the unknown dynamics via Gaussian process regression. Then, it builds a
formal abstraction of the switched system in terms of an uncertain Markov
model, namely an Interval Markov Decision Process (IMDP), by accounting for
both the stochastic behavior of the system and the uncertainty in the learning
step. Then, we synthesize a strategy on the resulting IMDP that maximizes the
satisfaction probability of the LTLf specification and is robust against all
the uncertainties in the abstraction. This strategy is then refined into a
switching strategy for the original stochastic system. We show that this
strategy is near-optimal and provide a bound on its distance (error) to the
optimal strategy. We experimentally validate our framework on various case
studies, including both linear and non-linear switched stochastic systems.
